---

Step * of Lemma qeq_wf

∀[r,s:ℤ ⋃ (ℤ × ℤ-o)].  (qeq(r;s) ∈ 𝔹)
BY
{ (Auto
   THEN D_b_union 1
   THEN D_b_union 2
   THEN xxx(Unfold `qeq` 0
            THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
            THEN Reduce 0
            THEN Auto
            THEN DProdsAndUnions
            THEN All Reduce
            THEN Auto)xxx) }

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].    (qeq(r;s)  \mmember{}  \mBbbB{})


By

---

Latex:
(Auto
  THEN  D\_b\_union  1
  THEN  D\_b\_union  2
  THEN  xxx(Unfold  `qeq`  0
                    THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                    THEN  Reduce  0
                    THEN  Auto
                    THEN  DProdsAndUnions
                    THEN  All  Reduce
                    THEN  Auto)xxx)

---

Home Index