Step * of Lemma list_accum_cons_lemma

y,x,z,f:Top.
  (accumulate (with value and list item b):
    f[a;b]
   over list:
     [x y]
   with starting value:
    z) accumulate (with value and list item b):
          f[a;b]
         over list:
           y
         with starting value:
          f[z;x]))
BY
((UnivCD THENA Auto) THEN Try (RW (AddrC [1] (RecUnfoldC `list_accum` ANDTHENC ReduceC)) 0)⋅}

1
1. Top
2. Top
3. Top
4. Top
⊢ accumulate (with value and list item b):
   f[a;b]
  over list:
    y
  with starting value:
   f[z;x]) accumulate (with value and list item b):
              f[a;b]
             over list:
               y
             with starting value:
              f[z;x])


Latex:


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


By


Latex:
((UnivCD  THENA  Auto)  THEN  Try  (RW  (AddrC  [1]  (RecUnfoldC  `list\_accum`  ANDTHENC  ReduceC))  0)\mcdot{})




Home Index