---

Step * of Lemma bag-reduce_wf

∀[T:Type]. ∀[zero:T]. ∀[f:T ⟶ T ⟶ T].
  (∀[bs:bag(T)]. (bag-reduce(x,y.f[x;y];zero;bs) ∈ T)) supposing (Assoc(T;λx,y. f[x;y]) and Comm(T;λx,y. f[x;y]))
BY
{ (Auto THEN BagD (-1) THEN Auto THEN RepUR ``bag-reduce`` 0) }

1
1. T : Type
2. zero : T
3. f : T ⟶ T ⟶ T
4. Comm(T;λx,y. f[x;y])
5. Assoc(T;λx,y. f[x;y])
6. as : T List
7. bs : T List
8. permutation(T;as;bs)
⊢ reduce(λx,y. f[x;y];zero;as) = reduce(λx,y. f[x;y];zero;bs) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[zero:T].  \mforall{}[f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
    (\mforall{}[bs:bag(T)].  (bag-reduce(x,y.f[x;y];zero;bs)  \mmember{}  T))  supposing 
          (Assoc(T;\mlambda{}x,y.  f[x;y])  and 
          Comm(T;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(Auto  THEN  BagD  (-1)  THEN  Auto  THEN  RepUR  ``bag-reduce``  0)

---

Home Index