### Nuprl Lemma : isr-omega

`∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].  ¬satisfiable(eqs;ineqs) supposing ↑isr(omega(eqs;ineqs))`

Proof

Definitions occuring in Statement :  omega: `omega(eqs;ineqs)` satisfiable-integer-problem: `satisfiable(eqs;ineqs)` length: `||as||` list: `T List` nat: `ℕ` assert: `↑b` isr: `isr(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` set: `{x:A| B[x]} ` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` omega: `omega(eqs;ineqs)` int-constraint-problem: `IntConstraints` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` unit: `Unit` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` and: `P ∧ Q` cand: `A c∧ B`
Lemmas referenced :  valueall-type-has-valueall int-constraint-problem_wf union-valueall-type tunion_wf nat_wf list_wf equal-wf-base-T unit_wf2 tunion-valueall-type product-valueall-type list-valueall-type set-valueall-type int-valueall-type equal-valueall-type omega_start_wf evalall-reduce isr-rep_int_constraint_step omega_step_wf omega_step_measure less_than_wf int-problem-dimension_wf unsat-omega_step unsat-int-problem_wf unsat-omega_start satisfiable-integer-problem_wf subtype_rel_list assert_wf isr_wf omega_wf equal-wf-T-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalHypSubstitution sqequalRule extract_by_obid isectElimination hypothesis independent_isectElimination lambdaEquality productEquality setEquality intEquality baseApply closedConclusion baseClosed hypothesisEquality applyEquality because_Cache addEquality setElimination rename natural_numberEquality independent_functionElimination callbyvalueReduce dependent_functionElimination independent_pairFormation voidElimination isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
\mneg{}satisfiable(eqs;ineqs)  supposing  \muparrow{}isr(omega(eqs;ineqs))

Date html generated: 2017_04_14-AM-09_12_43
Last ObjectModification: 2017_02_27-PM-03_50_00

Theory : omega

Home Index