---

Step * 1 of Lemma reduce-permutation


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])
BY
{ (InstLemma `append_functionality_wrt_permutation` [⌜A⌝;⌜[e]⌝;⌜as⌝;⌜[e]⌝;⌜bs⌝]⋅
   THEN Auto
   THEN BLemma `permutation_weakening`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
3.  e  :  A
4.  Assoc(A;\mlambda{}x,y.  f[x;y])
5.  Comm(A;\mlambda{}x,y.  f[x;y])
6.  as  :  A  List
7.  bs  :  A  List
8.  permutation(A;as;bs)
9.  \mforall{}[L:A  List].  \mforall{}[z:A].    (reduce(f;z;L)  =  combine-list(x,y.f[x;y];[z  /  L]))
\mvdash{}  permutation(A;[e  /  as];[e  /  bs])


By

---

Latex:
(InstLemma  `append\_functionality\_wrt\_permutation`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[e]\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}[e]\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  BLemma  `permutation\_weakening`
  THEN  Auto)\mcdot{}

---

Home Index