---

Step * of Lemma list-accum-append

∀[l1:Top List]. ∀[l2,b,f:Top].
  (list-accum(t,a,h.f[t;a;h];b;l1 @ l2) ~ list-accum(t,a,h.f[t;a;h];list-accum(t,a,h.f[t @ l2;a;h];b;l1);l2))
BY
{ (InductionOnList THEN Reduce 0 THEN Try (Complete (Auto)) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l1:Top  List].  \mforall{}[l2,b,f:Top].
    (list-accum(t,a,h.f[t;a;h];b;l1  @  l2)  \msim{}  list-accum(t,a,h.f[t;a;h];list-accum(t,a,h.f[t
    @  l2;a;h];b;l1);l2))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Try  (Complete  (Auto))  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index