Step
*
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)
⊢ ∃L:𝔹 List. ((k, k + 1) = reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) ∈ (ℕn ⟶ ℕn))
BY
{ (InstConcl [⌜primrec(k;[];λi,l. (l @ [tt])) @ [ff] @ primrec(n - k;[];λi,l. (l @ [tt]))⌝]⋅ 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)
⊢ (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)
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{} \mexists{}L:\mBbbB{} List. ((k, k + 1) = reduce(\mlambda{}i,g. (if i then rot(n) else (0, 1) fi o g);\mlambda{}x.x;L))
By
Latex:
(InstConcl [\mkleeneopen{}primrec(k;[];\mlambda{}i,l. (l @ [tt])) @ [ff] @ primrec(n - k;[];\mlambda{}i,l. (l @ [tt]))\mkleeneclose{}]\mcdot{} THEN Auto\000C')
Home
Index