### Nuprl Lemma : KozenSilva-lemma

`∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[n,m:ℕ].`
`  [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r) `
`  supposing (n ≤ m) ∧ (¬(x = y ∈ Atom))`

Proof

Definitions occuring in Statement :  fps-set-to-one: `[f]_n(y:=1)` fps-pascal: `Δ(x,y)` fps-compose: `g(x:=f)` fps-exp: `(f)^(n)` fps-slice: `[f]_n` fps-mul: `(f*g)` fps-add: `(f+g)` fps-atom: `atom(x)` power-series: `PowerSeries(X;r)` atom-deq: `AtomDeq` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` not: `¬A` and: `P ∧ Q` subtract: `n - m` atom: `Atom` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` prop: `ℙ` nat: `ℕ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` ge: `i ≥ j ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` cand: `A c∧ B` crng: `CRng` rng: `Rng` compose: `f o g` true: `True` squash: `↓T` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` dist_1op_2op_lr: `Dist1op2opLR(A;1op;2op)` infix_ap: `x f y` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` monoid_p: `IsMonoid(T;op;id)` assoc: `Assoc(T;op)` ident: `Ident(T;op;id)` comm: `Comm(T;op)` single-bag: `{x}` bag-filter: `[x∈b|p[x]]` int_seg: `{i..j-}` l_member!: `(x ∈! l)` le: `A ≤ B` lelt: `i ≤ j < k` less_than: `a < b` rev_uimplies: `rev_uimplies(P;Q)` l_all: `(∀x∈L.P[x])` fps-summation: `fps-summation(r;b;x.f[x])` fps-atom: `atom(x)` nequal: `a ≠ b ∈ T ` empty-bag: `{}` fps-add: `(f+g)` fps-coeff: `f[b]` fps-single: `<c>` bag-eq: `bag-eq(eq;as;bs)` bag-count: `(#x in bs)` bag-all: `bag-all(x.p[x];bs)` count: `count(P;L)` bag-map: `bag-map(f;bs)` bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` lt_int: `i <z j` band: `p ∧b q` fps-slice: `[f]_n` fps-mul: `(f*g)`
Lemmas referenced :  le_wf not_wf equal-wf-base atom_subtype_base nat_wf power-series_wf crng_wf fps-linear-ucont-equal atom-valueall-type atom-deq_wf fps-slice_wf fps-mul_wf fps-set-to-one_wf fps-pascal_wf fps-compose_wf fps-add_wf fps-atom_wf fps-exp_wf subtract_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_wf rng_car_wf bag_wf fps-ucont-composition fps-slice-ucont fps-mul-ucont fps-set-to-one-ucont fps-compose-ucont equal_wf fps-add-slice iff_weakening_equal squash_wf true_wf valueall-type_wf deq_wf fps-set-to-one-add mul_over_plus_fps mul_comm_fps fps-compose-add fps-set-to-one-scalar-mul fps-scalar-mul-slice fps-scalar-mul-property fps-scalar-mul_wf fps-compose-scalar-mul eq_int_wf bag-size_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int fps-set-to-one-single fps-single-slice fps-mul-slice fps-single_wf bag-co-restrict_wf fps-zero_wf mon_assoc_fps abmonoid_comm_fps mon_ident_fps bag-restrict-size-bound fps-summation_wf filter_is_singleton upto_wf subtype_rel_list int_seg_wf length_upto itermAdd_wf int_term_value_add_lemma decidable__lt intformless_wf intformeq_wf int_formula_prop_less_lemma int_formula_prop_eq_lemma select_upto non_neg_length length_wf_nat lelt_wf select_wf less_than_wf length_wf all_wf decidable__equal_int assert_wf int_seg_properties list-subtype-bag bag-summation-single fps-pascal-slice fps-compose-single rng_zero_wf reduce_nil_lemma reduce_cons_lemma map_nil_lemma map_cons_lemma rng_plus_zero fps-mul-assoc bag-restrict_wf fps-exp-add bag-summation-filter bag-summation_wf bag-summation-equal bag-member_wf ifthenelse_wf mul_zero_fps fps-zero-slice fps-compose-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis productEquality extract_by_obid isectElimination setElimination rename hypothesisEquality atomEquality applyEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry independent_isectElimination lambdaEquality dependent_set_memberEquality dependent_functionElimination natural_numberEquality unionElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll lambdaFormation independent_functionElimination imageElimination imageMemberEquality baseClosed universeEquality cumulativity equalityElimination promote_hyp instantiate independent_pairEquality hyp_replacement applyLambdaEquality addEquality functionEquality equalityUniverse levelHypothesis functionExtensionality

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[h:PowerSeries(r)].  \mforall{}[n,m:\mBbbN{}].
[([h]\_n(y:=1)*\mDelta{}(x,y))]\_m  =  ([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m  -  n))
supposing  (n  \mleq{}  m)  \mwedge{}  (\mneg{}(x  =  y))

Date html generated: 2018_05_21-PM-10_13_40
Last ObjectModification: 2017_07_26-PM-06_35_24

Theory : power!series

Home Index