---

Step * of Lemma oal_neg_wf2

∀a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (--ps ∈ |oal(a;b)|)
BY
{ (RepD 
THENM DVar `ps' 
THENM Force `8` (Reduce 0) 
THENM MemTypeCD) THEN Auto⋅ }

1
1. a : LOSet
2. b : AbDGrp
3. ps : |((a × (b↓set)) List)|
4. ↑sd_ordered(map(λx.(fst(x));ps))
5. ¬↑(e ∈b map(λx.(snd(x));ps))
6. ↑sd_ordered(map(λx.(fst(x));--ps))
⊢ ¬↑(e ∈b map(λx.(snd(x));--ps))

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDGrp.  \mforall{}ps:|oal(a;b)|.    (--ps  \mmember{}  |oal(a;b)|)


By

---

Latex:
(RepD 
THENM  DVar  `ps' 
THENM  Force  `8`  (Reduce  0) 
THENM  MemTypeCD)  THEN  Auto\mcdot{}

---

Home Index