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