---

Step * 1 1 1 1 of Lemma satisfiable-elim-eq-constraints


1. xs : ℤ List
2. v : ℤ List
⊢ (v ⋅ xs = 0 ∈ ℤ) ⇒ (map(λx.(-x);v) ⋅ xs ≥ 0 )
BY
{ (Subst' map(λx.(-x);v) ~ -1 * v 0 THENA (Auto THEN Unfold `int-vec-mul` 0 THEN EqCD THEN Auto)) }

1
1. xs : ℤ List
2. v : ℤ List
⊢ (v ⋅ xs = 0 ∈ ℤ) ⇒ (-1 * v ⋅ xs ≥ 0 )

---

Latex:

---

Latex:

1.  xs  :  \mBbbZ{}  List
2.  v  :  \mBbbZ{}  List
\mvdash{}  (v  \mcdot{}  xs  =  0)  {}\mRightarrow{}  (map(\mlambda{}x.(-x);v)  \mcdot{}  xs  \mgeq{}  0  )


By

---

Latex:
(Subst'  map(\mlambda{}x.(-x);v)  \msim{}  -1  *  v  0  THENA  (Auto  THEN  Unfold  `int-vec-mul`  0  THEN  EqCD  THEN  Auto))

---

Home Index