---

Step * 2 1 2 1 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. u1 : ℤ
13. v1 : ℤ List
14. [better-gcd(a;u) / v] = x * [u1 / v1] ∈ (ℤ List)
15. S : ℤ List
16. ||S|| = (||v|| + 1) ∈ ℤ
17. x = S ⋅ [better-gcd(a;u) / v] ∈ ℤ
⊢ ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
BY
{ (Unfold `int-vec-mul` -4 THEN Reduce (-4) THEN Fold `int-vec-mul` (-4)) }

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. u1 : ℤ
13. v1 : ℤ List
14. [better-gcd(a;u) / v] = [x * u1 / x * v1] ∈ (ℤ List)
15. S : ℤ List
16. ||S|| = (||v|| + 1) ∈ ℤ
17. x = S ⋅ [better-gcd(a;u) / v] ∈ ℤ
⊢ ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))

---

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.  u1  :  \mBbbZ{}
13.  v1  :  \mBbbZ{}  List
14.  [better-gcd(a;u)  /  v]  =  x  *  [u1  /  v1]
15.  S  :  \mBbbZ{}  List
16.  ||S||  =  (||v||  +  1)
17.  x  =  S  \mcdot{}  [better-gcd(a;u)  /  v]
\mvdash{}  \mexists{}R:\mBbbZ{}  List.  ([a;  [u  /  v]]  =  x  *  R)


By

---

Latex:
(Unfold  `int-vec-mul`  -4  THEN  Reduce  (-4)  THEN  Fold  `int-vec-mul`  (-4))

---

Home Index