Nuprl Lemma : push-spread-into-ifthenelse

∀[a,X,Y,Z:Top].
  (let c,d = a 
   in if X[c;d] then Y[c;d] else Z[c;d] fi  ~ if let c,d = a 
                                                 in X[c;d]
  then let c,d = a 
       in Y[c;d]
  else let c,d = a 
       in Z[c;d]
  fi )


Proof



Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s1;s2],  spread: spread def,  sqequal: s ~ t
Definitions unfolded in proof :  so_apply: x[s1;s2],  so_lambda: λ2x y.t[x; y],  squash: ↓T,  or: P ∨ Q,  prop: ℙ,  has-value: (a)↓,  ifthenelse: if b then t else f fi ,  implies: P ⇒ Q,  all: ∀x:A. B[x],  and: P ∧ Q,  strict4: strict4(F),  uimplies: b supposing a,  top: Top,  so_apply: x[s1;s2;s3;s4],  member: t ∈ T,  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  uall: ∀[x:A]. B[x]
Lemmas referenced :  istype-top,  is-exception_wf,  istype-base,  has-value_wf_base,  istype-void,  lifting-strict-spread
Rules used in proof :  axiomSqleEquality,  spreadExceptionCases,  productElimination,  callbyvalueSpread,  divergentSqle,  sqequalSqle,  Error :inlFormation_alt,  exceptionSqequal,  imageElimination,  imageMemberEquality,  because_Cache,  Error :inrFormation_alt,  decideExceptionCases,  closedConclusion,  baseApply,  Error :universeIsType,  independent_functionElimination,  dependent_functionElimination,  Error :equalityIstype,  sqleReflexivity,  unionElimination,  Error :inhabitedIsType,  equalitySymmetry,  equalityTransitivity,  hypothesisEquality,  callbyvalueDecide,  Error :lambdaFormation_alt,  independent_pairFormation,  independent_isectElimination,  hypothesis,  voidElimination,  Error :isect_memberEquality_alt,  baseClosed,  thin,  isectElimination,  sqequalHypSubstitution,  extract_by_obid,  introduction,  cut,  sqequalRule,  Error :isect_memberFormation_alt,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution
Latex:
\mforall{}[a,X,Y,Z:Top].
    (let  c,d  =  a 
      in  if  X[c;d]  then  Y[c;d]  else  Z[c;d]  fi    \msim{}  if  let  c,d  =  a 
                                                                                                  in  X[c;d]
    then  let  c,d  =  a 
              in  Y[c;d]
    else  let  c,d  =  a 
              in  Z[c;d]
    fi  )


Date html generated: 2019_06_20-AM-11_27_18
Last ObjectModification: 2019_06_19-PM-04_37_01

Theory : computation


Home Index