---

Step * of Lemma rotate-injection

∀[n:ℕ]. Inj(ℕn;ℕn;rot(n))
BY
{ (Auto THEN D 0 THEN Auto THEN RepUR ``rotate`` (-1)) }

1
1. n : ℕ
2. a1 : ℕn
3. a2 : ℕn
4. if (a1 =z n - 1) then 0 else a1 + 1 fi  = if (a2 =z n - 1) then 0 else a2 + 1 fi  ∈ ℕn
⊢ a1 = a2 ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  Inj(\mBbbN{}n;\mBbbN{}n;rot(n))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RepUR  ``rotate``  (-1))

---

Home Index