---

Step * of Lemma accumulate_abort_cons_lemma

∀v,u,s,F:Top.
  (accumulate_abort(x,y.F[x;y];s;[u / v]) ~ let s' ⟵ case s of inl(y) => F[u;y] | inr(_) => s
                                            in accumulate_abort(x,y.F[x;y];s';v))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``accumulate_abort`` 0
   THEN RW (AddrC [1] (RecUnfoldC `eager-accum`)) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}v,u,s,F:Top.
    (accumulate\_abort(x,y.F[x;y];s;[u  /  v])  \msim{}  let  s'  \mleftarrow{}{}  case  s  of  inl(y)  =>  F[u;y]  |  inr($_\mbackslash{}ff\000C7b}$)  =>  s
                                                                                        in  accumulate\_abort(x,y.F[x;y];s';v))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``accumulate\_abort``  0
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `eager-accum`))  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index