---

Step * of Lemma ml-gcd-list-sq

∀[L:ℤ List+]. (ml-gcd-list(L) ~ gcd-list(L))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ℤ BY
               (UseWitness ⌜0⌝⋅ THEN Auto))
   THEN Unfolds ``ml-gcd-list gcd-list`` 0
   THEN RWO "ml-accumulate-sq" 0
   THEN Auto
   THEN Reduce 0
   THEN RWO "eager-accum-list_accum" 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List\msupplus{}].  (ml-gcd-list(L)  \msim{}  gcd-list(L))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mBbbZ{}  BY
                          (UseWitness  \mkleeneopen{}0\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfolds  ``ml-gcd-list  gcd-list``  0
  THEN  RWO  "ml-accumulate-sq"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  RWO  "eager-accum-list\_accum"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index