---

Step * of Lemma hdf-base-transformation2

∀[F:Top]. (hdf-base(m.F[m]) ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λx.⊥; λg.<mk-hdf Ax, F[a]>; 0))))) Ax)
BY
{ (Auto
   THEN RepUR ``hdf-base mk-hdf cbva_seq hdf-run it`` 0
   THEN RecUnfold `callbyvalueall_seq` 0
   THEN Reduce 0
   THEN SqequalSqle
   THEN OneFixpointLeast
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Try (Complete (Auto))
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
   THEN Reduce 0
   THEN RW (AddrC [2] UnrollLoopsOnceC) 0
   THEN Auto) }

---

Latex:


\mforall{}[F:Top].  (hdf-base(m.F[m])  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}x.\mbot{};  \mlambda{}g.<mk-hdf  Ax,  F[a]>  0)))))  A\000Cx)


By

(Auto
  THEN  RepUR  ``hdf-base  mk-hdf  cbva\_seq  hdf-run  it``  0
  THEN  RecUnfold  `callbyvalueall\_seq`  0
  THEN  Reduce  0
  THEN  SqequalSqle
  THEN  OneFixpointLeast
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RW  (AddrC  [2]  UnrollLoopsOnceC)  0
  THEN  Auto)

---

Home Index