Nuprl Lemma : polyalg_mo_wf

S:DSet. ∀A:CRng. ∀p:polynom_alg{i:l}(S;A).  (p.mo ∈ FAbMon(S))


Proof




Definitions occuring in Statement :  polyalg_mo: p.mo polynom_alg: polynom_alg{i:l}(S;A) free_abmonoid: FAbMon(S) all: x:A. B[x] member: t ∈ T crng: CRng dset: DSet
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T polynom_alg: polynom_alg{i:l}(S;A) polyalg_mo: p.mo pi1: fst(t)
Lemmas referenced :  polynom_alg_wf crng_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis lemma_by_obid dependent_functionElimination

Latex:
\mforall{}S:DSet.  \mforall{}A:CRng.  \mforall{}p:polynom\_alg\{i:l\}(S;A).    (p.mo  \mmember{}  FAbMon(S))



Date html generated: 2016_05_16-AM-08_14_33
Last ObjectModification: 2015_12_28-PM-06_09_13

Theory : polynom_1


Home Index