### Nuprl Lemma : KozenSilva-theorem

`∀[r:CRng]. ∀[x,y:Atom].`
`  ∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].`
`    (Moessner(r;x;y;h;d;k)`
`    = ([h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))`
`    ∈ PowerSeries(r)) `
`  supposing ¬(x = y ∈ Atom)`

Proof

Definitions occuring in Statement :  Moessner: `Moessner(r;x;y;h;d;k)` fps-compose: `g(x:=f)` fps-exp: `(f)^(n)` fps-scalar-mul: `(c)*f` fps-product: `Π(x∈b).f[x]` fps-slice: `[f]_n` fps-mul: `(f*g)` fps-add: `(f+g)` fps-atom: `atom(x)` power-series: `PowerSeries(X;r)` upto: `upto(n)` atom-deq: `AtomDeq` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` apply: `f a` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` atom: `Atom` equal: `s = t ∈ T` rng_nat_op: `n ⋅r e` crng: `CRng` rng_one: `1`
Definitions unfolded in proof :  Moessner: `Moessner(r;x;y;h;d;k)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` Moessner-aux: `Moessner-aux(r;x;y;h;d;k)` eq_int: `(i =z j)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` upto: `upto(n)` from-upto: `[n, m)` lt_int: `i <z j` bfalse: `ff` subtype_rel: `A ⊆r B` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` subtract: `n - m` sum: `Σ(f[x] | x < k)` sum_aux: `sum_aux(k;v;i;x.f[x])` nequal: `a ≠ b ∈ T ` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` bag-summation: `Σ(x∈b). f[x]` bag-product: `Πx ∈ b. f[x]` fps-product: `Π(x∈b).f[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` rng_zero: `0` add_grp_of_rng: `r↓+gp` pi2: `snd(t)` pi1: `fst(t)` grp_id: `e` ycomb: `Y` itop: `Π(op,id) lb ≤ i < ub. E[i]` nat_op: `n x(op;id) e` mon_nat_op: `n ⋅ e` rng_nat_op: `n ⋅r e` less_than': `less_than'(a;b)` le: `A ≤ B` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` squash: `↓T` true: `True` decidable: `Dec(P)` int_seg: `{i..j-}` lelt: `i ≤ j < k` crng: `CRng` rng: `Rng` istype: `istype(T)` nat_plus: `ℕ+` cand: `A c∧ B` atom-deq: `AtomDeq` empty-bag: `{}` fps-atom: `atom(x)` fps-add: `(f+g)` fps-coeff: `f[b]` single-bag: `{x}` 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)` band: `p ∧b q` infix_ap: `x f y` bag-append: `as + bs`
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation_alt natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination independent_pairFormation universeIsType axiomEquality functionIsTypeImplies inhabitedIsType unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination because_Cache equalityIsType4 baseClosed baseApply closedConclusion applyEquality promote_hyp instantiate cumulativity equalityIsType1 isectIsTypeImplies functionIsType atomEquality voidEquality isect_memberEquality lambdaFormation dependent_set_memberEquality functionExtensionality imageMemberEquality imageElimination lambdaEquality universeEquality dependent_set_memberEquality_alt applyLambdaEquality addEquality hyp_replacement intEquality dependent_pairFormation equalityIsType3 minusEquality multiplyEquality productIsType

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].
\mforall{}[h:PowerSeries(r)].  \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
(Moessner(r;x;y;h;d;k)
=  ([h]\_d  0(y:=((k  \mcdot{}r  1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k)).((((k  -  i)  \mcdot{}r  1)*atom(x)
+atom(y)))\^{}(d  (i  +  1))))
supposing  \mneg{}(x  =  y)

Date html generated: 2019_10_16-AM-11_36_49
Last ObjectModification: 2018_10_19-AM-00_13_17

Theory : power!series

Home Index