Nuprl Lemma : KozenSilva-corollary1

[x,y:Atom].
∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
(Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then else (i 1) fi ;k)
= Π(i∈upto(k)).(((k i)*atom(x)+atom(y)))^(d i)
∈ PowerSeries(ℤ-rng))
supposing ¬(x y ∈ Atom)

Proof

Definitions occuring in Statement :  Moessner: Moessner(r;x;y;h;d;k) fps-exp: (f)^(n) fps-scalar-mul: (c)*f fps-product: Π(x∈b).f[x] fps-add: (f+g) fps-atom: atom(x) fps-one: 1 power-series: PowerSeries(X;r) upto: upto(n) atom-deq: AtomDeq nat: ifthenelse: if then else fi  eq_int: (i =z j) uimplies: supposing a uall: [x:A]. B[x] not: ¬A apply: a lambda: λx.A[x] function: x:A ⟶ B[x] subtract: m natural_number: \$n atom: Atom equal: t ∈ T int_ring: -rng
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a squash: T prop: nat: subtype_rel: A ⊆B all: x:A. B[x] implies:  Q integ_dom: IntegDom{i} so_lambda: λ2x.t[x] int_seg: {i..j-} int_ring: -rng rng_car: |r| pi1: fst(t) le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A so_apply: x[s] true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q ge: i ≥  lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top crng: CRng rng: Rng subtract: m rng_one: 1 pi2: snd(t) so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  equal_wf squash_wf true_wf upto_wf list-subtype-bag int_seg_wf subtype_rel_self bag_wf power-series_wf int_ring_wf integ_dom_wf KozenSilva-corollary0 fps-product_wf atom-valueall-type atom-deq_wf fps-exp_wf fps-add_wf fps-scalar-mul_wf subtract_wf fps-atom_wf nat_wf int_seg_subtype_nat false_wf iff_weakening_equal rng_nat_op-int int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_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_less_lemma int_formula_prop_wf le_wf rng_one_wf rng_car_wf not_wf equal-wf-base atom_subtype_base lifting-strict-spread strict4-spread decidable__equal_int intformeq_wf itermMultiply_wf itermAdd_wf itermMinus_wf int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_add_lemma int_term_value_minus_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality setElimination rename natural_numberEquality because_Cache independent_isectElimination sqequalRule lambdaFormation dependent_functionElimination independent_functionElimination atomEquality intEquality functionExtensionality independent_pairFormation imageMemberEquality baseClosed productElimination dependent_set_memberEquality unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll axiomEquality functionEquality

Latex:
\mforall{}[x,y:Atom].
\mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
(Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  d  (i  -  1)  fi  ;k)
=  \mPi{}(i\mmember{}upto(k)).(((k  -  i)*atom(x)+atom(y)))\^{}(d  i))
supposing  \mneg{}(x  =  y)

Date html generated: 2018_05_21-PM-10_14_22
Last ObjectModification: 2017_07_26-PM-06_35_34

Theory : power!series

Home Index