---

Step * 1 of Lemma permutation_inversion


1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
⊢ ∃f@0:ℕ||as|| ⟶ ℕ||as||. (Inj(ℕ||as||;ℕ||as||;f@0) ∧ (as = (as o f o f@0) ∈ (A List)))
BY
{ Assert ⌜∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)⌝⋅ }

1
.....assertion..... 
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
⊢ ∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)

2
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
8. ∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
⊢ ∃f@0:ℕ||as|| ⟶ ℕ||as||. (Inj(ℕ||as||;ℕ||as||;f@0) ∧ (as = (as o f o f@0) ∈ (A List)))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  as  :  A  List
3.  bs  :  A  List
4.  f  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
5.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
6.  bs  =  (as  o  f)
7.  ||as||  =  ||bs||
\mvdash{}  \mexists{}f@0:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||.  (Inj(\mBbbN{}||as||;\mBbbN{}||as||;f@0)  \mwedge{}  (as  =  (as  o  f  o  f@0)))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}g:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)\mkleeneclose{}\mcdot{}

---

Home Index