### Nuprl Lemma : fps-compose-ucont

[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)].  ∀x:X. fps-ucont(X;eq;r;f.f(x:=g)) supposing valueall-type(X)

Proof

Definitions occuring in Statement :  fps-ucont: fps-ucont(X;eq;r;f.G[f]) fps-compose: g(x:=f) power-series: PowerSeries(X;r) deq: EqDecider(T) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] universe: Type crng: CRng
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T valueall-type: valueall-type(T) has-value: (a)↓ all: x:A. B[x] crng: CRng comm: Comm(T;op) and: P ∧ Q cand: c∧ B rng: Rng sq_stable: SqStable(P) implies:  Q squash: T fps-ucont: fps-ucont(X;eq;r;f.G[f]) exists: x:A. B[x] subtype_rel: A ⊆B fps-restrict: fps-restrict(eq;r;f;d) fps-compose: g(x:=f) fps-coeff: f[b] tlp: tlp(L) hdp: hdp(L) so_lambda: λ2x.t[x] power-series: PowerSeries(X;r) so_apply: x[s] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) iff: ⇐⇒ Q ifthenelse: if then else fi  bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A rev_implies:  Q prop: ring_p: IsRing(T;plus;zero;neg;times;one) group_p: IsGroup(T;op;id;inv) listp: List+ ge: i ≥  le: A ≤ B less_than': less_than'(a;b) true: True cons: [a b] top: Top length: ||as|| list_ind: list_ind nil: [] bag-union: bag-union(bbs) concat: concat(ll) bag-append: as bs nat: satisfiable_int_formula: satisfiable_int_formula(fmla) bag-size: #(bs) reduce: reduce(f;k;as) colength: colength(L) less_than: a < b so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] decidable: Dec(P) l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k nat_plus: + select: L[n] sub-bag: sub-bag(T;as;bs)
Lemmas referenced :  rng_plus_comm sq_stable__monoid_p rng_car_wf rng_plus_wf rng_zero_wf crng_properties rng_properties crng_all_properties bag-append_wf bag-rep_wf bag-size_wf list-subtype-bag bag-summation-equal listp_wf bag_wf bag-parts'_wf infix_ap_wf rng_times_wf hdp_wf length_wf_nat tlp_wf bag-product_wf rng_one_wf deq-sub-bag_wf eqtt_to_assert assert-deq-sub-bag eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot sub-bag_wf bag-member_wf fps-coeff_wf fps-compose_wf fps-restrict_wf power-series_wf crng_wf deq_wf valueall-type_wf istype-universe bag-member-parts' sub-bag-union-of-list hd_wf listp_properties hd_member list-cases null_nil_lemma reduce_tl_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma istype-void sub-bag-rep tl_wf reduce_hd_cons_lemma reduce_tl_cons_lemma length_of_cons_lemma reduce_cons_lemma equal_wf squash_wf true_wf istype-nat subtype_rel_self iff_weakening_equal bag-size-append l_all_wf2 not_wf equal-wf-T-base l_member_wf list_wf nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than le_witness_for_triv istype-false nil_wf colength-cons-not-zero colength_wf_list istype-le subtract-1-ge-0 intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf intformnot_wf itermSubtract_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_subtract_lemma int_term_value_add_lemma decidable__le le_wf cons_wf length-append add_nat_plus nat_plus_properties decidable__lt add-is-int-iff false_wf length_wf bag-size-zero empty-bag_wf l_all_cons bag-union_wf non_neg_length bag-append-assoc2 bag-append-ac bag-append-comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction sqequalRule sqequalHypSubstitution isect_memberEquality_alt isectElimination thin hypothesisEquality axiomSqleEquality hypothesis isectIsTypeImplies inhabitedIsType rename lambdaFormation_alt extract_by_obid setElimination independent_pairFormation because_Cache independent_functionElimination imageMemberEquality baseClosed imageElimination productElimination dependent_pairFormation_alt applyEquality independent_isectElimination lambdaEquality_alt universeIsType unionElimination equalityElimination dependent_functionElimination equalityTransitivity equalitySymmetry equalityIstype promote_hyp instantiate cumulativity voidElimination functionIsType universeEquality natural_numberEquality hypothesis_subsumption hyp_replacement applyLambdaEquality intEquality setIsType intWeakElimination approximateComputation int_eqEquality functionIsTypeImplies voidEquality dependent_set_memberEquality_alt baseApply closedConclusion sqequalBase pointwiseFunctionality productIsType addEquality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[g:PowerSeries(X;r)].    \mforall{}x:X.  fps-ucont(X;eq;r;f.f(x:=g))
supposing  valueall-type(X)

Date html generated: 2019_10_16-AM-11_36_06
Last ObjectModification: 2018_11_26-PM-03_09_19

Theory : power!series

Home Index