---

Step * 1 1 1 1 1 1 1 1 of Lemma unsat-omega_step


1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. xs : ℤ List
4. (∀as∈[].xs ⋅ as =0)
5. (∀bs∈[].xs ⋅ bs ≥0)
⊢ unsat(case gcd-reduce-ineq-constraints([];[]) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x ) ⇒ False
BY
{ xxx(RepUR ``gcd-reduce-ineq-constraints unsat-int-problem satisfies-int-constraint-problem`` 0
      THEN Auto
      THEN (InstHyp [⌜[]⌝] (-1)⋅ THENA Auto)
      THEN D -1
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mneg{}(n  =  0)
3.  xs  :  \mBbbZ{}  List
4.  (\mforall{}as\mmember{}[].xs  \mcdot{}  as  =0)
5.  (\mforall{}bs\mmember{}[].xs  \mcdot{}  bs  \mgeq{}0)
\mvdash{}  unsat(case  gcd-reduce-ineq-constraints([];[])  of  inl(ineqs')  =>  inl  <[],  ineqs'>  |  inr(x)  =>  inr  x\000C  )
{}\mRightarrow{}  False


By

---

Latex:
xxx(RepUR  ``gcd-reduce-ineq-constraints  unsat-int-problem  satisfies-int-constraint-problem``  0
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
        THEN  D  -1
        THEN  Auto)xxx

---

Home Index