Step
*
of Lemma
flip-generators
∀n:ℕ
∀i,j:ℕn. ∃L:𝔹 List. ((i, j) = reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) ∈ (ℕn ⟶ ℕn)) supposing 1 <\000C n
BY
{ TACTIC:(InstLemma `flip-adjacent` []
THEN ParallelLast'
THEN (D 0 THENA Auto)
THEN PromoteHyp (-1) 2
THEN RepeatFor 2 (ParallelLast')
THEN ExRepD) }
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)
⊢ ∃L:𝔹 List. ((i, j) = reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) ∈ (ℕn ⟶ ℕn))
Latex:
Latex:
\mforall{}n:\mBbbN{}
\mforall{}i,j:\mBbbN{}n. \mexists{}L:\mBbbB{} List. ((i, j) = reduce(\mlambda{}i,g. (if i then rot(n) else (0, 1) fi o g);\mlambda{}x.x;L))
supposing 1 < n
By
Latex:
TACTIC:(InstLemma `flip-adjacent` []
THEN ParallelLast'
THEN (D 0 THENA Auto)
THEN PromoteHyp (-1) 2
THEN RepeatFor 2 (ParallelLast')
THEN ExRepD)
Home
Index