---

Step * 2 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. (∀bs∈map(λeq.eager-map(λx.(-x);eq);eqs).xs ⋅ bs ≥0)
7. i : ℕ||eqs||
8. xs ⋅ eqs[i] =0
⊢ xs ⋅ eqs[i] ≥0
BY
{ (UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN Auto) }

---

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.  (\mforall{}bs\mmember{}map(\mlambda{}eq.eager-map(\mlambda{}x.(-x);eq);eqs).xs  \mcdot{}  bs  \mgeq{}0)
7.  i  :  \mBbbN{}||eqs||
8.  xs  \mcdot{}  eqs[i]  =0
\mvdash{}  xs  \mcdot{}  eqs[i]  \mgeq{}0


By

---

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

---

Home Index