---

Step * 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(λeq.eager-map(λx.(-x);eq);eqs)[i] ≥0
BY
{ ((RWO "select-map" 0 THEN Auto) THEN Reduce 0 THEN RWO "eager-map-is-map" 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] =0
⊢ xs ⋅ map(λx.(-x);eqs[i]) ≥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{}eq.eager-map(\mlambda{}x.(-x);eq);eqs)[i]  \mgeq{}0


By

---

Latex:
((RWO  "select-map"  0  THEN  Auto)  THEN  Reduce  0  THEN  RWO  "eager-map-is-map"  0  THEN  Auto)

---

Home Index