---

Step * 1 1 of Lemma accum_list_cons_lemma


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])
BY
{ Try (RW (AddrC [2] (IdC)) 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{}  accumulate  (with  value  a  and  list  item  y):
      f[a;y]
    over  list:
        L
    with  starting  value:
      base[u])  \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  [2]  (IdC))  0)\mcdot{}

---

Home Index