Nuprl Lemma : sqequal-spread-cbva-weak
∀[a:Top × Top]. ∀[b,F:Top].  (let x ⟵ a in let u,v = x in F[u;v] ~ let u,v = a in let x ⟵ u in let y ⟵ v in F[x;y])
Proof
Definitions occuring in Statement : 
callbyvalueall: callbyvalueall, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s1;s2]
, 
spread: spread def, 
product: x:A × B[x]
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
so_apply: x[s1;s2]
, 
so_lambda: λ2x.t[x]
, 
top: Top
, 
so_apply: x[s]
Latex:
\mforall{}[a:Top  \mtimes{}  Top].  \mforall{}[b,F:Top].
    (let  x  \mleftarrow{}{}  a
      in  let  u,v  =  x 
            in  F[u;v]  \msim{}  let  u,v  =  a 
                                    in  let  x  \mleftarrow{}{}  u
                                          in  let  y  \mleftarrow{}{}  v
                                                in  F[x;y])
Date html generated:
2016_05_16-AM-10_51_06
Last ObjectModification:
2015_12_28-PM-07_38_09
Theory : halting!dataflow
Home
Index