---

Step * 1 2 1 of Lemma oal_bpos_trichot


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 < lv(rs))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ (e < (~ lv(rs)))
BY
{ ((InstLemma `grp_lt_trichot` [g;e;lv(rs)] 
THENM GenExRepD) THENA Auto)⋅ }

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 = 00 ∈ |oal(s;g)|)
8. --rs ∈ |oal(s;g)|
9. e < lv(rs)
⊢ (e < lv(rs))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ (e < (~ lv(rs)))

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)|
9. e = lv(rs) ∈ |g|
⊢ (e < lv(rs))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ (e < (~ lv(rs)))

3
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)|
9. lv(rs) < e
⊢ (e < lv(rs))
∨ (rs = 00 ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
∨ (e < (~ lv(rs)))

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  g  \mmember{}  AbDMon
4.  g  \mmember{}  AbDGrp
5.  rs  :  |oal(s;g)|
6.  \mneg{}((--rs)  =  00)
7.  \mneg{}(rs  =  00)
8.  --rs  \mmember{}  |oal(s;g)|
\mvdash{}  (e  <  lv(rs))  \mvee{}  (rs  =  00)  \mvee{}  (e  <  (\msim{}  lv(rs)))


By

---

Latex:
((InstLemma  `grp\_lt\_trichot`  [g;e;lv(rs)] 
THENM  GenExRepD)  THENA  Auto)\mcdot{}

---

Home Index