---

Step * of Lemma flip-conjugate-rotate

∀[n:ℕ]. ∀[i:ℕn - 1].  ((i, i + 1) = (rot(n)^i o ((0, 1) o rot(n)^n - i)) ∈ (ℕn ⟶ ℕn))
BY
{ TACTIC:(Auto
          THEN (Assert i ∈ ℕn BY
                      Auto)
          THEN (Assert i + 1 ∈ ℕn BY
                      Auto)
          THEN Ext
          THEN Reduce 0
          THEN Auto
          THEN (InstLemma `iterated-rotate` [⌜n⌝;⌜i⌝]⋅ THENA Auto')
          THEN InstLemma `iterated-rotate` [⌜n⌝;⌜n - i⌝]⋅
          THEN Auto') }

1
1. n : ℕ
2. i : ℕn - 1
3. i ∈ ℕn
4. i + 1 ∈ ℕn
5. x : ℕn
6. rot(n)^i = (λx.if x + i <z n then x + i else (x + i) - n fi ) ∈ (ℕn ⟶ ℕn)
7. rot(n)^n - i = (λx.if x + (n - i) <z n then x + (n - i) else (x + (n - i)) - n fi ) ∈ (ℕn ⟶ ℕn)
⊢ ((i, i + 1) x) = (rot(n)^i ((0, 1) (rot(n)^n - i x))) ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n  -  1].    ((i,  i  +  1)  =  (rot(n)\^{}i  o  ((0,  1)  o  rot(n)\^{}n  -  i)))


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  i  \mmember{}  \mBbbN{}n  BY
                                        Auto)
                THEN  (Assert  i  +  1  \mmember{}  \mBbbN{}n  BY
                                        Auto)
                THEN  Ext
                THEN  Reduce  0
                THEN  Auto
                THEN  (InstLemma  `iterated-rotate`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto')
                THEN  InstLemma  `iterated-rotate`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n  -  i\mkleeneclose{}]\mcdot{}
                THEN  Auto')

---

Home Index