---

Step * 2 1 1 of Lemma rotate-by-id


1. n : ℕ
2. i : ℕ
3. x : ℕn
4. (i rem n) = 0 ∈ ℤ
⊢ (x + i rem n) = x ∈ ℕn
BY
{ ((InstLemma `rem_addition` [⌜x⌝;⌜i⌝;⌜n⌝]⋅ THEN Auto) THEN HypSubst' (-2) (-1) THEN RevHypSubst' (-1) 0) }

1
1. n : ℕ
2. i : ℕ
3. x : ℕn
4. (i rem n) = 0 ∈ ℤ
5. ((x rem n) + 0 rem n) = (x + i rem n) ∈ ℤ
⊢ ((x rem n) + 0 rem n) = x ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
3.  x  :  \mBbbN{}n
4.  (i  rem  n)  =  0
\mvdash{}  (x  +  i  rem  n)  =  x


By

---

Latex:
((InstLemma  `rem\_addition`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  HypSubst'  (-2)  (-1)
  THEN  RevHypSubst'  (-1)  0)

---

Home Index