Nuprl Lemma : decidable__equal-int_seg
∀[a,b:ℤ]. ∀x,y:{a..b-}. Dec(x = y ∈ {a..b-})
Proof
Definitions occuring in Statement :
int_seg: {i..j-},
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
or: P ∨ Q,
decidable: Dec(P),
int_seg: {i..j-},
member: t ∈ T,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
prop: ℙ,
squash: ↓T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
and: P ∧ Q,
lelt: i ≤ j < k,
false: False,
not: ¬A
Lemmas referenced :
int_seg_wf,
decidable__int_equal,
equal_wf,
not_wf,
less_than_wf,
and_wf,
decidable__le,
le_wf,
sq_stable_from_decidable
Rules used in proof :
intEquality,
isectElimination,
unionElimination,
hypothesis,
hypothesisEquality,
rename,
setElimination,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
because_Cache,
imageElimination,
baseClosed,
imageMemberEquality,
sqequalRule,
productElimination,
independent_functionElimination,
independent_pairFormation,
dependent_set_memberEquality,
inlFormation,
voidElimination,
applyLambdaEquality,
inrFormation
Latex:
\mforall{}[a,b:\mBbbZ{}]. \mforall{}x,y:\{a..b\msupminus{}\}. Dec(x = y)
Date html generated:
2018_05_21-PM-00_01_49
Last ObjectModification:
2018_01_05-PM-00_05_52
Theory : arithmetic
Home
Index