Nuprl Lemma : hdf-sqequal6-1

  (fix((λmk-hdf,s0. (inl a.let bs' ←─ ∪b∈s0.[G[a;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]
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf base_wf strictness-apply bottom_diverge has-value_wf_base decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel fun_exp_unroll_1 bag-combine-unit-left-top bag-append-empty cons_wf top_wf nil_wf callbyvalueall-single-sqle2 int_subtype_base callbyvalueall-single-sqle
    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  \mcup{}b\mmember{}s0.[G[a;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: 2015_07_17-AM-08_17_14
Last ObjectModification: 2015_01_27-AM-11_51_19

Home Index