---

Step * 1 2 1 of Lemma assert-is-qrep


1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
⊢ qrep(<p1, p2>) = <p1, p2> ∈ (ℤ × ℕ+)
BY
{ (RepUR ``qrep`` 0
   THEN (CallByValueReduce 0 THEN Auto)
   THEN All Reduce
   THEN (InstLemma `gcd_reduce_property` [⌜p1⌝;⌜p2⌝]⋅ THENA Auto))⋅ }

1
1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
4. let g,a,b = gcd_reduce(p1;p2) in 
(p1 = (a * g) ∈ ℤ) ∧ (p2 = (b * g) ∈ ℤ) ∧ CoPrime(a,b) ∧ ((p1 * b) = (a * p2) ∈ ℤ)
⊢ let g,a,b = gcd_reduce(p1;p2) in if 0 ≤z b then <a, b> else <-a, -b> fi  = <p1, p2> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  p1  :  \mBbbZ{}
2.  p2  :  \mBbbN{}\msupplus{}
3.  (gcd(p1;p2)  =  1)  \mvee{}  (gcd(p1;p2)  =  (-1))
\mvdash{}  qrep(<p1,  p2>)  =  <p1,  p2>


By

---

Latex:
(RepUR  ``qrep``  0
  THEN  (CallByValueReduce  0  THEN  Auto)
  THEN  All  Reduce
  THEN  (InstLemma  `gcd\_reduce\_property`  [\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index