### Nuprl Lemma : has-value-implies-dec-isaxiom-2

`∀t:Base. ((t)↓ `` ((t ~ Ax) ∨ (∀a,b:Base.  (if t = Ax then a otherwise b ~ b))))`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` isaxiom: `if z = Ax then a otherwise b` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` base: `Base` sqequal: `s ~ t` axiom: `Ax`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` or: `P ∨ Q` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` uimplies: `b supposing a` has-value: `(a)↓` false: `False` top: `Top` sq_type: `SQType(T)`
Lemmas referenced :  top_wf not_zero_sqequal_one is-exception_wf has-value_wf_base subtype_rel_self subtype_base_sq base_wf all_wf has-value-implies-dec-isaxiom
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality baseClosed independent_functionElimination hypothesis unionElimination inlFormation isectElimination sqequalRule lambdaEquality sqequalIntensionalEquality baseApply closedConclusion inrFormation instantiate because_Cache independent_isectElimination isaxiomCases divergentSqle voidElimination isect_memberFormation introduction sqequalAxiom isect_memberEquality voidEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}t:Base.  ((t)\mdownarrow{}  {}\mRightarrow{}  ((t  \msim{}  Ax)  \mvee{}  (\mforall{}a,b:Base.    (if  t  =  Ax  then  a  otherwise  b  \msim{}  b))))

Date html generated: 2016_05_13-PM-03_22_38
Last ObjectModification: 2016_01_14-PM-06_46_54

Theory : call!by!value_1

Home Index