Nuprl Lemma : fps-mul-coeff0
∀[eq:Top]. ∀[r:CRng]. ∀[f,g:Top]. ((f*g)[{}] ~ (f[{}] * g[{}]) +r 0)
Proof
Definitions occuring in Statement :
fps-mul: (f*g),
fps-coeff: f[b],
empty-bag: {},
uall: ∀[x:A]. B[x],
top: Top,
infix_ap: x f y,
sqequal: s ~ t,
crng: CRng,
rng_times: *,
rng_zero: 0,
rng_plus: +r
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
crng: CRng,
rng: Rng,
rng_sig: RngSig,
fps-coeff: f[b],
fps-mul: (f*g),
bag-summation: Σ(x∈b). f[x],
bag-accum: bag-accum(v,x.f[v; x];init;bs),
list_accum: list_accum,
bag-partitions: bag-partitions(eq;bs),
callbyvalueall: callbyvalueall,
evalall: evalall(t),
bag-splits: bag-splits(b),
list_ind: list_ind,
empty-bag: {},
nil: [],
it: ⋅,
single-bag: {x},
cons: [a / b],
bag-to-set: bag-to-set(eq;bs),
bag-remove-repeats: bag-remove-repeats(eq;bs),
list-to-set: list-to-set(eq;L),
l-union: as ⋃ bs,
reduce: reduce(f;k;as),
insert: insert(a;L),
eval_list: eval_list(t),
ifthenelse: if b then t else f fi ,
deq-member: x ∈b L,
bfalse: ff,
rng_plus: +r,
pi1: fst(t),
pi2: snd(t),
infix_ap: x f y,
rng_times: *
Lemmas referenced :
crng_properties,
rng_properties,
top_wf,
crng_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
setElimination,
rename,
productElimination,
sqequalRule,
sqequalAxiom,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[eq:Top]. \mforall{}[r:CRng]. \mforall{}[f,g:Top]. ((f*g)[\{\}] \msim{} (f[\{\}] * g[\{\}]) +r 0)
Date html generated:
2018_05_21-PM-09_54_56
Last ObjectModification:
2018_05_19-PM-04_13_13
Theory : power!series
Home
Index