---

Step * 1 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)> ∈ GrpSig
BY
{ ((Unfold `grp_sig` 0) THEN Auto) }

---

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{}  GrpSig


By

---

Latex:
((Unfold  `grp\_sig`  0)  THEN  Auto)

---

Home Index