Nuprl Lemma : satisfiable-pcs-to-integer-problem

`∀X:polynomial-constraints()`
`  (satisfiable_polynomial_constraints(X) `` satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))`

Proof

Definitions occuring in Statement :  satisfiable-integer-problem: `satisfiable(eqs;ineqs)` pcs-to-integer-problem: `pcs-to-integer-problem(X)` satisfiable_polynomial_constraints: `satisfiable_polynomial_constraints(X)` polynomial-constraints: `polynomial-constraints()` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` satisfiable_polynomial_constraints: `satisfiable_polynomial_constraints(X)` exists: `∃x:A. B[x]` pcs-to-integer-problem: `pcs-to-integer-problem(X)` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` uimplies: `b supposing a` polynomial-constraints: `polynomial-constraints()` satisfies-poly-constraints: `satisfies-poly-constraints(f;X)` and: `P ∧ Q` subtype_rel: `A ⊆r B` pi1: `fst(t)` pi2: `snd(t)` has-value: `(a)↓` sq_type: `SQType(T)` guard: `{T}` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` or: `P ∨ Q` squash: `↓T` iPolynomial: `iPolynomial()` cand: `A c∧ B` l_all: `(∀x∈L.P[x])` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` iMonomial: `iMonomial()` pcs-mon-vars: `pcs-mon-vars(X)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` l_member: `(x ∈ l)` l_exists: `(∃x∈L. P[x])` nat: `ℕ` le: `A ≤ B` less_than: `a < b` int_nzero: `ℤ-o` satisfiable-integer-problem: `satisfiable(eqs;ineqs)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` satisfies-integer-problem: `satisfies-integer-problem(eqs;ineqs;xs)` top: `Top` satisfies-integer-equality: `xs ⋅ as =0` linearization: `linearization(p;L)` subtract: `n - m` less_than': `less_than'(a;b)` false: `False` cons: `[a / b]` not: `¬A` satisfies-integer-inequality: `xs ⋅ as ≥0`
Lemmas referenced :  hd-rev-pcs-mon-vars reverse_wf list_wf pcs-mon-vars_wf equal_wf satisfiable_polynomial_constraints_wf polynomial-constraints_wf value-type-has-value list-value-type iPolynomial_wf linearization_wf equal-wf-base list_subtype_base int_subtype_base less_than_wf length_wf map_wf list-valueall-type int-valueall-type eager-map-is-map evalall-reduce subtype_base_sq no_repeats_reverse no_repeats-pcs-mon-vars or_wf l_member_wf squash_wf true_wf int_term_value_wf ipolynomial-term_wf linearization-value int_seg_wf iMonomial_wf iff_weakening_equal member-pcs-mon-vars select_wf sq_stable__le member-reverse equal-wf-T-base l_exists_wf pi1_wf pi2_wf lelt_wf set_subtype_base product_subtype_base list_accum_wf satisfies-integer-problem_wf select-map subtype_rel_list top_wf map-length length_wf_nat and_wf nat_wf map_length poly-coeff-of_wf non_neg_length le_wf subtract_wf minus-one-mul add-swap add-commutes add-associates add-mul-special two-mul mul-distributes-right zero-mul zero-add one-mul int_seg_properties nat_properties list-cases map_nil_lemma length_of_nil_lemma product_subtype_list map_cons_lemma length_of_cons_lemma reduce_hd_cons_lemma list_accum_nil_lemma list_accum_cons_lemma null_nil_lemma btrue_wf null_wf null_cons_lemma bfalse_wf btrue_neq_bfalse length-map select_member ge_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid dependent_functionElimination hypothesisEquality isectElimination intEquality hypothesis equalityTransitivity equalitySymmetry independent_functionElimination independent_isectElimination sqequalRule lambdaEquality applyEquality setElimination rename setEquality baseApply closedConclusion baseClosed because_Cache productEquality natural_numberEquality callbyvalueReduce instantiate cumulativity independent_pairEquality isect_memberFormation functionEquality imageElimination universeEquality functionExtensionality independent_pairFormation imageMemberEquality axiomEquality addLevel inrFormation unionElimination inlFormation dependent_pairFormation dependent_set_memberEquality multiplyEquality isect_memberEquality voidElimination voidEquality hyp_replacement applyLambdaEquality levelHypothesis sqequalIntensionalEquality promote_hyp addEquality hypothesis_subsumption

Latex:
\mforall{}X:polynomial-constraints()
(satisfiable\_polynomial\_constraints(X)
{}\mRightarrow{}  satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))

Date html generated: 2017_04_14-AM-09_04_51
Last ObjectModification: 2017_02_27-PM-03_45_39

Theory : omega

Home Index