---

Step * 1 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. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j)
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f])
7. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
8. i : ℕn
9. j : ℕn
10. i < j
11. P[f1]
⊢ P[f1 o (i, j)]
BY
{ ((Assert ⌜∀d:ℕ. ∀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))⌝⋅
   THENM (InstHyp [⌜|i - j|⌝;⌜f1⌝;⌜i⌝;⌜j⌝] (-1)⋅ THEN Auto)
   )
   THEN RepeatFor 7 (Thin (-1))
   THEN (InductionOnNat THENW (Auto THEN BLemma `compose-injections` THEN Auto))
   THEN Auto) }

1
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. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. i : ℕn
7. j : ℕn
8. ¬(i = j ∈ ℤ)
9. |i - j| ≤ (0 + 1)
10. P[f]
⊢ P[f o (i, j)]

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]
⊢ P[f o (i, j)]

---

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.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
6.  (\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  i  <  j)
{}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f])
7.  f1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
8.  i  :  \mBbbN{}n
9.  j  :  \mBbbN{}n
10.  i  <  j
11.  P[f1]
\mvdash{}  P[f1  o  (i,  j)]


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \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))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}|i  -  j|\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  RepeatFor  7  (Thin  (-1))
  THEN  (InductionOnNat  THENW  (Auto  THEN  BLemma  `compose-injections`  THEN  Auto))
  THEN  Auto)

---

Home Index