---

Step * of Lemma iterate-rotate

∀[n,k:ℕ].  (rot(n)^k = (λx.(x + k rem n)) ∈ (ℕn ⟶ ℕn))
BY
{ ((D 0 THENA Auto) THEN Assert ⌜∀x:ℕn. ∀k:ℕ.  (x + k rem n ∈ ℕn)⌝⋅) }

1
.....assertion..... 
1. n : ℕ
⊢ ∀x:ℕn. ∀k:ℕ.  (x + k rem n ∈ ℕn)

2
1. n : ℕ
2. ∀x:ℕn. ∀k:ℕ.  (x + k rem n ∈ ℕn)
⊢ ∀[k:ℕ]. (rot(n)^k = (λx.(x + k rem n)) ∈ (ℕn ⟶ ℕn))

---

Latex:

---

Latex:
\mforall{}[n,k:\mBbbN{}].    (rot(n)\^{}k  =  (\mlambda{}x.(x  +  k  rem  n)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}\mforall{}x:\mBbbN{}n.  \mforall{}k:\mBbbN{}.    (x  +  k  rem  n  \mmember{}  \mBbbN{}n)\mkleeneclose{}\mcdot{})

---

Home Index