---

Step * 1 2 of Lemma assert-is-qrep


1. p : ℤ × ℕ+
2. ↑is-qrep(p)
⊢ qrep(p) = p ∈ (ℤ × ℕ+)
BY
{ xxx(D 1
      THEN RepUR ``is-qrep`` (-1)
      THEN (CallByValueReduce (-1) THENA Auto)
      THEN (RWO "better-gcd-gcd" (-1) THENA Auto)
      THEN (RW assert_pushdownC (-1) THENA Auto))xxx }

1
1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
⊢ qrep(<p1, p2>) = <p1, p2> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  \muparrow{}is-qrep(p)
\mvdash{}  qrep(p)  =  p


By

---

Latex:
xxx(D  1
        THEN  RepUR  ``is-qrep``  (-1)
        THEN  (CallByValueReduce  (-1)  THENA  Auto)
        THEN  (RWO  "better-gcd-gcd"  (-1)  THENA  Auto)
        THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))xxx

---

Home Index