Nuprl Lemma : not-has-value-bottom
¬(⊥)↓
Proof
Definitions occuring in Statement :
bottom: ⊥,
has-value: (a)↓,
not: ¬A
Definitions unfolded in proof :
has-value: (a)↓,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
top: Top,
so_apply: x[s],
not: ¬A,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
true: True,
false: False,
prop: ℙ
Lemmas referenced :
sqle_wf_base,
int_subtype_base,
subtype_base_sq,
strictness-callbyvalue,
bottom-sqle,
cbv_bottom_lemma
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
comment,
lambdaFormation,
sqequalSqle,
isectElimination,
natural_numberEquality,
instantiate,
cumulativity,
intEquality,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
promote_hyp,
baseClosed
Latex:
\mneg{}(\mbot{})\mdownarrow{}
Date html generated:
2016_05_15-PM-02_07_15
Last ObjectModification:
2016_01_15-PM-10_24_00
Theory : untyped!computation
Home
Index