---

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