---

Step * of Lemma hdf-sqequal3

∀[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.<mk-hdf, F[a]>)))), s> ~ fix((λmk-hdf,s0. (inl (λa.let bs' ←─ G[F[a];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.<mk-hdf,  F[a]>)))),  s>  \msim{}  fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  G[F[a];s0]
                                                                                                                                                          in  <mk-hdf  K[s0;bs']
                                                                                                                                                                ,  L[s0;bs']
                                                                                                                                                                >)))) 
                                                                                                      s)


By

ProveSqFixpoints

---

Home Index