Step
*
2
1
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. S : ℤ List
15. ||S|| = (||v|| + 1) ∈ ℤ
16. x = S ⋅ [better-gcd(a;u) / v] ∈ ℤ
17. ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = ((||v|| + 1) + 1) ∈ ℤ) ∧ (x = S ⋅ [a; [u / v]] ∈ ℤ))
BY
{ (DVar `S' THEN All Reduce) }
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. 0 = (||v|| + 1) ∈ ℤ
15. x = 0 ∈ ℤ
16. ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = ((||v|| + 1) + 1) ∈ ℤ) ∧ (x = S ⋅ [a; [u / v]] ∈ ℤ))
2
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]] ∈ ℤ))
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. S : \mBbbZ{} List
15. ||S|| = (||v|| + 1)
16. x = S \mcdot{} [better-gcd(a;u) / v]
17. \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:
(DVar `S' THEN All Reduce)
Home
Index