### Nuprl Lemma : satisfies-integer-problem_wf

`∀[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List].  (satisfies-integer-problem(eqs;ineqs;xs) ∈ ℙ)`

Proof

Definitions occuring in Statement :  satisfies-integer-problem: `satisfies-integer-problem(eqs;ineqs;xs)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` satisfies-integer-problem: `satisfies-integer-problem(eqs;ineqs;xs)` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  and_wf l_all_wf list_wf satisfies-integer-equality_wf l_member_wf satisfies-integer-inequality_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis hypothesisEquality lambdaEquality setElimination rename setEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[eqs,ineqs:\mBbbZ{}  List  List].  \mforall{}[xs:\mBbbZ{}  List].    (satisfies-integer-problem(eqs;ineqs;xs)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_14-AM-07_11_36
Last ObjectModification: 2015_12_26-PM-01_06_48

Theory : omega

Home Index