Nuprl Lemma : hdf-sqequal3-cbva

  (fix((λmk-hdf,s0. let X,bs s0 
                    in case X
                        of inl(y) =>
                        inl a.let X',fs 
                                in let bs' ⟵ G[fs;bs]
                                   in <mk-hdf <X', K[bs;bs']>L[bs;bs']>)
                        inr(z) =>
   <fix((λmk-hdf.(inl a.let out ⟵ F[a] in <mk-hdf, out>)))), s> fix((λmk-hdf,s0. (inl a.let out ⟵ F[a]
                                                                            in let bs' ⟵ G[out;s0]
                                                                               in <mk-hdf K[s0;bs'], L[s0;bs']>)))) 


Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] apply: a fix: fix(F) lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: 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: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s]

    (fix((\mlambda{}mk-hdf,s0.  let  X,bs  =  s0 
                                        in  case  X
                                                of  inl(y)  =>
                                                inl  (\mlambda{}a.let  X',fs  =  y  a 
                                                                in  let  bs'  \mleftarrow{}{}  G[fs;bs]
                                                                      in  <mk-hdf  <X',  K[bs;bs']>,  L[bs;bs']>)
                                                |  inr(z)  =>
      <fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  F[a]  in  <mk-hdf,  out>)))),  s>  \msim{}  fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  o\000Cut  \mleftarrow{}{}  F[a]
                                                                                                                                                        in  let  bs'  \mleftarrow{}{}  G[out;s0]
                                                                                                                                                              in  <mk-hdf  K[s0;bs']
                                                                                                                                                                    ,  L[s0;bs']

Date html generated: 2016_05_16-AM-10_50_56
Last ObjectModification: 2016_01_17-AM-11_09_21

Theory : halting!dataflow

Home Index