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