---

Step * 1 of Lemma int_add_grp_wf


<ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.(-x)> ∈ Group{i}
BY
{ ((BLemma `mk_grp`) THENA Auto) }

1
Assoc(ℤ;λx,y. (x + y))

2
Ident(ℤ;λx,y. (x + y);0)

3
Inverse(ℤ;λx,y. (x + y);0;λx.(-x))

---

Latex:

---

Latex:

<\mBbbZ{},  \mlambda{}x,y.  (x  =\msubz{}  y),  \mlambda{}x,y.  x  \mleq{}z  y,  \mlambda{}x,y.  (x  +  y),  0,  \mlambda{}x.(-x)>  \mmember{}  Group\{i\}


By

---

Latex:
((BLemma  `mk\_grp`)  THENA  Auto)

---

Home Index