Nuprl Lemma : omega_wf

`∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List].  (omega(eqs;ineqs) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} )`

Proof

Definitions occuring in Statement :  omega: `omega(eqs;ineqs)` int-problem-dimension: `dim(p)` int-constraint-problem: `IntConstraints` length: `||as||` list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` 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` omega: `omega(eqs;ineqs)` uimplies: `b supposing a` int-constraint-problem: `IntConstraints` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` prop: `ℙ` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` unit: `Unit` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)`
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 rep_int_constraint_step_wf omega_step_measure less_than_wf int-problem-dimension_wf list_subtype_base int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination lambdaEquality productEquality setEquality intEquality because_Cache baseApply closedConclusion baseClosed hypothesisEquality applyEquality addEquality setElimination rename natural_numberEquality independent_functionElimination lambdaFormation callbyvalueReduce dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[eqs,ineqs:\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List].
(omega(eqs;ineqs)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}  )

Date html generated: 2017_04_14-AM-09_12_38
Last ObjectModification: 2017_02_27-PM-03_49_57

Theory : omega

Home Index