---

Step * 1 of Lemma oal_bpos_trichot


1. s : LOSet
2. g : OGrp
3. g ∈ AbDMon
4. g ∈ AbDGrp
5. rs : |oal(s;g)|
⊢ (↑pos(rs)) ∨ (rs = 00 ∈ |oal(s;g)|) ∨ (↑pos(--rs))
BY
{ ((Assert --rs ∈ |oal(s;g)| BY Auto) THEN RepUR ``oal_bpos band`` 0⋅ THEN RepeatFor 2 (AutoSplit)) }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDMon
4. g ∈ AbDGrp
5. rs : |oal(s;g)|
6. ¬(rs = 00 ∈ |oal(s;g)|)
7. --rs ∈ |oal(s;g)|
8. (--rs) = 00 ∈ |oal(s;g)|
⊢ (↑(e <b lv(rs)))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ False

2
1. s : LOSet
2. g : OGrp
3. g ∈ AbDMon
4. g ∈ AbDGrp
5. rs : |oal(s;g)|
6. ¬((--rs) = 00 ∈ |oal(s;g)|)
7. ¬(rs = 00 ∈ |oal(s;g)|)
8. --rs ∈ |oal(s;g)|
⊢ (↑(e <b lv(rs)))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ (↑(e <b lv(--rs)))

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  g  \mmember{}  AbDMon
4.  g  \mmember{}  AbDGrp
5.  rs  :  |oal(s;g)|
\mvdash{}  (\muparrow{}pos(rs))  \mvee{}  (rs  =  00)  \mvee{}  (\muparrow{}pos(--rs))


By

---

Latex:
((Assert  --rs  \mmember{}  |oal(s;g)|  BY  Auto)  THEN  RepUR  ``oal\_bpos  band``  0\mcdot{}  THEN  RepeatFor  2  (AutoSplit))

---

Home Index