---

Step * of Lemma hdf-compose1-transformation0

∀[f,F:Top].
  (f o fix((λmk-hdf.(inl (λa.<mk-hdf, F[a]>)))) 
  ~ fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.bag-map(f;F[a]);λout.<mk-hdf, out>;1))))))
BY
{ (Auto
   THEN RepUR ``simple-cbva-seq cbva-seq mk_lambdas`` 0
   THEN RepeatFor 2 ((RecUnfold `callbyvalueall-seq` 0⋅ THEN Reduce 0))) }

1
1. f : Top
2. F : Top
⊢ f o fix((λmk-hdf.(inl (λa.<mk-hdf, F[a]>)))) ~ fix((λmk-hdf.(inl (λa.let v ←─ bag-map(f;F[a])
                                                                       in <mk-hdf, v>))))

---

Latex:


\mforall{}[f,F:Top].
    (f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.<mk-hdf,  F[a]>)))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.bag-map(f;F[a]);\mlambda{}out.<mk-hdf,  out>1))))))


By

(Auto
  THEN  RepUR  ``simple-cbva-seq  cbva-seq  mk\_lambdas``  0
  THEN  RepeatFor  2  ((RecUnfold  `callbyvalueall-seq`  0\mcdot{}  THEN  Reduce  0)))

---

Home Index