Nuprl Lemma : has-value-implies-dec-islambda-2

t:Base. ((t)↓  ((t ~ λx.(t x)) ∨ (∀a,b:Base.  (if is lambda then otherwise b))))


Proof




Definitions occuring in Statement :  has-value: (a)↓ islambda: if is lambda then otherwise b all: x:A. B[x] implies:  Q or: P ∨ Q apply: a lambda: λx.A[x] base: Base sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] implies:  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: 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-islambda
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 islambdaCases divergentSqle voidElimination isect_memberFormation introduction sqequalAxiom isect_memberEquality voidEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}t:Base.  ((t)\mdownarrow{}  {}\mRightarrow{}  ((t  \msim{}  \mlambda{}x.(t  x))  \mvee{}  (\mforall{}a,b:Base.    (if  t  is  lambda  then  a  otherwise  b  \msim{}  b))))



Date html generated: 2016_05_13-PM-03_22_47
Last ObjectModification: 2016_01_14-PM-06_46_38

Theory : call!by!value_1


Home Index