Step
*
1
1
1
2
2
1
2
1
1
2
of Lemma
permutation-generators
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. L : 𝔹 List
14. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L))
⊢ P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) o f1]
BY
{ ListInd' (-2) }
1
.....wf.....
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L))
⊢ λL.P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) o f1] ∈ (𝔹 List) ⟶ ℙ
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)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L))
⊢ P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;[]) o f1]
3
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L))
14. u : 𝔹
15. v : 𝔹 List
16. P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;v) o f1]
⊢ P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;[u / v]) o f1]
4
.....wf.....
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L))
14. u : 𝔹
15. v : 𝔹 List
⊢ P[reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;v) o 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)\} . (P[f] {}\mRightarrow{} P[(0, 1) o f]) supposing 1 < n
5. \mforall{}f:\{f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;f)\} . (P[f] {}\mRightarrow{} P[rot(n) o f])
6. f : \{f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;f)\}
7. i : \mBbbN{}n
8. j : \mBbbN{}n
9. f1 : \{f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;f)\}
10. P[f1]
11. \mneg{}(n = 0)
12. \mneg{}(n = 1)
13. L : \mBbbB{} List
14. \mforall{}L:\mBbbB{} List. Inj(\mBbbN{}n;\mBbbN{}n;reduce(\mlambda{}i,g. (if i then rot(n) else (0, 1) fi o g);\mlambda{}x.x;L))
\mvdash{} P[reduce(\mlambda{}i,g. (if i then rot(n) else (0, 1) fi o g);\mlambda{}x.x;L) o f1]
By
Latex:
ListInd' (-2)
Home
Index