---

Step * 1 1 of Lemma rotate-surjection


1. n : ℕ+
2. (rot(n) o rot(n)^n - 1) = (λx.x) ∈ (ℕn ⟶ ℕn)
3. b : ℕn
⊢ ∃a:ℕn. ((rot(n) a) = b ∈ ℕn)
BY
{ ((ApFunToHypEquands `Z' ⌜Z b⌝ ⌜ℕn⌝ 2⋅ THENA Auto) THEN Reduce -1 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  (rot(n)  o  rot(n)\^{}n  -  1)  =  (\mlambda{}x.x)
3.  b  :  \mBbbN{}n
\mvdash{}  \mexists{}a:\mBbbN{}n.  ((rot(n)  a)  =  b)


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  b\mkleeneclose{}  \mkleeneopen{}\mBbbN{}n\mkleeneclose{}  2\mcdot{}  THENA  Auto)  THEN  Reduce  -1  THEN  Auto)

---

Home Index