Nuprl Lemma : hdf-sqequal2-cbva

  (fix((λmk-hdf,s0. case s0 of inl(y) => inl a.let X',bs in let out ⟵ G[bs] in <mk-hdf X', out>inr(z) => H[\000Cz])) 
   fix((λmk-hdf.(inl m.let out ⟵ F[m]
                         in <mk-hdf, out>)))) fix((λmk-hdf.(inl a.let out1 ⟵ F[a]
                                                                   in let out2 ⟵ G[out1]
                                                                      in <mk-hdf, out2>)))))


Definitions occuring in Statement :  callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top 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 so_apply: x[s] 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] top: Top so_apply: x[s1;s2] uimplies: supposing a so_lambda: λ2x.t[x] all: x:A. B[x] guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A prop: decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) nat: callbyvalueall: callbyvalueall ge: i ≥  sq_type: SQType(T)

    (fix((\mlambda{}mk-hdf,s0.  case  s0
                                        of  inl(y)  =>
                                        inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                        in  let  out  \mleftarrow{}{}  G[bs]
                                                              in  <mk-hdf  X',  out>)
                                        |  inr(z)  =>
      fix((\mlambda{}mk-hdf.(inl  (\mlambda{}m.let  out  \mleftarrow{}{}  F[m]
                                                  in  <mk-hdf,  out>))))  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out1  \mleftarrow{}{}  F[a]
                                                                                                                                      in  let  out2  \mleftarrow{}{}  G[out1]
                                                                                                                                            in  <mk-hdf,  out2>)))))

Date html generated: 2016_05_16-AM-10_45_01
Last ObjectModification: 2016_01_17-AM-11_13_10

Theory : halting!dataflow

Home Index