---

Step * of Lemma hdf-sqequal7

∀[F,G,H,K,L,J,init:Top].
  (fix((λmk-hdf,s0. (inl (λa.let X,s = s0 
                             in case X
                                 of inl(P) =>
                                 let X',fs = P a 
                                 in let b ←─ G[fs;s]
                                    in let s' ←─ J[b;s]
                                       in <mk-hdf <X', K[s;s']>, L[s;s']>
                                 | inr(z) =>
                                 H[mk-hdf;s;z])))) 
   <fix((λmk-hdf.(inl (λa.let out ←─ F[a] in <mk-hdf, out>)))), init> ~ fix((λmk-hdf,s. (inl (λa.let out ←─ F[a]
                                                                              in let b ←─ G[out;s]
                                                                                 in let s' ←─ J[b;s]
                                                                                    in <mk-hdf K[s;s'], L[s;s']>)))) 
                                                     init)
BY
{ ProveSqFixpoints }

---

Latex:


\mforall{}[F,G,H,K,L,J,init:Top].
    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  X,s  =  s0 
                                                          in  case  X
                                                                  of  inl(P)  =>
                                                                  let  X',fs  =  P  a 
                                                                  in  let  b  \mleftarrow{}{}  G[fs;s]
                                                                        in  let  s'  \mleftarrow{}{}  J[b;s]
                                                                              in  <mk-hdf  <X',  K[s;s']>,  L[s;s']>
                                                                  |  inr(z)  =>
                                                                  H[mk-hdf;s;z])))) 
      <fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  F[a]  in  <mk-hdf,  out>)))),  init>  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.let\000C  out  \mleftarrow{}{}  F[a]
                                                                                                                                                            in  let  b  \mleftarrow{}{}  G[out;s]
                                                                                                                                                                  in  let  s'  \mleftarrow{}{}  J[b;s]
                                                                                                                                                                        in  <mk-hdf 
                                                                                                                                                                                K[s;s']
                                                                                                                                                                              ,  L[s;s']
                                                                                                                                                                              >)))) 
                                                                                                          init)


By

ProveSqFixpoints

---

Home Index