---

Step * 1 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]|| ∈ ℤ
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 
BY
{ (MoveToConcl (-4) THEN (RWO "length-map" 6 THENA Auto) THEN (GenConclTerm ⌜eqs[i]⌝⋅ THENA Auto) THEN All Thin) }

1
1. xs : ℤ List
2. v : ℤ List
⊢ (v ⋅ xs = 0 ∈ ℤ) ⇒ (map(λx.(-x);v) ⋅ 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||  =  ||eqs[i]||
8.  0  <  ||xs||
9.  hd(xs)  =  1
10.  eqs[i]  \mcdot{}  xs  =  0
11.  ||xs||  =  ||map(\mlambda{}x.(-x);eqs[i])||
12.  0  <  ||xs||
13.  hd(xs)  =  1
\mvdash{}  map(\mlambda{}x.(-x);eqs[i])  \mcdot{}  xs  \mgeq{}  0 


By

---

Latex:
(MoveToConcl  (-4)
  THEN  (RWO  "length-map"  6  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}eqs[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index