---

Step * 1 2 of Lemma oal_grp_wf


1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ IsMonoid(|oal(s;g)|;λx,y. (x ++ y);00)
BY
{ ((AGenRepD ["compound";"basic"] 
THENM Force `5` (Reduce 0) 
THENM Backchain ``oal_merge_assoc oal_nil_ident_l oal_nil_ident_r``) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  AbDGrp@i'
\mvdash{}  IsMonoid(|oal(s;g)|;\mlambda{}x,y.  (x  ++  y);00)


By

---

Latex:
((AGenRepD  ["compound";"basic"] 
THENM  Force  `5`  (Reduce  0) 
THENM  Backchain  ``oal\_merge\_assoc  oal\_nil\_ident\_l  oal\_nil\_ident\_r``)  THEN  Auto)

---

Home Index