Step
*
1
1
1
1
1
of Lemma
permutation-generators4
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n. (P[f] ⇒ P[f o (0, j)])
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]
12. ¬(i = 0 ∈ ℤ)
13. ¬(j = 0 ∈ ℤ)
14. x : ℕn
⊢ (f1 ((i, j) x)) = (f1 ((0, i) ((0, j) ((0, i) x)))) ∈ ℕn
BY
{ EqCDA }
1
.....subterm..... T:t
2:n
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n. (P[f] ⇒ P[f o (0, j)])
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]
12. ¬(i = 0 ∈ ℤ)
13. ¬(j = 0 ∈ ℤ)
14. x : ℕn
⊢ ((i, j) x) = ((0, i) ((0, j) ((0, i) x))) ∈ ℕn
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{}j:\mBbbN{}\msupplus{}n. (P[f] {}\mRightarrow{} P[f o (0, j)])
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]
12. \mneg{}(i = 0)
13. \mneg{}(j = 0)
14. x : \mBbbN{}n
\mvdash{} (f1 ((i, j) x)) = (f1 ((0, i) ((0, j) ((0, i) x))))
By
Latex:
EqCDA
Home
Index