---

Step * of Lemma hdf-return-transformation1

∀[x:Top]. (hdf-return(x) ~ fix((λmk-hdf.(inl (λa.cbva_seq(λx.⊥; λg.<inr ⋅ , x>; 0))))))
BY
{ (Auto
   THEN RepUR ``hdf-return cbva_seq hdf-run`` 0
   THEN RecUnfold `callbyvalueall_seq` 0
   THEN Reduce 0
   THEN UnrollLoopsOnce) }

---

Latex:

---

Latex:
\mforall{}[x:Top].  (hdf-return(x)  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}x.\mbot{};  \mlambda{}g.<inr  \mcdot{}  ,  x>  0))))))


By

---

Latex:
(Auto
  THEN  RepUR  ``hdf-return  cbva\_seq  hdf-run``  0
  THEN  RecUnfold  `callbyvalueall\_seq`  0
  THEN  Reduce  0
  THEN  UnrollLoopsOnce)

---

Home Index