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