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 = y a 
                                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: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x,  sqequal: s ~ 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