Step
*
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-eq-constraints([];[])
of inl(eqs') =>
case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x
| inr(x) =>
inr x
BY
{ RepUR ``gcd-reduce-eq-constraints`` 0 }
1
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
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-eq-constraints([];[])
of inl(eqs') =>
case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x
| inr(x) =>
inr x
By
Latex:
RepUR ``gcd-reduce-eq-constraints`` 0
Home
Index