Step
*
1
of Lemma
unsat-omega_start
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)
BY
{ (Unfold `omega_start` 0 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. (∀as∈eqs.xs ⋅ as =0)
6. (∀bs∈ineqs.xs ⋅ bs ≥0)
⊢ xs |= case gcd-reduce-eq-constraints([];eqs)
of inl(eqs') =>
case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x
| inr(x) =>
inr x
Latex:
Latex:
1. n : \mBbbN{}
2. eqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
3. ineqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
4. xs : \mBbbZ{} List
5. satisfies-integer-problem(eqs;ineqs;xs)
\mvdash{} xs |= omega\_start(eqs;ineqs)
By
Latex:
(Unfold `omega\_start` 0 THEN D -1)
Home
Index