Nuprl Lemma : fps-pascal-elim

`∀[r:CRng]. ∀[x,y:Atom].  Δ(x,y)(x:=0) = (1÷(1-atom(y))) ∈ PowerSeries(r) supposing (¬(x = y ∈ Atom)) ∧ (¬(1 = 0 ∈ |r|))`

Proof

Definitions occuring in Statement :  fps-pascal: `Δ(x,y)` fps-elim-x: `f(x:=0)` fps-div: `(f÷g)` fps-sub: `(f-g)` fps-atom: `atom(x)` fps-one: `1` power-series: `PowerSeries(X;r)` atom-deq: `AtomDeq` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` 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` fps-pascal: `Δ(x,y)` fps-elim-x: `f(x:=0)` fps-atom: `atom(x)` squash: `↓T` prop: `ℙ` crng: `CRng` rng: `Rng` cand: `A c∧ B` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` true: `True` all: `∀x:A. B[x]` top: `Top` 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)` bnot: `¬bb` assert: `↑b` fps-sub: `(f-g)` empty-bag: `{}` fps-add: `(f+g)` fps-one: `1` fps-coeff: `f[b]` infix_ap: `x f y` single-bag: `{x}` fps-single: `<c>` fps-neg: `-(f)` bag-eq: `bag-eq(eq;as;bs)` bag-null: `bag-null(bs)` null: `null(as)` nil: `[]` 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` atom-deq: `AtomDeq` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  equal_wf squash_wf true_wf power-series_wf fps-elim-div atom-valueall-type atom-deq_wf fps-one_wf fps-sub_wf fps-add_wf fps-atom_wf rng_one_wf fps-div_wf iff_weakening_equal not_wf equal-wf-base atom_subtype_base rng_car_wf rng_zero_wf crng_wf fps-zero_wf atomdeq_reduce_lemma 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 fps-neg_wf fps-elim-x-one fps-elim-x-sub fps-elim-x-add fps-elim-x-atom neg_thru_op_fps abmonoid_ac_1_fps abmonoid_comm_fps fps-non-trivial rng_minus_wf rng_plus_wf infix_ap_wf rng_times_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_over_plus rng_minus_zero rng_plus_zero valueall-type_wf deq_wf neg_id_fps mon_ident_fps
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin applyEquality lambdaEquality imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality because_Cache independent_isectElimination atomEquality setElimination rename independent_pairFormation sqequalRule imageMemberEquality baseClosed independent_functionElimination productEquality isect_memberEquality axiomEquality natural_numberEquality dependent_functionElimination voidElimination voidEquality lambdaFormation unionElimination equalityElimination dependent_pairFormation promote_hyp instantiate cumulativity

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].    \mDelta{}(x,y)(x:=0)  =  (1\mdiv{}(1-atom(y)))  supposing  (\mneg{}(x  =  y))  \mwedge{}  (\mneg{}(1  =  0))

Date html generated: 2018_05_21-PM-10_12_00
Last ObjectModification: 2017_07_26-PM-06_34_51

Theory : power!series

Home Index