---

Step * 1 1 of Lemma satisfiable-elim-eq-constraints


1. eqs : ℤ List List
2. ineqs : ℤ List List
3. xs : ℤ List
4. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
5. (∀bs∈ineqs.xs ⋅ bs ≥0)
6. i : ℕ||map(λeq.eager-map(λx.(-x);eq);eqs)||
7. xs ⋅ eqs[i] =0
⊢ xs ⋅ map(λx.(-x);eqs[i]) ≥0
BY
{ (UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN Auto) }

1
1. eqs : ℤ List List
2. ineqs : ℤ List List
3. xs : ℤ List
4. ∀i:ℕ||eqs||. xs ⋅ eqs[i] =0
5. (∀bs∈ineqs.xs ⋅ bs ≥0)
6. i : ℕ||map(λeq.eager-map(λx.(-x);eq);eqs)||
7. ||xs|| = ||eqs[i]|| ∈ ℤ
8. 0 < ||xs||
9. hd(xs) = 1 ∈ ℤ
10. eqs[i] ⋅ xs = 0 ∈ ℤ
11. ||xs|| = ||map(λx.(-x);eqs[i])|| ∈ ℤ
12. 0 < ||xs||
13. hd(xs) = 1 ∈ ℤ
⊢ map(λx.(-x);eqs[i]) ⋅ xs ≥ 0 

---

Latex:

---

Latex:

1.  eqs  :  \mBbbZ{}  List  List
2.  ineqs  :  \mBbbZ{}  List  List
3.  xs  :  \mBbbZ{}  List
4.  \mforall{}i:\mBbbN{}||eqs||.  xs  \mcdot{}  eqs[i]  =0
5.  (\mforall{}bs\mmember{}ineqs.xs  \mcdot{}  bs  \mgeq{}0)
6.  i  :  \mBbbN{}||map(\mlambda{}eq.eager-map(\mlambda{}x.(-x);eq);eqs)||
7.  xs  \mcdot{}  eqs[i]  =0
\mvdash{}  xs  \mcdot{}  map(\mlambda{}x.(-x);eqs[i])  \mgeq{}0


By

---

Latex:
(UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0  THEN  Auto)

---

Home Index