---

Step * of Lemma hdf-compose1-transformation1

∀[f,L:Base]. ∀[m:ℕ+].
  (f o fix((λmk-hdf.(inl (λa.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m))))) 
  ~ fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if (n =z m)
                                             then mk_lambdas(λout.bag-map(f;out);m - 1)
                                             else L[a] n
                                             fi ;λout.<mk-hdf, out>;m + 1))))))
BY
{ (Auto THEN RepUR ``hdf-compose1 mk-hdf`` 0) }

1
1. f : Base
2. L : Base
3. m : ℕ+
⊢ fix((λmk-hdf,s0. if hdf-halted(s0)
                  then hdf-halt()
                  else hdf-run(λa.let s1,b = let X',bs = s0(a) 
                                             in let out ←─ bag-map(f;bs)
                                                in <X', out> 
                                  in <mk-hdf s1, b>)
                  fi )) 
  fix((λmk-hdf.(inl (λa.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m))))) 
~ fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if (n =z m)
                                           then mk_lambdas(λout.bag-map(f;out);m - 1)
                                           else L[a] n
                                           fi ;λout.<mk-hdf, out>;m + 1)))))

---

Latex:


\mforall{}[f,L:Base].  \mforall{}[m:\mBbbN{}\msupplus{}].
    (f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L[a];\mlambda{}out.<mk-hdf,  out>m))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                          then  mk\_lambdas(\mlambda{}out.bag-map(f;out);m  -  1)
                                                                                          else  L[a]  n
                                                                                          fi  ;\mlambda{}out.<mk-hdf,  out>m  +  1))))))


By

(Auto  THEN  RepUR  ``hdf-compose1  mk-hdf``  0)

---

Home Index