---

Step * of Lemma gcd_reduce_wf

∀[p,q:ℤ].  (gcd_reduce(p;q) ∈ ℕ × ℤ × ℤ)
BY
{ xxx(xxxAutoxxx
      THEN Unfold `gcd_reduce` 0
      THEN xxx((GenConclAtAddr [2;1] THENA Auto) THEN RepUR ``spreadn`` 0 THEN Auto)xxx)xxx }

---

Latex:

---

Latex:
\mforall{}[p,q:\mBbbZ{}].    (gcd\_reduce(p;q)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbZ{})


By

---

Latex:
xxx(xxxAutoxxx
        THEN  Unfold  `gcd\_reduce`  0
        THEN  xxx((GenConclAtAddr  [2;1]  THENA  Auto)  THEN  RepUR  ``spreadn``  0  THEN  Auto)xxx)xxx

---

Home Index