Nuprl Lemma : fps-compose-identity

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X].  (f(x:=atom(x)) = f ∈ PowerSeries(X;r)) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-compose: `g(x:=f)` fps-atom: `atom(x)` power-series: `PowerSeries(X;r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` cand: `A c∧ B` all: `∀x:A. B[x]` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` crng: `CRng` rng: `Rng` fps-compose: `g(x:=f)` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` fps-one: `1` fps-coeff: `f[b]` fps-single: `<c>` empty-bag: `{}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` cons-bag: `x.b` top: `Top` fps-atom: `atom(x)` deq: `EqDecider(T)` eqof: `eqof(d)` bag-eq: `bag-eq(eq;as;bs)` band: `p ∧b q` bag-all: `bag-all(x.p[x];bs)` bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` reduce: `reduce(f;k;as)` list_ind: list_ind bag-map: `bag-map(f;bs)` map: `map(f;as)` nil: `[]` single-bag: `{x}` cons: `[a / b]` lt_int: `i <z j` bag-count: `(#x in bs)` count: `count(P;L)` rng_zero: `0` pi1: `fst(t)` pi2: `snd(t)` fps-sub: `(f-g)`
Lemmas referenced :  fps-linear-ucont-equal fps-compose_wf fps-atom_wf power-series_wf fps-compose-ucont fps-id-ucont equal_wf squash_wf true_wf fps-compose-add fps-add_wf iff_weakening_equal fps-compose-scalar-mul fps-scalar-mul_wf rng_car_wf bag_wf crng_wf deq_wf valueall-type_wf bag_to_squash_list list_induction fps-single_wf list-subtype-bag list_wf fps-compose-one fps-one_wf fps-ext nil_wf bag-eq_wf empty-bag_wf bool_wf eqtt_to_assert assert-bag-eq bag-null_wf assert-bag-null rng_one_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base rng_zero_wf single-bag_wf cons-bag-as-append fps-mul-single fps-compose-mul fps-mul_wf safe-assert-deq fps-compose-atom-neq fps-compose-atom-eq fps-sub_wf fps-scalar-mul-zero neg_id_fps mon_ident_fps
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache independent_isectElimination hypothesis hypothesisEquality sqequalRule lambdaEquality cumulativity dependent_functionElimination independent_pairFormation lambdaFormation applyEquality imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination setElimination rename applyLambdaEquality functionExtensionality isect_memberEquality axiomEquality promote_hyp hyp_replacement voidEquality voidElimination unionElimination equalityElimination dependent_pairFormation instantiate equalityUniverse levelHypothesis

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

Date html generated: 2018_05_21-PM-10_11_49
Last ObjectModification: 2017_07_26-PM-06_34_46

Theory : power!series

Home Index