### Nuprl Lemma : fps-Pascal-iff

`∀[r:CRng]. ∀[x,y:Atom]. ∀[f:PowerSeries(r)].`
`  fps-Pascal(r;x;y;f) `⇐⇒` f = (((((1-atom(y))*f(x:=0))+((1-atom(x))*f(y:=0)))-f(x:=0)(y:=0))*Δ(x,y)) ∈ PowerSeries(r) `
`  supposing ¬(x = y ∈ Atom)`

Proof

Definitions occuring in Statement :  fps-pascal: `Δ(x,y)` fps-Pascal: `fps-Pascal(r;x;y;f)` fps-elim-x: `f(x:=0)` fps-mul: `(f*g)` fps-sub: `(f-g)` fps-add: `(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]` iff: `P `⇐⇒` Q` not: `¬A` atom: `Atom` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` fps-atom: `atom(x)` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` rev_implies: `P `` Q` fps-Pascal: `fps-Pascal(r;x;y;f)` all: `∀x:A. B[x]` not: `¬A` false: `False` true: `True` subtype_rel: `A ⊆r B` so_apply: `x[s]` infix_ap: `x f y` rng: `Rng` crng: `CRng` so_lambda: `λ2x.t[x]` prop: `ℙ` power-series: `PowerSeries(X;r)` fps-elim: `fps-elim(x)` fps-add: `(f+g)` fps-sub: `(f-g)` fps-neg: `-(f)` fps-coeff: `f[b]` fps-elim-x: `f(x:=0)` squash: `↓T` guard: `{T}` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` or: `P ∨ Q` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` it: `⋅` unit: `Unit` bool: `𝔹` bfalse: `ff` btrue: `tt` ifthenelse: `if b then t else f fi ` isl: `isl(x)` top: `Top` ringeq_int_terms: `t1 ≡ t2` sq_or: `a ↓∨ b` nequal: `a ≠ b ∈ T ` bor: `p ∨bq` deq-member: `x ∈b L` so_apply: `x[s1;s2;s3]` so_lambda: so_lambda3 append: `as @ bs` bag-deq-member: `bag-deq-member(eq;x;b)` atom-deq: `AtomDeq` bag-append: `as + bs` single-bag: `{x}` fps-pascal: `Δ(x,y)` empty-bag: `{}` fps-single: `<c>` fps-one: `1` bag-eq: `bag-eq(eq;as;bs)` bag-count: `(#x in bs)` bag-all: `bag-all(x.p[x];bs)` bag-null: `bag-null(bs)` null: `null(as)` nil: `[]` 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`
Lemmas referenced :  istype-void power-series_wf istype-atom crng_wf fps-one_wf fps-single_wf atom-valueall-type fps-neg_wf fps-add_wf unit_wf2 bag-diff_wf fps-mul_wf fps-sub_wf fps-elim-x_wf fps-Pascal_wf rng_zero_wf atom-deq_wf bag-deq-member_wf ifthenelse_wf rng_minus_wf rng_plus_wf single-bag_wf bag-append_wf rng_car_wf equal_wf bag_wf all_wf squash_wf true_wf abmonoid_ac_1_fps subtype_rel_self iff_weakening_equal abmonoid_comm_fps mon_assoc_fps neg_thru_op_fps mul_comm_fps mul_one_fps mul_over_plus_fps mul_over_minus_fps fps-mul-single-general fps-mul-comm bag-member_wf assert_wf not_functionality_wrt_uiff assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert assert-bag-deq-member eqtt_to_assert bool_wf not_wf bag-diff-property bag-deq-member-bag-diff rng_minus_zero rng_plus_ac_1 rng_plus_comm rng_plus_zero rng_plus_inv_assoc bag-member-iff and_wf bag-append-comm bag-append-assoc bag-append-cancel ringeq-iff-rsub-is-0 itermConstant_wf itermMinus_wf itermVar_wf itermAdd_wf ring_polynomial_null int-to-ring_wf ring_term_value_add_lemma ring_term_value_var_lemma ring_term_value_minus_lemma ring_term_value_const_lemma int-to-ring-zero bag-member-single bag-member-append assert_of_bor iff_weakening_uiff iff_transitivity equal-wf-base or_wf iff_functionality_wrt_iff btrue_wf bfalse_wf bor_wf reduce_wf iff_imp_equal_bool neg_assert_of_eq_atom assert_of_eq_atom eq_atom_wf deq_member_cons_lemma list_ind_nil_lemma list_ind_cons_lemma bag-diff-equal-inl bag-append-assoc2 rng_plus_assoc rng_plus_inv fps-pascal_wf fps-div_wf rng_one_wf valueall-type_wf deq_wf istype-universe mul_ac_1_fps fps-div-property rng_times_wf fps-coeff_wf empty-bag_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 fps-mul-assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality_alt dependent_functionElimination hypothesisEquality axiomEquality hypothesis functionIsTypeImplies inhabitedIsType functionIsType equalityIstype extract_by_obid isect_memberEquality_alt isectElimination isectIsTypeImplies universeIsType atomEquality natural_numberEquality universeEquality unionEquality independent_isectElimination instantiate cumulativity unionElimination independent_functionElimination equalitySymmetry equalityTransitivity functionEquality applyEquality because_Cache rename setElimination lambdaEquality lambdaFormation independent_pairFormation imageElimination imageMemberEquality baseClosed voidElimination promote_hyp dependent_pairFormation equalityElimination applyLambdaEquality hyp_replacement dependent_set_memberEquality voidEquality isect_memberEquality approximateComputation int_eqEquality intEquality inlFormation inrFormation closedConclusion lambdaFormation_alt productIsType Error :memTop

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[f:PowerSeries(r)].
fps-Pascal(r;x;y;f)
\mLeftarrow{}{}\mRightarrow{}  f  =  (((((1-atom(y))*f(x:=0))+((1-atom(x))*f(y:=0)))-f(x:=0)(y:=0))*\mDelta{}(x,y))
supposing  \mneg{}(x  =  y)

Date html generated: 2020_05_20-AM-09_07_14
Last ObjectModification: 2019_12_31-PM-09_47_22

Theory : power!series

Home Index