---

Step * of Lemma reduce-permutation

∀[A:Type]. ∀[f:A ⟶ A ⟶ A]. ∀[e:A].
  (∀[as,bs:A List].  reduce(f;e;as) = reduce(f;e;bs) ∈ A supposing permutation(A;as;bs)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))
BY
{ (Auto
   THEN (InstLemma `reduce-as-combine-list` [⌜A⌝;⌜f⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THEN Auto)
   THEN BLemma `combine-list-permutation`
   THEN Auto') }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. e : A
4. Assoc(A;λx,y. f[x;y])
5. Comm(A;λx,y. f[x;y])
6. as : A List
7. bs : A List
8. permutation(A;as;bs)
9. ∀[L:A List]. ∀[z:A].  (reduce(f;z;L) = combine-list(x,y.f[x;y];[z / L]) ∈ A)
⊢ permutation(A;[e / as];[e / bs])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[e:A].
    (\mforall{}[as,bs:A  List].    reduce(f;e;as)  =  reduce(f;e;bs)  supposing  permutation(A;as;bs))  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(Auto
  THEN  (InstLemma  `reduce-as-combine-list`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THEN  Auto)
  THEN  BLemma  `combine-list-permutation`
  THEN  Auto')

---

Home Index