Step
*
1
1
1
1
1
2
of Lemma
omega_step_measure
1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
4. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
5. ¬(n = 0 ∈ ℤ)
6. first-success(λL.find-exact-eq-constraint(L);[u / v]) ∈ i:ℕ||[u / v]||
× x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
× {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?
7. i : ℕ||[u / v]||
8. x : {x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);[u / v])
= (inl <i, x, x2>)
∈ (i:ℕ||[u / v]|| × x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)} × {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?)
11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
12. exact-reduce-constraints(x;x2;[u / v]) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
13. x3 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
14. gcd-reduce-eq-constraints([];xx) = (inl x3) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
15. yy : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
16. exact-reduce-constraints(x;x2;ineqs) = yy ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
17. x4 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
18. gcd-reduce-ineq-constraints([];yy) = (inl x4) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
⊢ 0 < ||u|| - 1
⇒ (¬if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)|| - 1 < ||u|| - 1)
⇒ (¬((if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)|| - 1 = (||u|| - 1) ∈ ℤ)
∧ ||x3|| < ||v|| + 1))
⇒ False
BY
{ TACTIC:(DVar `x3' THEN Reduce 0) }
1
1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
4. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
5. ¬(n = 0 ∈ ℤ)
6. first-success(λL.find-exact-eq-constraint(L);[u / v]) ∈ i:ℕ||[u / v]||
× x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
× {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?
7. i : ℕ||[u / v]||
8. x : {x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);[u / v])
= (inl <i, x, x2>)
∈ (i:ℕ||[u / v]|| × x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)} × {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?)
11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
12. exact-reduce-constraints(x;x2;[u / v]) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
13. gcd-reduce-eq-constraints([];xx) = (inl []) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
14. yy : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
15. exact-reduce-constraints(x;x2;ineqs) = yy ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
16. x4 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
17. gcd-reduce-ineq-constraints([];yy) = (inl x4) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
⊢ 0 < ||u|| - 1
⇒ (¬if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 < ||u|| - 1)
⇒ (¬((if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 = (||u|| - 1) ∈ ℤ) ∧ 0 < ||v|| + 1))
⇒ False
2
1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
4. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
5. ¬(n = 0 ∈ ℤ)
6. first-success(λL.find-exact-eq-constraint(L);[u / v]) ∈ i:ℕ||[u / v]||
× x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
× {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?
7. i : ℕ||[u / v]||
8. x : {x:ℤ List| x = [u / v][i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);[u / v])
= (inl <i, x, x2>)
∈ (i:ℕ||[u / v]|| × x:{x:ℤ List| x = [u / v][i] ∈ (ℤ List)} × {i@0:ℕ+||[u / v][i]||| |[u / v][i][i@0]| = 1 ∈ ℤ} ?)
11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
12. exact-reduce-constraints(x;x2;[u / v]) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
13. u1 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ}
14. v1 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
15. gcd-reduce-eq-constraints([];xx) = (inl [u1 / v1]) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
16. yy : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
17. exact-reduce-constraints(x;x2;ineqs) = yy ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
18. x4 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
19. gcd-reduce-ineq-constraints([];yy) = (inl x4) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
⊢ 0 < ||u|| - 1 ⇒ (¬||u1|| - 1 < ||u|| - 1) ⇒ (¬(((||u1|| - 1) = (||u|| - 1) ∈ ℤ) ∧ ||v1|| + 1 < ||v|| + 1)) ⇒ False
Latex:
Latex:
1. n : \mBbbN{}
2. u : \{L:\mBbbZ{} List| ||L|| = (n + 1)\}
3. v : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
4. ineqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
5. \mneg{}(n = 0)
6. first-success(\mlambda{}L.find-exact-eq-constraint(L);[u / v]) \mmember{} i:\mBbbN{}||[u / v]||
\mtimes{} x:\{x:\mBbbZ{} List| x = [u / v][i]\}
\mtimes{} \{i@0:\mBbbN{}\msupplus{}||[u / v][i]||| |[u / v][i][i@0]| = 1\} ?
7. i : \mBbbN{}||[u / v]||
8. x : \{x:\mBbbZ{} List| x = [u / v][i]\}
9. x2 : \{i@0:\mBbbN{}\msupplus{}||[u / v][i]||| |[u / v][i][i@0]| = 1\}
10. first-success(\mlambda{}L.find-exact-eq-constraint(L);[u / v]) = (inl <i, x, x2>)
11. xx : \{l:\mBbbZ{} List| ||l|| = ((n - 1) + 1)\} List
12. exact-reduce-constraints(x;x2;[u / v]) = xx
13. x3 : \{L:\mBbbZ{} List| ||L|| = ((n - 1) + 1)\} List
14. gcd-reduce-eq-constraints([];xx) = (inl x3)
15. yy : \{l:\mBbbZ{} List| ||l|| = ((n - 1) + 1)\} List
16. exact-reduce-constraints(x;x2;ineqs) = yy
17. x4 : \{L:\mBbbZ{} List| ||L|| = ((n - 1) + 1)\} List
18. gcd-reduce-ineq-constraints([];yy) = (inl x4)
\mvdash{} 0 < ||u|| - 1
{}\mRightarrow{} (\mneg{}if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)|| - 1 < ||u||
- 1)
{}\mRightarrow{} (\mneg{}((if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)|| - 1
= (||u|| - 1))
\mwedge{} ||x3|| < ||v|| + 1))
{}\mRightarrow{} False
By
Latex:
TACTIC:(DVar `x3' THEN Reduce 0)
Home
Index