Nuprl Lemma : oal_fabmon_wf
∀s:LOSet. (oal_fabmon(s) ∈ FAbMon(s))
Proof
Definitions occuring in Statement :
oal_fabmon: oal_fabmon(s),
free_abmonoid: FAbMon(S),
all: ∀x:A. B[x],
member: t ∈ T,
loset: LOSet
Definitions unfolded in proof :
oal_fabmon: oal_fabmon(s),
all: ∀x:A. B[x],
member: t ∈ T,
loset: LOSet,
poset: POSet{i},
qoset: QOSet
Lemmas referenced :
fabmon_of_nat_mcp_wf,
oal_omcp_wf,
int_add_grp_wf2,
loset_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis
Latex:
\mforall{}s:LOSet. (oal\_fabmon(s) \mmember{} FAbMon(s))
Date html generated:
2016_05_16-AM-08_28_22
Last ObjectModification:
2015_12_28-PM-06_40_58
Theory : polynom_4
Home
Index