---

Step * 1 2 2 1 1 of Lemma permutation_inversion

.....subterm..... T:t
1:n
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. Inj(ℕ||as||;ℕ||as||;g)
11. i : ℕ
12. i < ||as||
⊢ i = ((f o g) i) ∈ ℤ
BY
{ (Reduce 0 THEN Symmetry THEN BackThruSomeHyp THEN Auto') }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;g)
11.  i  :  \mBbbN{}
12.  i  <  ||as||
\mvdash{}  i  =  ((f  o  g)  i)


By

---

Latex:
(Reduce  0  THEN  Symmetry  THEN  BackThruSomeHyp  THEN  Auto')

---

Home Index