Step
*
2
1
2
2
2
of Lemma
gcd-list-property
1. u : ℤ
2. v : ℤ List
3. a : ℤ
4. x : ℤ
5. c : ℤ
6. (c * better-gcd(a;u)) = a ∈ ℤ
7. d : ℤ
8. (d * better-gcd(a;u)) = u ∈ ℤ
9. s : ℤ
10. t : ℤ
11. better-gcd(a;u) = ((s * a) + (t * u)) ∈ ℤ
12. R : ℤ List
13. [better-gcd(a;u) / v] = x * R ∈ (ℤ List)
14. u1 : ℤ
15. v1 : ℤ List
16. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
17. x = ((u1 * better-gcd(a;u)) + v1 ⋅ v) ∈ ℤ
18. ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = ((||v|| + 1) + 1) ∈ ℤ) ∧ (x = S ⋅ [a; [u / v]] ∈ ℤ))
BY
{ (D 0 With ⌜[u1 * s; [u1 * t / v1]]⌝  THEN Reduce 0 THEN Auto) }
1
1. u : ℤ
2. v : ℤ List
3. a : ℤ
4. x : ℤ
5. c : ℤ
6. (c * better-gcd(a;u)) = a ∈ ℤ
7. d : ℤ
8. (d * better-gcd(a;u)) = u ∈ ℤ
9. s : ℤ
10. t : ℤ
11. better-gcd(a;u) = ((s * a) + (t * u)) ∈ ℤ
12. R : ℤ List
13. [better-gcd(a;u) / v] = x * R ∈ (ℤ List)
14. u1 : ℤ
15. v1 : ℤ List
16. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
17. x = ((u1 * better-gcd(a;u)) + v1 ⋅ v) ∈ ℤ
18. ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
19. ((||v1|| + 1) + 1) = ((||v|| + 1) + 1) ∈ ℤ
⊢ x = (((u1 * s) * a) + ((u1 * t) * u) + v1 ⋅ v) ∈ ℤ
Latex:
Latex:
1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  a  :  \mBbbZ{}
4.  x  :  \mBbbZ{}
5.  c  :  \mBbbZ{}
6.  (c  *  better-gcd(a;u))  =  a
7.  d  :  \mBbbZ{}
8.  (d  *  better-gcd(a;u))  =  u
9.  s  :  \mBbbZ{}
10.  t  :  \mBbbZ{}
11.  better-gcd(a;u)  =  ((s  *  a)  +  (t  *  u))
12.  R  :  \mBbbZ{}  List
13.  [better-gcd(a;u)  /  v]  =  x  *  R
14.  u1  :  \mBbbZ{}
15.  v1  :  \mBbbZ{}  List
16.  (||v1||  +  1)  =  (||v||  +  1)
17.  x  =  ((u1  *  better-gcd(a;u))  +  v1  \mcdot{}  v)
18.  \mexists{}R:\mBbbZ{}  List.  ([a;  [u  /  v]]  =  x  *  R)
\mvdash{}  \mexists{}S:\mBbbZ{}  List.  ((||S||  =  ((||v||  +  1)  +  1))  \mwedge{}  (x  =  S  \mcdot{}  [a;  [u  /  v]]))
By
Latex:
(D  0  With  \mkleeneopen{}[u1  *  s;  [u1  *  t  /  v1]]\mkleeneclose{}    THEN  Reduce  0  THEN  Auto)
Home
Index