---

Step * 1 1 1 1 of Lemma equipollent-nat-rationals


1. L : (ℤ × ℕ+) List
2. 0 < ||[1 / map(λp.(snd(p));L)]||
3. 0 ≤ imax-list([1 / map(λp.(snd(p));L)])
⊢ ↑eval g = better-gcd(1;imax-list([1 / map(λp.(snd(p));L)]) + 1) in
   (g =z 1) ∨b(g =z -1)
BY
{ xxx((((RWO "better-gcd-gcd" 0 THENA Auto) THEN GenConclAtAddr [1;1;2]) THEN Auto) THEN All Thin)xxx }

1
1. v : ℤ
⊢ ↑eval g = gcd(1;v) in
   (g =z 1) ∨b(g =z -1)

---

Latex:

---

Latex:

1.  L  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  List
2.  0  <  ||[1  /  map(\mlambda{}p.(snd(p));L)]||
3.  0  \mleq{}  imax-list([1  /  map(\mlambda{}p.(snd(p));L)])
\mvdash{}  \muparrow{}eval  g  =  better-gcd(1;imax-list([1  /  map(\mlambda{}p.(snd(p));L)])  +  1)  in
      (g  =\msubz{}  1)  \mvee{}\msubb{}(g  =\msubz{}  -1)


By

---

Latex:
xxx((((RWO  "better-gcd-gcd"  0  THENA  Auto)  THEN  GenConclAtAddr  [1;1;2])  THEN  Auto)  THEN  All  Thin)xxx

---

Home Index