---

Step * 1 1 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. i : ℕn
7. j : ℕn
8. ¬(i = j ∈ ℤ)
9. ((-(0 + 1)) ≤ (i - j)) ∧ ((i - j) ≤ (0 + 1))
10. P[f]
⊢ P[f o (i, j)]
BY
{ ((Decide ⌜j = (i + 1) ∈ ℤ⌝⋅ THENA Auto)
   THENL [(HypSubst' (-1) 0 THEN BackThruSomeHyp THEN Auto)
         ; ((Subst' i = (j + 1) ∈ ℤ 0 THENA Auto)
            THEN Subst' (f o (j + 1, j)) = (f o (j, j + 1)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  0
            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. (-(0 + 1)) ≤ (i - j)
10. (i - j) ≤ (0 + 1)
11. P[f]
12. ¬(j = (i + 1) ∈ ℤ)
⊢ (f o (j + 1, j)) = (f o (j, j + 1)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 

---

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.  i  :  \mBbbN{}n
7.  j  :  \mBbbN{}n
8.  \mneg{}(i  =  j)
9.  ((-(0  +  1))  \mleq{}  (i  -  j))  \mwedge{}  ((i  -  j)  \mleq{}  (0  +  1))
10.  P[f]
\mvdash{}  P[f  o  (i,  j)]


By

---

Latex:
((Decide  \mkleeneopen{}j  =  (i  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(HypSubst'  (-1)  0  THEN  BackThruSomeHyp  THEN  Auto)
              ;  ((Subst'  i  =  (j  +  1)  0  THENA  Auto)
                    THEN  Subst'  (f  o  (j  +  1,  j))  =  (f  o  (j,  j  +  1))  0
                    THEN  Auto)]
)

---

Home Index