---

Step * 1 of Lemma bag-accum_wf


1. T : Type
2. S : Type
3. init : S
4. f : S ⟶ T ⟶ S
5. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
6. as : T List
7. bs : T List
8. permutation(T;as;bs)
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    as
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    bs
  with starting value:
   init)
∈ S
BY
{ ((InstLemma `permutation-invariant` [⌜T⌝;⌜λ2as.accumulate (with value v and list item x):
                                                  f[v;x]
                                                 over list:
                                                   as
                                                 with starting value:
                                                  init)
                                            = accumulate (with value v and list item x):
                                               f[v;x]
                                              over list:
                                                bs
                                              with starting value:
                                               init)
                                            ∈ S⌝]⋅
    THENA Auto
    )
   THEN (Try (((InstHyp [⌜as⌝;⌜bs⌝] (-1)⋅ THENA Auto) THEN BHyp -1  THEN Auto))
         THEN NthHypEq (-1)⋅
         THEN EqCD
         THEN Auto
         THEN ThinVar `bs'
         THEN ThinVar `as')⋅
   )⋅ }

1
1. T : Type
2. S : Type
3. init : S
4. f : S ⟶ T ⟶ S
5. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
6. a1 : T List
7. a : T
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    a1 @ [a]
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a / a1]
  with starting value:
   init)
∈ S

2
1. T : Type
2. S : Type
3. init : S
4. f : S ⟶ T ⟶ S
5. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
6. a1 : T List
7. a1@0 : T
8. a2 : T
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a2; [a1@0 / a1]]
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a1@0; [a2 / a1]]
  with starting value:
   init)
∈ S

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `permutation-invariant`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}as.accumulate  (with  value  v  and  list  item  x):
                                                                                                f[v;x]
                                                                                              over  list:
                                                                                                  as
                                                                                              with  starting  value:
                                                                                                init)
                                                                                    =  accumulate  (with  value  v  and  list  item  x):
                                                                                          f[v;x]
                                                                                        over  list:
                                                                                            bs
                                                                                        with  starting  value:
                                                                                          init)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (Try  (((InstHyp  [\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto))
              THEN  NthHypEq  (-1)\mcdot{}
              THEN  EqCD
              THEN  Auto
              THEN  ThinVar  `bs'
              THEN  ThinVar  `as')\mcdot{}
  )\mcdot{}

---

Home Index