---

Step * of Lemma hdf-sqequal4

∀[F1,F2:Top].
  (fix((λmk-hdf.(inl (λa.let out ←─ F1[a]
                         in <mk-hdf, out>)))) || fix((λmk-hdf.(inl (λa.let out ←─ F2[a]
                                                                    in <mk-hdf, out>)))) 
  ~ fix((λmk-hdf.(inl (λa.let out1 ←─ F1[a]
                          in let out2 ←─ F2[a]
                             in let out ←─ out1 + out2
                                in <mk-hdf, out>)))))
BY
{ (Auto
   THEN RepUR ``hdf-parallel`` 0
   THEN SqequalInductionUsing' (UnrollLoopsOnceExcept [`bag-append`])⋅
   THEN Auto
   THEN RepeatFor 3 ((SqequalNNonCanonicalCD⋅ THEN Try (Complete (Auto))))
   THEN SqequalNCanonicalCD⋅
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:


\mforall{}[F1,F2:Top].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  F1[a]
                                                  in  <mk-hdf,  out>))))  ||  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out  \mleftarrow{}{}  F2[a]
                                                                                                                                        in  <mk-hdf,  out>)))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  out1  \mleftarrow{}{}  F1[a]
                                                    in  let  out2  \mleftarrow{}{}  F2[a]
                                                          in  let  out  \mleftarrow{}{}  out1  +  out2
                                                                in  <mk-hdf,  out>)))))


By

(Auto
  THEN  RepUR  ``hdf-parallel``  0
  THEN  SqequalInductionUsing'  (UnrollLoopsOnceExcept  [`bag-append`])\mcdot{}
  THEN  Auto
  THEN  RepeatFor  3  ((SqequalNNonCanonicalCD\mcdot{}  THEN  Try  (Complete  (Auto))))
  THEN  SqequalNCanonicalCD\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index