Nuprl Lemma : exception-not-bottom_1
∀[nm,val:Base].  ((exception(nm; val) ≤ ⊥) 
⇒ False)
Proof
Definitions occuring in Statement : 
bottom: ⊥
, 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
false: False
, 
base: Base
, 
sqle: s ≤ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
implies: P 
⇒ Q
, 
false: False
, 
prop: ℙ
Lemmas referenced : 
sqle_wf_base, 
base_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
lambdaFormation, 
exceptionNotBottom, 
hypothesis, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
sqequalRule, 
baseApply, 
closedConclusion, 
baseClosed, 
hypothesisEquality, 
lambdaEquality, 
dependent_functionElimination, 
because_Cache, 
isect_memberEquality, 
voidElimination
Latex:
\mforall{}[nm,val:Base].    ((exception(nm;  val)  \mleq{}  \mbot{})  {}\mRightarrow{}  False)
Date html generated:
2019_06_20-AM-11_20_35
Last ObjectModification:
2018_08_07-PM-03_15_14
Theory : call!by!value_1
Home
Index