---

Step * of Lemma int_add_grp_wf

<ℤ+> ∈ AbGrp
BY
{ Unfold `int_add_grp` 0 
THEN ((MemTypeCD) THENA Auto) }

1
<ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.(-x)> ∈ Group{i}

2
.....set predicate..... 
Comm(|<ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.(-x)>|;*)

---

Latex:

---

Latex:
<\mBbbZ{}+>  \mmember{}  AbGrp


By

---

Latex:
Unfold  `int\_add\_grp`  0 
THEN  ((MemTypeCD)  THENA  Auto)

---

Home Index