Step
*
1
1
2
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 ∈ ℤ)
⊢ P[((f1 o (0, i)) o (0, j)) o (0, i)]
BY
{ RepeatFor 3 ((BHyp 4 THENW (Auto THEN Repeat ((BLemma `compose-injections` 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)} . ∀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 ∈ ℤ)
⊢ P[f1]
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)
\mvdash{} P[((f1 o (0, i)) o (0, j)) o (0, i)]
By
Latex:
RepeatFor 3 ((BHyp 4 THENW (Auto THEN Repeat ((BLemma `compose-injections` THEN Auto)))))
Home
Index