Nuprl Lemma : oal_polyalg_wf
∀s:LOSet. ∀a:CDRng. (oal_polyalg(s;a) ∈ polynom_alg{i:l}(s;a))
Proof
Definitions occuring in Statement :
oal_polyalg: oal_polyalg(s;a),
polynom_alg: polynom_alg{i:l}(S;A),
all: ∀x:A. B[x],
member: t ∈ T,
cdrng: CDRng,
loset: LOSet
Definitions unfolded in proof :
oal_polyalg: oal_polyalg(s;a),
polynom_alg: polynom_alg{i:l}(S;A),
all: ∀x:A. B[x],
member: t ∈ T,
loset: LOSet,
poset: POSet{i},
qoset: QOSet,
cdrng: CDRng,
oal_fabmon: oal_fabmon(s),
fabmon_of_nat_mcp: fabmon_of_nat_mcp(m),
free_abmon_mon: f.mon,
pi1: fst(t),
oal_omcp: oal_omcp{s,g},
mcopower_mon: m.mon
Lemmas referenced :
cdrng_wf,
loset_wf,
fmonalg_wf,
free_abmon_mon_wf,
oal_fabmon_wf,
omral_fma_wf2,
oal_hgp_wf2,
int_add_grp_wf2
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
sqequalHypSubstitution,
hypothesis,
lemma_by_obid,
dependent_pairEquality,
dependent_functionElimination,
thin,
setElimination,
rename,
hypothesisEquality
Latex:
\mforall{}s:LOSet. \mforall{}a:CDRng. (oal\_polyalg(s;a) \mmember{} polynom\_alg\{i:l\}(s;a))
Date html generated:
2016_05_16-AM-08_28_26
Last ObjectModification:
2015_12_28-PM-06_41_00
Theory : polynom_4
Home
Index