---

Step * of Lemma combine-list-permutation

∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[as,bs:A List].
     (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A) supposing 
        (permutation(A;as;bs) and 
        0 < ||as||)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))
BY
{ Auto }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. Assoc(A;λx,y. f[x;y])
4. Comm(A;λx,y. f[x;y])
5. as : A List
6. bs : A List
7. 0 < ||as||
8. permutation(A;as;bs)
⊢ combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as,bs:A  List].
          (combine-list(x,y.f[x;y];as)  =  combine-list(x,y.f[x;y];bs))  supposing 
                (permutation(A;as;bs)  and 
                0  <  ||as||))  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
Auto

---

Home Index