---

Step * 1 1 1 of Lemma itop_shift


1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. E : {a..b-} ⟶ |g|
6. k : ℤ
7. E1 : {a..a-} ⟶ |g|
⊢ Π(*,e) a ≤ j < a. E1[j] = Π(*,e) a + k ≤ j < a + k. E1[j - k] ∈ |g|
BY
{ RWH (LemmaC `itop_unroll_base`) 0 THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  a  \mleq{}  b
5.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  |g|
6.  k  :  \mBbbZ{}
7.  E1  :  \{a..a\msupminus{}\}  {}\mrightarrow{}  |g|
\mvdash{}  \mPi{}(*,e)  a  \mleq{}  j  <  a.  E1[j]  =  \mPi{}(*,e)  a  +  k  \mleq{}  j  <  a  +  k.  E1[j  -  k]


By

---

Latex:
RWH  (LemmaC  `itop\_unroll\_base`)  0  THEN  Auto

---

Home Index