Step
*
1
1
1
1
of Lemma
unsat-omega_start
1. n : ℕ
2. ineqs : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
3. xs : ℤ List
4. (∀as∈[].xs ⋅ as =0)
5. (∀bs∈ineqs.xs ⋅ bs ≥0)
⊢ xs |= case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x
BY
{ DVar `ineqs' }
1
1. n : ℕ
2. xs : ℤ List
3. (∀as∈[].xs ⋅ as =0)
4. (∀bs∈[].xs ⋅ bs ≥0)
⊢ xs |= case gcd-reduce-ineq-constraints([];[]) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x
2
1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List
4. xs : ℤ List
5. (∀as∈[].xs ⋅ as =0)
6. (∀bs∈[u / v].xs ⋅ bs ≥0)
⊢ xs |= case gcd-reduce-ineq-constraints([];[u / v]) of inl(ineqs') => inl <[], ineqs'> | inr(x) => inr x
Latex:
Latex:
1. n : \mBbbN{}
2. ineqs : \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List
3. xs : \mBbbZ{} List
4. (\mforall{}as\mmember{}[].xs \mcdot{} as =0)
5. (\mforall{}bs\mmember{}ineqs.xs \mcdot{} bs \mgeq{}0)
\mvdash{} xs |= case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <[], ineqs'> | inr(x) => in\000Cr x
By
Latex:
DVar `ineqs'
Home
Index