---

Step * 2 1 1 1 of Lemma unsat-omega_step


1. n : ℕ
2. v : {L:ℤ List| ||L|| = ((n + 1) - 1) ∈ ℤ}  List
3. ¬(n = 0 ∈ ℤ)
4. ∃xs:ℤ List. (∀as∈v.xs ⋅ as ≥0)
⊢ unsat(case gcd-reduce-ineq-constraints([];v) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x ) ⇒ False
BY
{ xxxDVar `v'xxx }

1
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

2
1. n : ℕ
2. u : {L:ℤ List| ||L|| = ((n + 1) - 1) ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = ((n + 1) - 1) ∈ ℤ}  List
4. ¬(n = 0 ∈ ℤ)
5. ∃xs:ℤ List. (∀as∈[u / v].xs ⋅ as ≥0)
⊢ unsat(case gcd-reduce-ineq-constraints([];[u / v]) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x ) ⇒ False

---

Latex:

---

Latex:

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


By

---

Latex:
xxxDVar  `v'xxx

---

Home Index