---

Step * of Lemma accum_list_cons_lemma

∀L,u,base,f:Top.
  (accum_list(a,x.f[a;x]; y.base[y]; [u / L]) ~ accumulate (with value a and list item y):
                                                 f[a;y]
                                                over list:
                                                  L
                                                with starting value:
                                                 base[u]))
BY
{ (UnivCD THENA Auto) }

1
1. L : Top@i
2. u : Top@i
3. base : Top@i
4. f : Top@i
⊢ accum_list(a,x.f[a;x]; y.base[y]; [u / L]) ~ accumulate (with value a and list item y):
                                                f[a;y]
                                               over list:
                                                 L
                                               with starting value:
                                                base[u])

---

Latex:

---

Latex:
\mforall{}L,u,base,f:Top.
    (accum\_list(a,x.f[a;x];  y.base[y];  [u  /  L])  \msim{}  accumulate  (with  value  a  and  list  item  y):
                                                                                                  f[a;y]
                                                                                                over  list:
                                                                                                    L
                                                                                                with  starting  value:
                                                                                                  base[u]))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index