Step
*
1
1
2
1
1
of Lemma
satisfiable-exact-reduce-constraints
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ+||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (∀e∈eqs.||e|| = ||xs|| ∈ ℤ)
9. (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)
10. ||eqs[i]|| ~ ||xs||
11. eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
12. ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
13. 1 ≤ j
14. j < ||xs||
15. 0 < ||xs\j||
16. hd(xs\j) = hd(xs) ∈ ℤ
17. (∀bs∈ineqs.xs ⋅ bs ≥0)
18. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
19. i@0 : ℕ||eqs||
20. ||xs|| = ||eqs[i@0]|| ∈ ℤ
21. 0 < ||xs||
22. hd(xs) = 1 ∈ ℤ
23. eqs[i@0] ⋅ xs = 0 ∈ ℤ
24. 0 < ||xs\j||
25. hd(xs\j) = 1 ∈ ℤ
26. ||xs|| = ||eqs[i@0]|| ∈ ℤ
27. 0 < ||xs||
28. hd(xs) = 1 ∈ ℤ
29. eqs[i@0] ⋅ xs = 0 ∈ ℤ
⊢ eqs[i@0] ⋅ xs = -(eqs[i][j] * eqs[i@0][j]) * eqs[i]\j + eqs[i@0]\j ⋅ xs\j ∈ ℤ
BY
{ TACTIC:(InstLemma `int-dot-reduce-dim` [⌜eqs[i@0]⌝;⌜xs⌝;⌜j⌝;⌜-eqs[i][j] * eqs[i]\j⌝]⋅ THENA Auto) }
1
.....antecedent.....
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ+||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (∀e∈eqs.||e|| = ||xs|| ∈ ℤ)
9. (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)
10. ||eqs[i]|| ~ ||xs||
11. eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
12. ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
13. 1 ≤ j
14. j < ||xs||
15. 0 < ||xs\j||
16. hd(xs\j) = hd(xs) ∈ ℤ
17. (∀bs∈ineqs.xs ⋅ bs ≥0)
18. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
19. i@0 : ℕ||eqs||
20. ||xs|| = ||eqs[i@0]|| ∈ ℤ
21. 0 < ||xs||
22. hd(xs) = 1 ∈ ℤ
23. eqs[i@0] ⋅ xs = 0 ∈ ℤ
24. 0 < ||xs\j||
25. hd(xs\j) = 1 ∈ ℤ
26. ||xs|| = ||eqs[i@0]|| ∈ ℤ
27. 0 < ||xs||
28. hd(xs) = 1 ∈ ℤ
29. eqs[i@0] ⋅ xs = 0 ∈ ℤ
⊢ ||-eqs[i][j] * eqs[i]\j|| = (||eqs[i@0]|| - 1) ∈ ℤ
2
.....antecedent.....
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ+||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (∀e∈eqs.||e|| = ||xs|| ∈ ℤ)
9. (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)
10. ||eqs[i]|| ~ ||xs||
11. eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
12. ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
13. 1 ≤ j
14. j < ||xs||
15. 0 < ||xs\j||
16. hd(xs\j) = hd(xs) ∈ ℤ
17. (∀bs∈ineqs.xs ⋅ bs ≥0)
18. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
19. i@0 : ℕ||eqs||
20. ||xs|| = ||eqs[i@0]|| ∈ ℤ
21. 0 < ||xs||
22. hd(xs) = 1 ∈ ℤ
23. eqs[i@0] ⋅ xs = 0 ∈ ℤ
24. 0 < ||xs\j||
25. hd(xs\j) = 1 ∈ ℤ
26. ||xs|| = ||eqs[i@0]|| ∈ ℤ
27. 0 < ||xs||
28. hd(xs) = 1 ∈ ℤ
29. eqs[i@0] ⋅ xs = 0 ∈ ℤ
⊢ xs[j] = -eqs[i][j] * eqs[i]\j ⋅ xs\j ∈ ℤ
3
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ+||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (∀e∈eqs.||e|| = ||xs|| ∈ ℤ)
9. (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)
10. ||eqs[i]|| ~ ||xs||
11. eqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
12. ineqs ∈ {l:ℤ List| ||l|| = ||eqs[i]|| ∈ ℤ} List
13. 1 ≤ j
14. j < ||xs||
15. 0 < ||xs\j||
16. hd(xs\j) = hd(xs) ∈ ℤ
17. (∀bs∈ineqs.xs ⋅ bs ≥0)
18. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
19. i@0 : ℕ||eqs||
20. ||xs|| = ||eqs[i@0]|| ∈ ℤ
21. 0 < ||xs||
22. hd(xs) = 1 ∈ ℤ
23. eqs[i@0] ⋅ xs = 0 ∈ ℤ
24. 0 < ||xs\j||
25. hd(xs\j) = 1 ∈ ℤ
26. ||xs|| = ||eqs[i@0]|| ∈ ℤ
27. 0 < ||xs||
28. hd(xs) = 1 ∈ ℤ
29. eqs[i@0] ⋅ xs = 0 ∈ ℤ
30. eqs[i@0] ⋅ xs ~ eqs[i@0][j] * -eqs[i][j] * eqs[i]\j + eqs[i@0]\j ⋅ xs\j
⊢ eqs[i@0] ⋅ xs = -(eqs[i][j] * eqs[i@0][j]) * eqs[i]\j + eqs[i@0]\j ⋅ xs\j ∈ ℤ
Latex:
Latex:
1. eqs : \mBbbZ{} List List
2. i : \mBbbN{}||eqs||
3. j : \mBbbN{}\msupplus{}||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : \mBbbZ{} List List
6. xs : \mBbbZ{} List
7. satisfies-integer-problem(eqs;ineqs;xs)
8. (\mforall{}e\mmember{}eqs.||e|| = ||xs||)
9. (\mforall{}e\mmember{}ineqs.||e|| = ||xs||)
10. ||eqs[i]|| \msim{} ||xs||
11. eqs \mmember{} \{l:\mBbbZ{} List| ||l|| = ||eqs[i]||\} List
12. ineqs \mmember{} \{l:\mBbbZ{} List| ||l|| = ||eqs[i]||\} List
13. 1 \mleq{} j
14. j < ||xs||
15. 0 < ||xs\mbackslash{}j||
16. hd(xs\mbackslash{}j) = hd(xs)
17. (\mforall{}bs\mmember{}ineqs.xs \mcdot{} bs \mgeq{}0)
18. \mforall{}i:\mBbbN{}||eqs||. xs \mcdot{} eqs[i] =0
19. i@0 : \mBbbN{}||eqs||
20. ||xs|| = ||eqs[i@0]||
21. 0 < ||xs||
22. hd(xs) = 1
23. eqs[i@0] \mcdot{} xs = 0
24. 0 < ||xs\mbackslash{}j||
25. hd(xs\mbackslash{}j) = 1
26. ||xs|| = ||eqs[i@0]||
27. 0 < ||xs||
28. hd(xs) = 1
29. eqs[i@0] \mcdot{} xs = 0
\mvdash{} eqs[i@0] \mcdot{} xs = -(eqs[i][j] * eqs[i@0][j]) * eqs[i]\mbackslash{}j + eqs[i@0]\mbackslash{}j \mcdot{} xs\mbackslash{}j
By
Latex:
TACTIC:(InstLemma `int-dot-reduce-dim` [\mkleeneopen{}eqs[i@0]\mkleeneclose{};\mkleeneopen{}xs\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}-eqs[i][j] * eqs[i]\mbackslash{}j\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index