---

Step * of Lemma exact-eq-constraint-implies

∀[eqs:ℤ List List]. ∀[i:ℕ||eqs||]. ∀[j:ℕ||eqs[i]||].
  ∀ineqs:ℤ List List. ∀xs:ℤ List.
    (satisfies-integer-problem(eqs;ineqs;xs)
    ⇒ (xs[j] = if (eqs[i][j] =z 1) then -1 * eqs[i]\j ⋅ xs\j else eqs[i]\j ⋅ xs\j fi  ∈ ℤ)) 
  supposing exact-eq-constraint(eqs;i;j)
BY
{ (Auto THEN D -1 THEN Thin (-1) THEN (With ⌜i⌝ (D (-1))⋅ THENA Auto) THEN RepeatFor 2 (D -1)) }

1
1. eqs : ℤ List List
2. i : ℕ||eqs||
3. j : ℕ||eqs[i]||
4. exact-eq-constraint(eqs;i;j)
5. ineqs : ℤ List List
6. xs : ℤ List
7. ||xs|| = ||eqs[i]|| ∈ ℤ
8. 0 < ||xs||
9. (hd(xs) = 1 ∈ ℤ) ∧ (eqs[i] ⋅ xs = 0 ∈ ℤ)
⊢ xs[j] = if (eqs[i][j] =z 1) then -1 * eqs[i]\j ⋅ xs\j else eqs[i]\j ⋅ xs\j fi  ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[eqs:\mBbbZ{}  List  List].  \mforall{}[i:\mBbbN{}||eqs||].  \mforall{}[j:\mBbbN{}||eqs[i]||].
    \mforall{}ineqs:\mBbbZ{}  List  List.  \mforall{}xs:\mBbbZ{}  List.
        (satisfies-integer-problem(eqs;ineqs;xs)
        {}\mRightarrow{}  (xs[j]  =  if  (eqs[i][j]  =\msubz{}  1)  then  -1  *  eqs[i]\mbackslash{}j  \mcdot{}  xs\mbackslash{}j  else  eqs[i]\mbackslash{}j  \mcdot{}  xs\mbackslash{}j  fi  )) 
    supposing  exact-eq-constraint(eqs;i;j)


By

---

Latex:
(Auto  THEN  D  -1  THEN  Thin  (-1)  THEN  (With  \mkleeneopen{}i\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (D  -1))

---

Home Index