---

Step * 1 2 1 1 2 of Lemma permutation-generators5


1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i:ℕn - 1.  (P[f] ⇒ P[f o (i, i + 1)])
5. d : ℤ
6. [%5] : 0 < d
7. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing (¬(i = j ∈ ℤ)) ∧ (|i - j| ≤ ((d - 1) + 1))
8. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
9. i : ℕn
10. j : ℕn
11. i < j
12. |i - j| ≤ (d + 1)
13. P[f]
14. ¬(i = (j - 1) ∈ ℤ)
⊢ P[f o (i, j)]
BY
{ (Subst ⌜(f o (i, j)) = (((f o (j, j - 1)) o (i, j - 1)) o (j, j - 1)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⌝ 0⋅ THENW Auto) }

1
.....equality..... 
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i:ℕn - 1.  (P[f] ⇒ P[f o (i, i + 1)])
5. d : ℤ
6. 0 < d
7. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing (¬(i = j ∈ ℤ)) ∧ (|i - j| ≤ ((d - 1) + 1))
8. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
9. i : ℕn
10. j : ℕn
11. i < j
12. |i - j| ≤ (d + 1)
13. P[f]
14. ¬(i = (j - 1) ∈ ℤ)
⊢ (f o (i, j)) = (((f o (j, j - 1)) o (i, j - 1)) o (j, j - 1)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 

2
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i:ℕn - 1.  (P[f] ⇒ P[f o (i, i + 1)])
5. d : ℤ
6. [%5] : 0 < d
7. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing (¬(i = j ∈ ℤ)) ∧ (|i - j| ≤ ((d - 1) + 1))
8. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
9. i : ℕn
10. j : ℕn
11. i < j
12. |i - j| ≤ (d + 1)
13. P[f]
14. ¬(i = (j - 1) ∈ ℤ)
⊢ P[((f o (j, j - 1)) o (i, j - 1)) o (j, j - 1)]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  [P]  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}
3.  P[\mlambda{}x.x]
4.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}i:\mBbbN{}n  -  1.    (P[f]  {}\mRightarrow{}  P[f  o  (i,  i  +  1)])
5.  d  :  \mBbbZ{}
6.  [\%5]  :  0  <  d
7.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}i,j:\mBbbN{}n.
          P[f]  {}\mRightarrow{}  P[f  o  (i,  j)]  supposing  (\mneg{}(i  =  j))  \mwedge{}  (|i  -  j|  \mleq{}  ((d  -  1)  +  1))
8.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
9.  i  :  \mBbbN{}n
10.  j  :  \mBbbN{}n
11.  i  <  j
12.  |i  -  j|  \mleq{}  (d  +  1)
13.  P[f]
14.  \mneg{}(i  =  (j  -  1))
\mvdash{}  P[f  o  (i,  j)]


By

---

Latex:
(Subst  \mkleeneopen{}(f  o  (i,  j))  =  (((f  o  (j,  j  -  1))  o  (i,  j  -  1))  o  (j,  j  -  1))\mkleeneclose{}  0\mcdot{}  THENW  Auto)

---

Home Index