---

Step * of Lemma qeq-sym

Sym(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
BY
{ (D 0
   THEN Auto
   THEN All (Unfold `qeq`)⋅
   THEN RepeatFor 2 ((All CallByValueReduce⋅ THENA Auto))
   THEN All D_rational_form
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
Sym(\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{});r,s.qeq(r;s)  =  tt)


By

---

Latex:
(D  0
  THEN  Auto
  THEN  All  (Unfold  `qeq`)\mcdot{}
  THEN  RepeatFor  2  ((All  CallByValueReduce\mcdot{}  THENA  Auto))
  THEN  All  D\_rational\_form
  THEN  All  Reduce
  THEN  Auto)

---

Home Index