Nuprl Lemma : spread-ifthenelse

[b:𝔹]. ∀[f1,f2,x,y:Top].
  (let u,v 
   in if then f1[u;v] else f2[u;v] fi  if then let u,v in f1[u;v] else let u,v in f2[u;v] fi )


Proof




Definitions occuring in Statement :  ifthenelse: if then else fi  bool: 𝔹 uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] spread: spread def sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False
Lemmas referenced :  bool_wf eqtt_to_assert top_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base Error :assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality thin extract_by_obid hypothesis lambdaFormation sqequalHypSubstitution unionElimination equalityElimination isectElimination productElimination independent_isectElimination sqequalRule sqequalAxiom isect_memberEquality because_Cache dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination voidElimination

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[f1,f2,x,y:Top].
    (let  u,v  =  x 
      in  if  b  then  f1[u;v]  else  f2[u;v]  fi    \msim{}  if  b
    then  let  u,v  =  x 
              in  f1[u;v]
    else  let  u,v  =  x 
              in  f2[u;v]
    fi  )



Date html generated: 2018_05_21-PM-00_01_29
Last ObjectModification: 2018_01_28-PM-02_24_28

Theory : union


Home Index