Nuprl Lemma : oal_cons_pr_wf
∀a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.
((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |b|)) ⇒ (oal_cons_pr(x;y;ws) ∈ |oal(a;b)|))
Proof
Definitions occuring in Statement :
oal_cons_pr: oal_cons_pr(x;y;ws),
oalist: oal(a;b),
before: before(u;ps),
map: map(f;as),
assert: ↑b,
pi1: fst(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
member: t ∈ T,
lambda: λx.A[x],
equal: s = t ∈ T,
abdmonoid: AbDMon,
grp_id: e,
grp_car: |g|,
loset: LOSet,
set_car: |p|
Definitions unfolded in proof :
oal_cons_pr: oal_cons_pr(x;y;ws)
Lemmas referenced :
cons_in_oalist
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}a:LOSet. \mforall{}b:AbDMon. \mforall{}ws:|oal(a;b)|. \mforall{}x:|a|. \mforall{}y:|b|.
((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws))) {}\mRightarrow{} (\mneg{}(y = e)) {}\mRightarrow{} (oal\_cons\_pr(x;y;ws) \mmember{} |oal(a;b)|))
Date html generated:
2016_05_16-AM-08_15_53
Last ObjectModification:
2015_12_28-PM-06_28_36
Theory : polynom_2
Home
Index