---

Step * 3 of Lemma qrep_wf


1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
⊢ ((a4 * a3) = a2 ∈ ℤ) ⇒ (<a4, 1> = let g,a,b = gcd_reduce(a2;a3) in if 0 ≤z b then <a, b> else <-a, -b> fi  ∈ (ℤ × ℕ+)\000C)
BY
{ TACTIC:((RenameVar `z' 1 THEN RenameVar `z1' 2 THEN RenameVar `z2' 3)
          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 RepUR ``spreadn`` 0
          THEN Auto) }

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

---

Latex:

---

Latex:

1.  a4  :  \mBbbZ{}
2.  a2  :  \mBbbZ{}
3.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  ((a4  *  a3)  =  a2)
{}\mRightarrow{}  (<a4,  1>  =  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  `z'  1  THEN  RenameVar  `z1'  2  THEN  RenameVar  `z2'  3)
                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  RepUR  ``spreadn``  0
                THEN  Auto)

---

Home Index