Nuprl Lemma : hdf-sqequal3-cbva

[F,G,H,K,L,s:Top].
  (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) =>
                        H[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']>)))) 
                                                  s)


Proof




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
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf base_wf fun_exp0_lemma strictness-apply bottom_diverge has-value_wf_base exception-not-bottom 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 lifting-strict-callbyvalueall strict4-spread top_wf
\mforall{}[F,G,H,K,L,s:Top].
    (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)  =>
                                                H[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']
                                                                                                                                                                    >)))) 
                                                                                                    s)



Date html generated: 2015_07_17-AM-08_16_58
Last ObjectModification: 2015_04_30-AM-11_01_52

Home Index