Nuprl Lemma : not_has-value_decidable_on_base

`¬(∀t:Base. ((t)↓ ∨ (¬(t)↓)))`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` all: `∀x:A. B[x]` not: `¬A` or: `P ∨ Q` base: `Base`
Definitions unfolded in proof :  not: `¬A` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` false: `False` has-value: `(a)↓` all: `∀x:A. B[x]` or: `P ∨ Q`
Lemmas referenced :  equal_wf not-id-sqle-bottom is-exception_wf exception-not-bottom bottom_diverge not_wf has-value_wf_base or_wf base_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation rename cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule lambdaEquality hypothesisEquality sqleRule sqleReflexivity divergentSqle independent_functionElimination voidElimination baseClosed applyEquality unionElimination equalityTransitivity equalitySymmetry dependent_functionElimination

Latex:
\mneg{}(\mforall{}t:Base.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{})))

Date html generated: 2016_05_13-PM-03_45_59
Last ObjectModification: 2016_01_14-PM-07_11_28

Theory : call!by!value_2

Home Index