---

Step * 1 of Lemma combine-list-permutation


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
BY
{ (InstLemma `permutation-invariant` [⌜A⌝;⌜λ2bs.permutation(A;as;bs)
                                           ⇒ (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A)⌝]⋅
   THENA 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)
9. b1 : A List
10. permutation(A;as;b1)
⊢ 0 < ||b1||

2
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)
9. as@0 : A List
10. a : A
11. permutation(A;as;[a / as@0]) ⇒ (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];[a / as@0]) ∈ A)
12. permutation(A;as;as@0 @ [a])
⊢ combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];as@0 @ [a]) ∈ A

3
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)
9. as@0 : A List
10. a1 : A
11. a2 : A
12. permutation(A;as;[a1; [a2 / as@0]])
⇒ (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];[a1; [a2 / as@0]]) ∈ A)
13. permutation(A;as;[a2; [a1 / as@0]])
⊢ combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];[a2; [a1 / as@0]]) ∈ A

4
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)
9. ∀as@0,bs:A List.
     (permutation(A;as@0;bs)
     ⇒ (permutation(A;as;as@0) ⇒ (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];as@0) ∈ A)
        ⇐⇒ permutation(A;as;bs) ⇒ (combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A)))
⊢ combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
3.  Assoc(A;\mlambda{}x,y.  f[x;y])
4.  Comm(A;\mlambda{}x,y.  f[x;y])
5.  as  :  A  List
6.  bs  :  A  List
7.  0  <  ||as||
8.  permutation(A;as;bs)
\mvdash{}  combine-list(x,y.f[x;y];as)  =  combine-list(x,y.f[x;y];bs)


By

---

Latex:
(InstLemma  `permutation-invariant`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bs.permutation(A;as;bs)
                                                                                  {}\mRightarrow{}  (combine-list(x,y.f[x;y];as)
                                                                                        =  combine-list(x,y.f[x;y];bs))\mkleeneclose{}]\mcdot{}
  THENA  Auto'
  )

---

Home Index