Nuprl Lemma : hdf-sqequal7
∀[F,G,H,K,L,J,init:Top].
  (fix((λmk-hdf,s0. (inl (λa.let X,s = s0 
                             in case X
                                 of inl(P) =>
                                 let X',fs = P a 
                                 in let b ⟵ G[fs;s]
                                    in let s' ⟵ J[b;s]
                                       in <mk-hdf <X', K[s;s']>, L[s;s']>
                                 | inr(z) =>
                                 H[mk-hdf;s;z])))) 
   <fix((λmk-hdf.(inl (λa.let out ⟵ F[a] in <mk-hdf, out>)))), init> ~ fix((λmk-hdf,s. (inl (λa.let out ⟵ F[a]
                                                                              in let b ⟵ G[out;s]
                                                                                 in let s' ⟵ J[b;s]
                                                                                    in <mk-hdf K[s;s'], L[s;s']>)))) 
                                                     init)
Proof
Definitions occuring in Statement : 
callbyvalueall: callbyvalueall, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s1;s2;s3]
, 
so_apply: x[s1;s2]
, 
so_apply: x[s]
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inl: inl x
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
nat: ℕ
, 
implies: P 
⇒ Q
, 
false: False
, 
ge: i ≥ j 
, 
uimplies: b supposing a
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
exists: ∃x:A. B[x]
, 
not: ¬A
, 
all: ∀x:A. B[x]
, 
top: Top
, 
and: P ∧ Q
, 
prop: ℙ
, 
decidable: Dec(P)
, 
or: P ∨ Q
, 
nat_plus: ℕ+
, 
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w])
, 
so_apply: x[s1;s2;s3;s4]
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
so_lambda: so_lambda(x,y,z.t[x; y; z])
, 
so_apply: x[s1;s2;s3]
Latex:
\mforall{}[F,G,H,K,L,J,init:Top].
    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  X,s  =  s0 
                                                          in  case  X
                                                                  of  inl(P)  =>
                                                                  let  X',fs  =  P  a 
                                                                  in  let  b  \mleftarrow{}{}  G[fs;s]
                                                                        in  let  s'  \mleftarrow{}{}  J[b;s]
                                                                              in  <mk-hdf  <X',  K[s;s']>,  L[s;s']>
                                                                  |  inr(z)  =>
                                                                  H[mk-hdf;s;z])))) 
      <fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  F[a]  in  <mk-hdf,  out>)))),  init>  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.let\000C  out  \mleftarrow{}{}  F[a]
                                                                                                                                                            in  let  b  \mleftarrow{}{}  G[out;s]
                                                                                                                                                                  in  let  s'  \mleftarrow{}{}  J[b;s]
                                                                                                                                                                        in  <mk-hdf 
                                                                                                                                                                                K[s;s']
                                                                                                                                                                              ,  L[s;s']
                                                                                                                                                                              >)))) 
                                                                                                          init)
Date html generated:
2016_05_16-AM-10_51_33
Last ObjectModification:
2016_01_17-AM-11_09_34
Theory : halting!dataflow
Home
Index