---

Step * 1 1 1 of Lemma oal_le_char


1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ ↑((x (=b) y) ∨b(x <<b y)) ⇐⇒ (x = y ∈ |oal(s;g)|) ∨ (x << y)
BY
{ ((Assert g ∈ AbDGrp BY (BLemma `ocgrp_abdgrp` THEN Auto)) THEN Auto) }

1
1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
5. g ∈ AbDGrp
6. ↑((x (=b) y) ∨b(x <<b y))
⊢ (x = y ∈ |oal(s;g)|) ∨ (x << y)

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  x  :  |oal(s;g)|
4.  y  :  |oal(s;g)|
\mvdash{}  \muparrow{}((x  (=\msubb{})  y)  \mvee{}\msubb{}(x  <<\msubb{}  y))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (x  <<  y)


By

---

Latex:
((Assert  g  \mmember{}  AbDGrp  BY  (BLemma  `ocgrp\_abdgrp`  THEN  Auto))  THEN  Auto)

---

Home Index