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: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
and: P ∧ Q,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
cand: A 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