---

Step * of Lemma bag-val-append

∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].
  (Comm(T;+)
  ⇒ Assoc(T;+)
  ⇒ Ident(T;+;zero)
  ⇒ (∀[as,bs:bag(T)].  ((bag-val(zero;+) (as + bs)) = ((bag-val(zero;+) as) + (bag-val(zero;+) bs)) ∈ T)))
BY
{ (Auto
   THEN BagD (-2)
   THEN Auto
   THEN (Assert as = v1 ∈ bag(T) BY
               (EqTypeCD THEN Auto))
   THEN (HypSubst' (-1) 0
         THEN Auto
         THEN ThinVar `as'
         THEN RenameVar `as' (-1)
         THEN RepUR ``bag-val bag-append`` 0
         THEN (RWO "list_accum_append" 0 THENA Auto))⋅) }

1
1. T : Type
2. + : T ⟶ T ⟶ T
3. zero : T
4. Comm(T;+)
5. Assoc(T;+)
6. Ident(T;+;zero)
7. bs : bag(T)
8. as : T List
⊢ accumulate (with value v and list item x):
   v + x
  over list:
    bs
  with starting value:
   accumulate (with value v and list item x):
    v + x
   over list:
     as
   with starting value:
    zero))
= (accumulate (with value v and list item x):
    v + x
   over list:
     as
   with starting value:
    zero) 
   + 
   accumulate (with value v and list item x):
    v + x
   over list:
     bs
   with starting value:
    zero))
∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[+:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[zero:T].
    (Comm(T;+)
    {}\mRightarrow{}  Assoc(T;+)
    {}\mRightarrow{}  Ident(T;+;zero)
    {}\mRightarrow{}  (\mforall{}[as,bs:bag(T)].
                ((bag-val(zero;+)  (as  +  bs))  =  ((bag-val(zero;+)  as)  +  (bag-val(zero;+)  bs)))))


By

---

Latex:
(Auto
  THEN  BagD  (-2)
  THEN  Auto
  THEN  (Assert  as  =  v1  BY
                          (EqTypeCD  THEN  Auto))
  THEN  (HypSubst'  (-1)  0
              THEN  Auto
              THEN  ThinVar  `as'
              THEN  RenameVar  `as'  (-1)
              THEN  RepUR  ``bag-val  bag-append``  0
              THEN  (RWO  "list\_accum\_append"  0  THENA  Auto))\mcdot{})

---

Home Index