### Nuprl Lemma : fps-pascal-slice

`∀[r:CRng]. ∀[x,y:Atom]. ∀[n:ℕ].  ([Δ(x,y)]_n = ((<{x}>+<{y}>))^(n) ∈ PowerSeries(r))`

Proof

Definitions occuring in Statement :  fps-pascal: `Δ(x,y)` fps-exp: `(f)^(n)` fps-slice: `[f]_n` fps-add: `(f+g)` fps-single: `<c>` power-series: `PowerSeries(X;r)` single-bag: `{x}` atom-deq: `AtomDeq` nat: `ℕ` uall: `∀[x:A]. B[x]` atom: `Atom` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` prop: `ℙ` nat: `ℕ` crng: `CRng` rng: `Rng` fps-pascal: `Δ(x,y)` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` eq_int: `(i =z j)` bag-size: `#(bs)` length: `||as||` list_ind: list_ind single-bag: `{x}` cons: `[a / b]` nil: `[]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  fps-geometric-slice1 atom-valueall-type atom-deq_wf fps-add_wf fps-single_wf single-bag_wf equal_wf power-series_wf fps-slice_wf fps-div_wf rng_one_wf fps-one_wf fps-sub_wf fps-exp_wf nat_wf crng_wf eq_int_wf bag-size_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int fps-zero_wf ite_rw_true iff_weakening_equal squash_wf true_wf fps-add-slice fps-single-slice
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache independent_isectElimination hypothesis hypothesisEquality atomEquality dependent_functionElimination equalitySymmetry hyp_replacement applyLambdaEquality setElimination rename sqequalRule isect_memberEquality axiomEquality natural_numberEquality applyEquality lambdaEquality imageElimination lambdaFormation unionElimination equalityElimination productElimination equalityTransitivity dependent_pairFormation promote_hyp instantiate cumulativity independent_functionElimination voidElimination imageMemberEquality baseClosed universeEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[n:\mBbbN{}].    ([\mDelta{}(x,y)]\_n  =  ((<\{x\}>+<\{y\}>))\^{}(n))

Date html generated: 2018_05_21-PM-10_11_53
Last ObjectModification: 2017_07_26-PM-06_34_49

Theory : power!series

Home Index