---

Step * of Lemma satisfiable-elim-eq-constraints

∀eqs,ineqs:ℤ List List. ∀xs:ℤ List.
  (satisfies-integer-problem(eqs;ineqs;xs)
  ⇒ satisfies-integer-problem([];(eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs;xs))
BY
{ (Auto
   THEN ParallelLast
   THEN D -1
   THEN D 0
   THEN Auto
   THEN (RWO "eager-map-is-map" 0 THEN Auto)
   THEN RepeatFor 2 ((BLemma `l_all_append` THEN Auto))
   THEN RepeatFor 2 (ParallelOp 4)) }

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(λeq.eager-map(λx.(-x);eq);eqs)[i] ≥0

2
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

---

Latex:

---

Latex:
\mforall{}eqs,ineqs:\mBbbZ{}  List  List.  \mforall{}xs:\mBbbZ{}  List.
    (satisfies-integer-problem(eqs;ineqs;xs)
    {}\mRightarrow{}  satisfies-integer-problem([];(eager-map(\mlambda{}eq.eager-map(\mlambda{}x.(-x);eq);eqs)  @  eqs)  @  ineqs;xs))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  D  -1
  THEN  D  0
  THEN  Auto
  THEN  (RWO  "eager-map-is-map"  0  THEN  Auto)
  THEN  RepeatFor  2  ((BLemma  `l\_all\_append`  THEN  Auto))
  THEN  RepeatFor  2  (ParallelOp  4))

---

Home Index