---

Step * 1 2 3 of Lemma qadd_grp_wf2


Cancel(ℚ;ℚ;λx,y. (x + y))
BY
{ ((RepUR ``cancel`` 0 THEN Auto) THEN (ApFunToHypEquands `z'  ⌜-(w) + z⌝ ⌜ℚ⌝ (-1))⋅ THEN (QAddReduce (-1)) THEN Auto) }

---

Latex:

---

Latex:

Cancel(\mBbbQ{};\mBbbQ{};\mlambda{}x,y.  (x  +  y))


By

---

Latex:
((RepUR  ``cancel``  0  THEN  Auto)
  THEN  (ApFunToHypEquands  `z'    \mkleeneopen{}-(w)  +  z\mkleeneclose{}  \mkleeneopen{}\mBbbQ{}\mkleeneclose{}  (-1))\mcdot{}
  THEN  (QAddReduce  (-1))
  THEN  Auto)

---

Home Index