---

Step * 2 of Lemma gcd-list-property


1. u : ℤ
2. v : ℤ List
3. [%1] : 0 < ||[u / v]||
⊢ (∃R:ℤ List. ([u / v] = gcd-list([u / v]) * R ∈ (ℤ List)))
∧ (∃S:ℤ List. ((||S|| = ||[u / v]|| ∈ ℤ) ∧ (gcd-list([u / v]) = S ⋅ [u / v] ∈ ℤ)))
BY
{ (Thin (-1)
   THEN (Assert valueall-type(ℤ) BY
               Auto)
   THEN (Unfold `gcd-list` 0 THEN ((RWO "eager-accum-list_accum" 0 THENM Reduce 0) THENA Auto))
   THEN Try (Hypothesis)
   THEN Thin (-1)) }

1
1. u : ℤ
2. v : ℤ List
⊢ (∃R:ℤ List
    ([u / v]
    = accumulate (with value a and list item b):
       better-gcd(a;b)
      over list:
        v
      with starting value:
       u) * R
    ∈ (ℤ List)))
∧ (∃S:ℤ List
    ((||S|| = (||v|| + 1) ∈ ℤ)
    ∧ (accumulate (with value a and list item b):
        better-gcd(a;b)
       over list:
         v
       with starting value:
        u)
      = S ⋅ [u / v]
      ∈ ℤ)))

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  [\%1]  :  0  <  ||[u  /  v]||
\mvdash{}  (\mexists{}R:\mBbbZ{}  List.  ([u  /  v]  =  gcd-list([u  /  v])  *  R))
\mwedge{}  (\mexists{}S:\mBbbZ{}  List.  ((||S||  =  ||[u  /  v]||)  \mwedge{}  (gcd-list([u  /  v])  =  S  \mcdot{}  [u  /  v])))


By

---

Latex:
(Thin  (-1)
  THEN  (Assert  valueall-type(\mBbbZ{})  BY
                          Auto)
  THEN  (Unfold  `gcd-list`  0  THEN  ((RWO  "eager-accum-list\_accum"  0  THENM  Reduce  0)  THENA  Auto))
  THEN  Try  (Hypothesis)
  THEN  Thin  (-1))

---

Home Index