Step
*
1
1
1
1
of Lemma
flip-generators
1. n : ℕ
2. 1 < n
3. i : ℕn
4. j : ℕn
5. L : ℕn - 1 List
6. (i, j) = reduce(λi,g. ((i, i + 1) o g);λx.x;L) ∈ (ℕn ⟶ ℕn)
7. k : ℕn - 1
8. (k, k + 1) = (rot(n)^k o ((0, 1) o rot(n)^n - k)) ∈ (ℕn ⟶ ℕn)
⊢ (k, k + 1)
= reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;primrec(k;[];λi,l. (l @ [tt]))
@ [ff]
@ primrec(n - k;[];λi,l. (l @ [tt])))
∈ (ℕn ⟶ ℕn)
BY
{ (HypSubst (-1) 0 THEN Auto') }
1
1. n : ℕ
2. 1 < n
3. i : ℕn
4. j : ℕn
5. L : ℕn - 1 List
6. (i, j) = reduce(λi,g. ((i, i + 1) o g);λx.x;L) ∈ (ℕn ⟶ ℕn)
7. k : ℕn - 1
8. (k, k + 1) = (rot(n)^k o ((0, 1) o rot(n)^n - k)) ∈ (ℕn ⟶ ℕn)
⊢ (rot(n)^k o ((0, 1) o rot(n)^n - k))
= reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;primrec(k;[];λi,l. (l @ [tt]))
@ [ff]
@ primrec(n - k;[];λi,l. (l @ [tt])))
∈ (ℕn ⟶ ℕn)
Latex:
Latex:
1. n : \mBbbN{}
2. 1 < n
3. i : \mBbbN{}n
4. j : \mBbbN{}n
5. L : \mBbbN{}n - 1 List
6. (i, j) = reduce(\mlambda{}i,g. ((i, i + 1) o g);\mlambda{}x.x;L)
7. k : \mBbbN{}n - 1
8. (k, k + 1) = (rot(n)\^{}k o ((0, 1) o rot(n)\^{}n - k))
\mvdash{} (k, k + 1)
= reduce(\mlambda{}i,g. (if i then rot(n) else (0, 1) fi o g);\mlambda{}x.x;primrec(k;[];\mlambda{}i,l. (l @ [tt]))
@ [ff]
@ primrec(n - k;[];\mlambda{}i,l. (l @ [tt])))
By
Latex:
(HypSubst (-1) 0 THEN Auto')
Home
Index