---

Step * of Lemma qeq-trans

Trans(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
BY
{ (D 0 THEN Auto THEN InstLemma `qeq-functionality` [⌜a⌝;⌜b⌝;⌜c⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(D  0  THEN  Auto  THEN  InstLemma  `qeq-functionality`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index