---

Step * 1 of Lemma gcd-list-property


1. [%1] : 0 < ||[]||
⊢ (∃R:ℤ List. ([] = gcd-list([]) * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = ||[]|| ∈ ℤ) ∧ (gcd-list([]) = S ⋅ [] ∈ ℤ)))
BY
{ (Assert ⌜False⌝⋅ THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  All  Reduce  THEN  Auto)

---

Home Index