Nuprl Lemma : omega_start_wf
∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List]. (omega_start(eqs;ineqs) ∈ IntConstraints)
Proof
Definitions occuring in Statement :
omega_start: omega_start(eqs;ineqs),
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_start: omega_start(eqs;ineqs),
subtype_rel: A ⊆r B,
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
int-constraint-problem: IntConstraints,
tunion: ⋃x:A.B[x],
pi2: snd(t),
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
gcd-reduce-eq-constraints_wf2,
nil_wf,
list_wf,
equal-wf-base-T,
unit_wf2,
gcd-reduce-ineq-constraints_wf2,
equal_wf,
list_subtype_base,
int_subtype_base,
nat_wf,
subtype_rel_union,
tunion_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
setEquality,
intEquality,
hypothesis,
sqequalRule,
baseApply,
closedConclusion,
baseClosed,
applyEquality,
because_Cache,
addEquality,
setElimination,
rename,
natural_numberEquality,
unionEquality,
lambdaFormation,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
independent_isectElimination,
isect_memberEquality,
unionElimination,
inlEquality,
imageMemberEquality,
dependent_pairEquality,
independent_pairEquality,
productEquality,
inrEquality,
voidEquality,
lambdaEquality,
voidElimination
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[eqs,ineqs:\{L:\mBbbZ{} List| ||L|| = (n + 1)\} List]. (omega\_start(eqs;ineqs) \mmember{} IntConstraints)
Date html generated:
2017_04_14-AM-09_12_23
Last ObjectModification:
2017_02_27-PM-03_50_05
Theory : omega
Home
Index