---

Step * 2 of Lemma int_add_grp_wf

.....set predicate..... 
Comm(|<ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.(-x)>|;*)
BY
{ ((AbEval ``comm`` 0) THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
Comm(|<\mBbbZ{},  \mlambda{}x,y.  (x  =\msubz{}  y),  \mlambda{}x,y.  x  \mleq{}z  y,  \mlambda{}x,y.  (x  +  y),  0,  \mlambda{}x.(-x)>|;*)


By

---

Latex:
((AbEval  ``comm``  0)  THEN  Auto)

---

Home Index