---

Step * of Lemma ml-gcd-sq

∀[y,x:ℤ].  (ml-gcd(x;y) ~ better-gcd(x;y))
BY
{ (Auto
   THEN (Assert ⌜∀d:ℕ. ∀y:ℤ.  (|y| < d ⇒ (∀x:ℤ. (ml-gcd(x;y) = better-gcd(x;y) ∈ ℤ)))⌝⋅
   THENM (InstHyp [⌜|y| + 1⌝;⌜y⌝;⌜x⌝] (-1)⋅ THEN Auto)
   )
   THEN RepeatFor 2 (Thin (-1))
   THEN InductionOnNat
   THEN Auto
   THEN ((Assert 0 ≤ |y| BY Auto) THEN Auto)
   THEN (RecCaseSplit `better-gcd` THENA Auto)
   THEN Unfold `ml-gcd` 0
   THEN (RW (AddrC [2] (LemmaC `ml_apply-sq`)) 0 THEN Auto)
   THEN RW (AddrC [2;1] (LemmaC `ml_apply-sq`)) 0
   THEN Auto
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0⋅
   THEN Fold `ml-gcd` 0
   THEN AutoSplit) }

1
1. d : ℤ
2. 0 < d
3. ∀y:ℤ. (|y| < d - 1 ⇒ (∀x:ℤ. (ml-gcd(x;y) = better-gcd(x;y) ∈ ℤ)))
4. y : ℤ
5. y ≠ 0
6. |y| < d
7. x : ℤ
8. 0 ≤ |y|
9. ¬(y = 0 ∈ ℤ)
⊢ ml-gcd(y;x rem y) = eval r = x rem y in better-gcd(y;r) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[y,x:\mBbbZ{}].    (ml-gcd(x;y)  \msim{}  better-gcd(x;y))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}y:\mBbbZ{}.    (|y|  <  d  {}\mRightarrow{}  (\mforall{}x:\mBbbZ{}.  (ml-gcd(x;y)  =  better-gcd(x;y))))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}|y|  +  1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  InductionOnNat
  THEN  Auto
  THEN  ((Assert  0  \mleq{}  |y|  BY  Auto)  THEN  Auto)
  THEN  (RecCaseSplit  `better-gcd`  THENA  Auto)
  THEN  Unfold  `ml-gcd`  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto)
  THEN  RW  (AddrC  [2;1]  (LemmaC  `ml\_apply-sq`))  0
  THEN  Auto
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0\mcdot{}
  THEN  Fold  `ml-gcd`  0
  THEN  AutoSplit)

---

Home Index