Nuprl Lemma : stuck-decide

  (∀[F,H:Top].  (case of inl(x) => F[x] inr(x) => H[x] eval in ⊥)) supposing 
     ((∀b,c:Base.  (if is inl then else c)) and 
     (∀b,c:Base.  (if is inr then else c)))


Definitions occuring in Statement :  bottom: callbyvalue: callbyvalue uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s] isinr: isinr def isinl: isinl def all: x:A. B[x] decide: case of inl(x) => s[x] inr(y) => t[y] base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ all: x:A. B[x] or: P ∨ Q sq_type: SQType(T) implies:  Q guard: {T} uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  btrue: tt isl: isl(x) assert: b outl: outl(x) not: ¬A false: False bfalse: ff outr: outr(x) prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  base_wf all_wf exception-not-bottom bottom_diverge is-exception_wf has-value_wf_base assert_of_bnot eqff_to_assert not-btrue-sqeq-bfalse eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases top_wf isl_wf injection-eta
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueDecide sqequalHypSubstitution hypothesis lemma_by_obid dependent_functionElimination equalityTransitivity equalitySymmetry isectElimination because_Cache unionElimination instantiate cumulativity independent_isectElimination independent_functionElimination productElimination sqequalRule baseClosed promote_hyp voidElimination decideExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity baseApply closedConclusion hypothesisEquality callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases sqequalAxiom isect_memberEquality lambdaEquality sqequalIntensionalEquality

    (\mforall{}[F,H:Top].    (case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  H[x]  \msim{}  eval  x  =  a  in  \mbot{}))  supposing 
          ((\mforall{}b,c:Base.    (if  a  is  inl  then  b  else  c  \msim{}  c))  and 
          (\mforall{}b,c:Base.    (if  a  is  inr  then  b  else  c  \msim{}  c)))

Date html generated: 2016_05_13-PM-03_44_56
Last ObjectModification: 2016_01_14-PM-07_06_31

Theory : computation

Home Index