---

Step * of Lemma unsat-omega_start

∀n:ℕ. ∀eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List.  (unsat(omega_start(eqs;ineqs)) ⇒ (¬satisfiable(eqs;ineqs)))
BY
{ (Auto THEN D 0 THEN Auto THEN D -1 THEN (With ⌜xs⌝ (D 4)⋅ THENA Auto) THEN D -1) }

1
1. n : ℕ
2. eqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
3. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. xs : ℤ List
5. satisfies-integer-problem(eqs;ineqs;xs)
⊢ xs |= omega_start(eqs;ineqs)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List.
    (unsat(omega\_start(eqs;ineqs))  {}\mRightarrow{}  (\mneg{}satisfiable(eqs;ineqs)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  -1  THEN  (With  \mkleeneopen{}xs\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index