---

Step * 1 of Lemma accum_list_cons_lemma


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])
BY
{ Try (RW (AddrC [1] (UnfoldC `accum_list` ANDTHENC ReduceC)) 0)⋅ }

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

---

Latex:

---

Latex:

1.  L  :  Top@i
2.  u  :  Top@i
3.  base  :  Top@i
4.  f  :  Top@i
\mvdash{}  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:
Try  (RW  (AddrC  [1]  (UnfoldC  `accum\_list`  ANDTHENC  ReduceC))  0)\mcdot{}

---

Home Index