Step
*
1
1
1
1
1
of Lemma
omega_step_measure
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
4. 0 < dim(inl <eqs, ineqs>)
5. ¬(n = 0 ∈ ℤ)
6. first-success(λL.find-exact-eq-constraint(L);eqs) ∈ i:ℕ||eqs||
× x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)}
× {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?
7. i : ℕ||eqs||
8. x : {x:ℤ List| x = eqs[i] ∈ (ℤ List)}
9. x2 : {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ}
10. first-success(λL.find-exact-eq-constraint(L);eqs)
= (inl <i, x, x2>)
∈ (i:ℕ||eqs|| × x:{x:ℤ List| x = eqs[i] ∈ (ℤ List)} × {i@0:ℕ+||eqs[i]||| |eqs[i][i@0]| = 1 ∈ ℤ} ?)
11. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
12. exact-reduce-constraints(x;x2;eqs) = 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?)
⊢ (¬dim(inl <x3, x4>) < dim(inl <eqs, ineqs>)) ⇒ (¬((dim(inl <x3, x4>) = dim(inl <eqs, ineqs>) ∈ ℤ) ∧ num-eq-constraint\000Cs(inl <x3, x4>) < num-eq-constraints(inl <eqs, ineqs>))) ⇒ False
BY
{ TACTIC:(MoveToConcl 4 THEN RepUR ``int-problem-dimension num-eq-constraints`` 0 THEN DVar `eqs' THEN Reduce 0) }
1
1. n : ℕ
2. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
3. ¬(n = 0 ∈ ℤ)
4. first-success(λL.find-exact-eq-constraint(L);[]) ∈ i:ℕ||[]||
× x:{x:ℤ List| x = [][i] ∈ (ℤ List)}
× {i@0:ℕ+||[][i]||| |[][i][i@0]| = 1 ∈ ℤ} ?
5. i : ℕ||[]||
6. x : {x:ℤ List| x = [][i] ∈ (ℤ List)}
7. x2 : {i@0:ℕ+||[][i]||| |[][i][i@0]| = 1 ∈ ℤ}
8. 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 ∈ ℤ} ?)
9. xx : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
10. exact-reduce-constraints(x;x2;[]) = xx ∈ ({l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
11. x3 : {L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List
12. gcd-reduce-eq-constraints([];xx) = (inl x3) ∈ ({L:ℤ List| ||L|| = ((n - 1) + 1) ∈ ℤ} List?)
13. yy : {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List
14. exact-reduce-constraints(x;x2;ineqs) = 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 < if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1
⇒ (¬if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)||
- 1 < if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1)
⇒ (¬((if x3 = Ax then if x4 = Ax then 0 otherwise ||hd(x4)|| - 1 otherwise ||hd(x3)|| - 1
= if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1
∈ ℤ)
∧ ||x3|| < 0))
⇒ 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. 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
Latex:
Latex:
1. n : \mBbbN{}
2. eqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
3. ineqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
4. 0 < dim(inl <eqs, ineqs>)
5. \mneg{}(n = 0)
6. first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs) \mmember{} i:\mBbbN{}||eqs||
\mtimes{} x:\{x:\mBbbZ{} List| x = eqs[i]\}
\mtimes{} \{i@0:\mBbbN{}\msupplus{}||eqs[i]||| |eqs[i][i@0]| = 1\} ?
7. i : \mBbbN{}||eqs||
8. x : \{x:\mBbbZ{} List| x = eqs[i]\}
9. x2 : \{i@0:\mBbbN{}\msupplus{}||eqs[i]||| |eqs[i][i@0]| = 1\}
10. first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs) = (inl <i, x, x2>)
11. xx : \{l:\mBbbZ{} List| ||l|| = ((n - 1) + 1)\} List
12. exact-reduce-constraints(x;x2;eqs) = 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{} (\mneg{}dim(inl <x3, x4>) < dim(inl <eqs, ineqs>)) {}\mRightarrow{} (\mneg{}((dim(inl <x3, x4>) = dim(inl <eqs, ineqs>)) \mwedge{} n\000Cum-eq-constraints(inl <x3, x4>) < num-eq-constraints(inl <eqs, ineqs>))) {}\mRightarrow{} False
By
Latex:
TACTIC:(MoveToConcl 4
THEN RepUR ``int-problem-dimension num-eq-constraints`` 0
THEN DVar `eqs'
THEN Reduce 0)
Home
Index