---

Step * 1 of Lemma oal_grp_wf


1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ <|oal(s;g)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.(--x)> ∈ AbDGrp
BY
{ ((RepeatM MemTypeCD) THENA Auto) 
THEN Force `5` (Reduce 0) }

1
1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ <|oal(s;g)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.(--x)> ∈ GrpSig

2
1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ IsMonoid(|oal(s;g)|;λx,y. (x ++ y);00)

3
1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ Inverse(|oal(s;g)|;λx,y. (x ++ y);00;λx.(--x))

4
1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ Comm(|oal(s;g)|;λx,y. (x ++ y))

5
1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ IsEqFun(|oal(s;g)|;=b)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  AbDGrp@i'
\mvdash{}  <|oal(s;g)|,  =\msubb{},  \mlambda{}x,y.  x  \mleq{}\mleq{}\msubb{}  y,  \mlambda{}x,y.  (x  ++  y),  00,  \mlambda{}x.(--x)>  \mmember{}  AbDGrp


By

---

Latex:
((RepeatM  MemTypeCD)  THENA  Auto) 
THEN  Force  `5`  (Reduce  0)

---

Home Index