---

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


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> ∈ (ℤ × ℕ+)
BY
{ (MoveToConcl (-1) THEN GenConclAtAddr [1;1] THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN Auto) }

1
1. p1 : ℤ
2. p2 : ℕ+
3. (gcd(p1;p2) = 1 ∈ ℤ) ∨ (gcd(p1;p2) = (-1) ∈ ℤ)
4. v1 : ℕ
5. v3 : ℤ
6. v4 : ℤ
7. gcd_reduce(p1;p2) = <v1, v3, v4> ∈ (ℕ × ℤ × ℤ)
8. p1 = (v3 * v1) ∈ ℤ
9. p2 = (v4 * v1) ∈ ℤ
10. CoPrime(v3,v4)
11. (p1 * v4) = (v3 * p2) ∈ ℤ
⊢ if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  = <p1, p2> ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  p1  :  \mBbbZ{}
2.  p2  :  \mBbbN{}\msupplus{}
3.  (gcd(p1;p2)  =  1)  \mvee{}  (gcd(p1;p2)  =  (-1))
4.  let  g,a,b  =  gcd\_reduce(p1;p2)  in 
(p1  =  (a  *  g))  \mwedge{}  (p2  =  (b  *  g))  \mwedge{}  CoPrime(a,b)  \mwedge{}  ((p1  *  b)  =  (a  *  p2))
\mvdash{}  let  g,a,b  =  gcd\_reduce(p1;p2)  in  if  0  \mleq{}z  b  then  <a,  b>  else  <-a,  -b>  fi    =  <p1,  p2>


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;1]  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  0  THEN  Auto)

---

Home Index