### Nuprl Lemma : Pascal-completion-property

`∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x,y:Atom].`
`  ((Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r))`
`  ∧ (Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r))`
`  ∧ fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y)))`
`  ∧ (∀h:PowerSeries(r)`
`       (fps-Pascal(r;x;y;h)`
`       `` (h(x:=0) = f ∈ PowerSeries(r))`
`       `` (h(y:=0) = g ∈ PowerSeries(r))`
`       `` (h = Pascal-completion(r;f;g;x;y) ∈ PowerSeries(r)))) `
`  supposing (¬(1 = 0 ∈ |r|))`
`  ∧ (¬(x = y ∈ Atom))`
`  ∧ (f(x:=0) = f ∈ PowerSeries(r))`
`  ∧ (g(y:=0) = g ∈ PowerSeries(r))`
`  ∧ (f(y:=0) = g(x:=0) ∈ PowerSeries(r))`

Proof

Definitions occuring in Statement :  Pascal-completion: `Pascal-completion(r;f;g;x;y)` fps-Pascal: `fps-Pascal(r;x;y;f)` fps-elim-x: `f(x:=0)` power-series: `PowerSeries(X;r)` atom-deq: `AtomDeq` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` atom: `Atom` equal: `s = t ∈ T` crng: `CRng` rng_one: `1` rng_zero: `0` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` fps-Pascal: `fps-Pascal(r;x;y;f)` crng: `CRng` rng: `Rng` Pascal-completion: `Pascal-completion(r;f;g;x;y)` true: `True` atom-deq: `AtomDeq` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` fps-sub: `(f-g)` nequal: `a ≠ b ∈ T ` squash: `↓T` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` infix_ap: `x f y` empty-bag: `{}` fps-atom: `atom(x)` fps-neg: `-(f)` fps-one: `1` fps-add: `(f+g)` fps-coeff: `f[b]` single-bag: `{x}` fps-single: `<c>` bag-null: `bag-null(bs)` null: `null(as)` nil: `[]` 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)` top: `Top` lt_int: `i <z j` band: `p ∧b q`
Lemmas referenced :  equal_wf power-series_wf fps-elim-x_wf atom-deq_wf fps-Pascal_wf bag_wf not_wf rng_car_wf rng_one_wf rng_zero_wf equal-wf-base crng_wf atom-valueall-type fps-sub_wf fps-add_wf fps-mul_wf fps-one_wf fps-atom_wf fps-pascal_wf eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom neg_id_fps fps-neg_wf fps-pascal-elim iff_weakening_equal mon_ident_fps fps-div_wf squash_wf true_wf fps-elim-x-mul valueall-type_wf deq_wf fps-elim-x-sub fps-elim-x-add fps-elim-x-one fps-elim-x-atom fps-elim-x-elim-x mul_over_plus_fps mul_over_minus_fps mul_assoc_fps mul_one_fps mul_ac_1_fps mul_comm_fps mon_assoc_fps abmonoid_ac_1_fps abmonoid_comm_fps iabgrp_op_inv_assoc_fps fps-div-property rng_times_wf fps-coeff_wf empty-bag_wf rng_minus_wf rng_plus_wf infix_ap_wf reduce_nil_lemma reduce_cons_lemma map_nil_lemma map_cons_lemma rng_times_over_plus rng_times_over_minus rng_times_zero rng_times_one rng_minus_zero rng_plus_zero fps-pascal-symmetry fps-Pascal-iff Pascal-completion_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin independent_pairFormation hypothesis lambdaFormation extract_by_obid isectElimination atomEquality hypothesisEquality sqequalRule independent_pairEquality axiomEquality lambdaEquality dependent_functionElimination productEquality setElimination rename because_Cache isect_memberEquality equalityTransitivity equalitySymmetry independent_isectElimination natural_numberEquality unionElimination equalityElimination independent_functionElimination voidElimination dependent_pairFormation promote_hyp instantiate cumulativity applyEquality imageElimination imageMemberEquality baseClosed hyp_replacement applyLambdaEquality universeEquality equalityUniverse levelHypothesis voidEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(r)].  \mforall{}[x,y:Atom].
((Pascal-completion(r;f;g;x;y)(x:=0)  =  f)
\mwedge{}  (Pascal-completion(r;f;g;x;y)(y:=0)  =  g)
\mwedge{}  fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y)))
\mwedge{}  (\mforall{}h:PowerSeries(r)
(fps-Pascal(r;x;y;h)
{}\mRightarrow{}  (h(x:=0)  =  f)
{}\mRightarrow{}  (h(y:=0)  =  g)
{}\mRightarrow{}  (h  =  Pascal-completion(r;f;g;x;y))))
supposing  (\mneg{}(1  =  0))  \mwedge{}  (\mneg{}(x  =  y))  \mwedge{}  (f(x:=0)  =  f)  \mwedge{}  (g(y:=0)  =  g)  \mwedge{}  (f(y:=0)  =  g(x:=0))

Date html generated: 2018_05_21-PM-10_12_32
Last ObjectModification: 2017_07_26-PM-06_34_58

Theory : power!series

Home Index