---

Step * of 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)
BY
{ ProveSqFixpoints }

---

Latex:


\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)


By

ProveSqFixpoints

---

Home Index