---

Step * 2 of Lemma qadd_grp_wf

.....set predicate..... 
Comm(|<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)>|;*)
BY
{ (RepUR ``comm`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
Comm(|<\mBbbQ{},  \mlambda{}x,y.  qeq(x;y),  \mlambda{}x,y.  q\_le(x;y),  \mlambda{}x,y.  (x  +  y),  0,  \mlambda{}x.-(x)>|;*)


By

---

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

---

Home Index