---

Step * 1 3 of Lemma oal_grp_wf


1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ Inverse(|oal(s;g)|;λx,y. (x ++ y);00;λx.(--x))
BY
{ ((Force `5` (Eval ``inverse`` 0) 
THENM Backchain ``oal_neg_left_inv oal_neg_right_inv``) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Force  `5`  (Eval  ``inverse``  0) 
THENM  Backchain  ``oal\_neg\_left\_inv  oal\_neg\_right\_inv``)  THEN  Auto)

---

Home Index