---

Step * 1 2 1 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|| ∈ ℤ
8. g : ℕ||as|| ⟶ ℕ||as||
9. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
10. a1 : ℕ||as||
11. a2 : ℕ||as||
12. (g a1) = (g a2) ∈ ℕ||as||
⊢ a1 = a2 ∈ ℕ||as||
BY
{ (ApFunToHypEquands `Z' ⌜f Z⌝ ⌜ℕ||as||⌝ (-1) ⋅ THEN Auto) }

1
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||
9. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
10. a1 : ℕ||as||
11. a2 : ℕ||as||
12. (g a1) = (g a2) ∈ ℕ||as||
13. (f (g a1)) = (f (g a2)) ∈ ℕ||as||
⊢ a1 = a2 ∈ ℕ||as||

---

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||
8.  g  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
9.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)
10.  a1  :  \mBbbN{}||as||
11.  a2  :  \mBbbN{}||as||
12.  (g  a1)  =  (g  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}f  Z\mkleeneclose{}  \mkleeneopen{}\mBbbN{}||as||\mkleeneclose{}  (-1)  \mcdot{}  THEN  Auto)

---

Home Index