---

Step * 1 1 1 of Lemma bag-accum_wf


1. T : Type
2. S : Type
3. f : S ⟶ T ⟶ S
4. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
5. a : T
6. u : T
7. v : T List
8. ∀init:S
     (accumulate (with value v and list item x):
       f[v;x]
      over list:
        v @ [a]
      with starting value:
       init)
     = accumulate (with value v and list item x):
        f[v;x]
       over list:
         [a / v]
       with starting value:
        init)
     ∈ S)
9. init : S
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    v @ [a]
  with starting value:
   f[init;u])
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    v
  with starting value:
   f[f[init;a];u])
∈ S
BY
{ ((RWO "-2" 0 THEN Auto) THEN Reduce 0 THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  f  :  S  {}\mrightarrow{}  T  {}\mrightarrow{}  S
4.  \mforall{}v:S.  \mforall{}x,y:T.    (f[f[v;y];x]  =  f[f[v;x];y])
5.  a  :  T
6.  u  :  T
7.  v  :  T  List
8.  \mforall{}init:S
          (accumulate  (with  value  v  and  list  item  x):
              f[v;x]
            over  list:
                v  @  [a]
            with  starting  value:
              init)
          =  accumulate  (with  value  v  and  list  item  x):
                f[v;x]
              over  list:
                  [a  /  v]
              with  starting  value:
                init))
9.  init  :  S
\mvdash{}  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        v  @  [a]
    with  starting  value:
      f[init;u])
=  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        v
    with  starting  value:
      f[f[init;a];u])


By

---

Latex:
((RWO  "-2"  0  THEN  Auto)  THEN  Reduce  0  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index