`∀[t,B:Top].  (let x,y = t in B[x;y] ~ if t is a pair then let x,y = t in B[x;y] otherwise ⊥)`

Proof

Definitions occuring in Statement :  bottom: `⊥` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` ispair: `if z is a pair then a otherwise b` spread: spread def sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` has-value: `(a)↓` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` top: `Top`
Lemmas referenced :  bottom-sqle top_wf has-value-implies-dec-ispair-2 is-exception_wf has-value_wf_base pair-eta
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueSpread sqequalHypSubstitution hypothesis lemma_by_obid isectElimination equalityTransitivity equalitySymmetry sqequalRule sqleReflexivity baseApply closedConclusion baseClosed hypothesisEquality spreadExceptionCases axiomSqleEquality exceptionSqequal callbyvalueIspair dependent_functionElimination independent_functionElimination unionElimination lambdaFormation isect_memberEquality voidElimination voidEquality ispairExceptionCases sqequalAxiom because_Cache

Latex:
\mforall{}[t,B:Top].    (let  x,y  =  t  in  B[x;y]  \msim{}  if  t  is  a  pair  then  let  x,y  =  t  in  B[x;y]  otherwise  \mbot{})

Date html generated: 2016_05_13-PM-03_46_27
Last ObjectModification: 2016_01_14-PM-07_11_11

Theory : call!by!value_2

Home Index