---

Step * of Lemma append_functionality_wrt_permutation

∀[A:Type]
  ∀as1,as2,bs1,bs2:A List.  (permutation(A;as1;bs1) ⇒ permutation(A;as2;bs2) ⇒ permutation(A;as1 @ as2;bs1 @ bs2))
BY
{ (Auto THEN RepeatFor 2 ((FLemma `permutation-length` [-2] THENA Auto)) THEN All (Unfold `permutation`)⋅ THEN ExRepD) }

1
1. [A] : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
⊢ ∃f:ℕ||as1 @ as2|| ⟶ ℕ||as1 @ as2||
   (Inj(ℕ||as1 @ as2||;ℕ||as1 @ as2||;f) ∧ ((bs1 @ bs2) = (as1 @ as2 o f) ∈ (A List)))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}as1,as2,bs1,bs2:A  List.
        (permutation(A;as1;bs1)  {}\mRightarrow{}  permutation(A;as2;bs2)  {}\mRightarrow{}  permutation(A;as1  @  as2;bs1  @  bs2))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((FLemma  `permutation-length`  [-2]  THENA  Auto))
  THEN  All
  (Unfold  `permutation`)\mcdot{}
  THEN  ExRepD)

---

Home Index