Nuprl Lemma : hdf-sqequal6-2

  (fix((λmk-hdf,s0. (inl a.let bs' ⟵ ⋃f∈b.[G[a;b]]].⋃b∈s0.f b
                             in <mk-hdf case null(bs') of inl() => s0 inr() => bs', F[s0;bs']>)))) 
   [s] fix((λmk-hdf,s0. (inl a.let bs' ⟵ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)


Definitions occuring in Statement :  null: null(as) cons: [a b] nil: [] callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x sqequal: t bag-combine: x∈bs.f[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top and: P ∧ Q prop: fun_exp: f^n primrec: primrec(n;b;c) decidable: Dec(P) or: P ∨ Q nat_plus: + so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B null: null(as) cons: [a b] bfalse: ff so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]

    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}[\mlambda{}b.[G[a;b]]].\mcup{}b\mmember{}s0.f  b
                                                          in  <mk-hdf  case  null(bs')  of  inl()  =>  s0  |  inr()  =>  bs',  F[s0;bs']>))))\000C 
      [s]  \msim{}  fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  G[a;s0]  in  <mk-hdf  bs',  F[[s0];[bs']]>))))  s)

Date html generated: 2016_05_16-AM-10_51_28
Last ObjectModification: 2016_01_17-AM-11_09_25

Theory : halting!dataflow

Home Index