Nuprl Lemma : hdf-sqequal6

  (fix((λmk-hdf,s0. (inl a.let bs' ⟵ reduce(λl,l'. (l l');[];map(λb.[G[a;b]];s0))
                             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) map: map(f;as) append: as bs reduce: reduce(f;k;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
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: + append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] 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{}{}  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}b.[G[a;b]];s0))
                                                          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_19
Last ObjectModification: 2016_01_17-AM-11_09_12

Theory : halting!dataflow

Home Index