### Nuprl Lemma : no-value-bottom-base

`∀[x:Base]. x ~ ⊥ supposing (¬(x)↓) ∧ (¬is-exception(x))`

Proof

Definitions occuring in Statement :  bottom: `⊥` has-value: `(a)↓` is-exception: `is-exception(t)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` top: `Top` prop: `ℙ`
Lemmas referenced :  has-value_wf_base is-exception_wf bottom-sqle and_wf not_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle sqequalHypSubstitution productElimination thin independent_functionElimination hypothesis voidElimination lemma_by_obid isectElimination hypothesisEquality isect_memberEquality voidEquality sqequalAxiom sqequalRule because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[x:Base].  x  \msim{}  \mbot{}  supposing  (\mneg{}(x)\mdownarrow{})  \mwedge{}  (\mneg{}is-exception(x))

Date html generated: 2016_05_15-PM-10_04_10
Last ObjectModification: 2015_12_27-PM-05_16_55

Theory : bar!type

Home Index