---

Step * 1 of Lemma qadd_grp_wf


<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)> ∈ Group{i}
BY
{ TACTIC:(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:

<\mBbbQ{},  \mlambda{}x,y.  qeq(x;y),  \mlambda{}x,y.  q\_le(x;y),  \mlambda{}x,y.  (x  +  y),  0,  \mlambda{}x.-(x)>  \mmember{}  Group\{i\}


By

---

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

---

Home Index