---

Step * 4 of Lemma qrep_wf


1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
⊢ ((a5 * a3) = (a2 * a6) ∈ ℤ)
⇒ (let g,a,b = gcd_reduce(a5;a6) in 
   if 0 ≤z b then <a, b> else <-a, -b> fi 
   = let g,a,b = gcd_reduce(a2;a3) in 
     if 0 ≤z b then <a, b> else <-a, -b> fi 
   ∈ (ℤ × ℕ+))
BY
{ (TACTIC:(RenameVar `z3' 1 THEN RenameVar `z4' 2 THEN RenameVar `z1' 3 THEN RenameVar `z2' 4)
   THEN (InstLemma `gcd_reduce_property` [⌜z1⌝;⌜z2⌝]⋅ THENA Auto)
   THEN (MoveToConcl (-1))
   THEN (GenConclAtAddr [1;1] THENA Auto)
   THEN ((Thin (-1)) THEN RepeatFor 2 (D -1))
   THEN (InstLemma `gcd_reduce_property` [⌜z3⌝;⌜z4⌝]⋅ THENA Auto)
   THEN (MoveToConcl (-1))
   THEN (GenConclAtAddr [1;1] THENA Auto)
   THEN (Thin (-1))
   THEN RepeatFor 2 (D -1)
   THEN RepUR ``spreadn`` 0
   THEN Auto) }

1
1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
⊢ if 0 ≤z v8 then <v7, v8> else <-v7, -v8> fi  = if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  a5  :  \mBbbZ{}
2.  a6  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a2  :  \mBbbZ{}
4.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  ((a5  *  a3)  =  (a2  *  a6))
{}\mRightarrow{}  (let  g,a,b  =  gcd\_reduce(a5;a6)  in 
      if  0  \mleq{}z  b  then  <a,  b>  else  <-a,  -b>  fi 
      =  let  g,a,b  =  gcd\_reduce(a2;a3)  in 
          if  0  \mleq{}z  b  then  <a,  b>  else  <-a,  -b>  fi  )


By

---

Latex:
(TACTIC:(RenameVar  `z3'  1  THEN  RenameVar  `z4'  2  THEN  RenameVar  `z1'  3  THEN  RenameVar  `z2'  4)
  THEN  (InstLemma  `gcd\_reduce\_property`  [\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}z2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;1]  THENA  Auto)
  THEN  ((Thin  (-1))  THEN  RepeatFor  2  (D  -1))
  THEN  (InstLemma  `gcd\_reduce\_property`  [\mkleeneopen{}z3\mkleeneclose{};\mkleeneopen{}z4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;1]  THENA  Auto)
  THEN  (Thin  (-1))
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``spreadn``  0
  THEN  Auto)

---

Home Index