---

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


1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ∃xs:ℤ List. (∀as∈[].xs ⋅ as ≥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.  \mexists{}xs:\mBbbZ{}  List.  (\mforall{}as\mmember{}[].xs  \mcdot{}  as  \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