---

Step * of Lemma bag-val_wf

∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].  (Comm(T;+) ⇒ Assoc(T;+) ⇒ Ident(T;+;zero) ⇒ (bag-val(zero;+) ∈ bag(T) ⟶ T))
BY
{ (Auto THEN Unfold `bag-val` 0 THEN MemCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
1:n
1. T : Type
2. + : T ⟶ T ⟶ T
3. zero : T
4. Comm(T;+)
5. Assoc(T;+)
6. Ident(T;+;zero)
7. b : bag(T)
⊢ accumulate (with value v and list item x):
   v + x
  over list:
    b
  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{}  (bag-val(zero;+)  \mmember{}  bag(T)  {}\mrightarrow{}  T))


By

---

Latex:
(Auto  THEN  Unfold  `bag-val`  0  THEN  MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index