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

t:Base. ((t)↓  ((t inr outr(t) ) ∨ (∀a,b:Base.  (if is inr then else b))))

Proof

Definitions occuring in Statement :  has-value: (a)↓ outr: outr(x) isinr: isinr def all: x:A. B[x] implies:  Q or: P ∨ Q inr: inr  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-isinr
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 isinrCases divergentSqle voidElimination isect_memberFormation introduction sqequalAxiom isect_memberEquality voidEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}t:Base.  ((t)\mdownarrow{}  {}\mRightarrow{}  ((t  \msim{}  inr  outr(t)  )  \mvee{}  (\mforall{}a,b:Base.    (if  t  is  inr  then  a  else  b  \msim{}  b))))

Date html generated: 2016_05_13-PM-03_22_45
Last ObjectModification: 2016_01_14-PM-06_46_42

Theory : call!by!value_1

Home Index