Nuprl Lemma : satisfies-integer-problem-length

[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List].
  {(∀e∈eqs.||e|| ||xs|| ∈ ℤ) ∧ (∀e∈ineqs.||e|| ||xs|| ∈ ℤ)} supposing satisfies-integer-problem(eqs;ineqs;xs)


Proof




Definitions occuring in Statement :  satisfies-integer-problem: satisfies-integer-problem(eqs;ineqs;xs) l_all: (∀x∈L.P[x]) length: ||as|| list: List uimplies: supposing a uall: [x:A]. B[x] guard: {T} and: P ∧ Q int: equal: t ∈ T
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q cand: c∧ B satisfies-integer-problem: satisfies-integer-problem(eqs;ineqs;xs) l_all: (∀x∈L.P[x]) all: x:A. B[x] satisfies-integer-equality: xs ⋅ as =0 satisfies-integer-inequality: xs ⋅ as ≥0 prop:
Lemmas referenced :  int_seg_wf length_wf list_wf satisfies-integer-problem_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lambdaFormation hypothesis dependent_functionElimination hypothesisEquality equalitySymmetry lemma_by_obid isectElimination natural_numberEquality intEquality independent_pairFormation independent_pairEquality lambdaEquality axiomEquality isect_memberEquality because_Cache equalityTransitivity

Latex:
\mforall{}[eqs,ineqs:\mBbbZ{}  List  List].  \mforall{}[xs:\mBbbZ{}  List].
    \{(\mforall{}e\mmember{}eqs.||e||  =  ||xs||)  \mwedge{}  (\mforall{}e\mmember{}ineqs.||e||  =  ||xs||)\} 
    supposing  satisfies-integer-problem(eqs;ineqs;xs)



Date html generated: 2016_05_14-AM-07_11_55
Last ObjectModification: 2015_12_26-PM-01_06_42

Theory : omega


Home Index