---

Step * 1 1 1 of Lemma itop_split


1. g : IMonoid
2. a : ℤ
3. c : ℤ
4. a ≤ c
5. E : {a..c-} ⟶ |g|
⊢ Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < a. E[j] * Π(*,e) a ≤ j < c. E[j]) ∈ |g|
BY
{ RWN 2 (LemmaC `itop_unroll_base`) 0 
THEN RW MonNormC 0 THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  a  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  a  \mleq{}  c
5.  E  :  \{a..c\msupminus{}\}  {}\mrightarrow{}  |g|
\mvdash{}  \mPi{}(*,e)  a  \mleq{}  j  <  c.  E[j]  =  (\mPi{}(*,e)  a  \mleq{}  j  <  a.  E[j]  *  \mPi{}(*,e)  a  \mleq{}  j  <  c.  E[j])


By

---

Latex:
RWN  2  (LemmaC  `itop\_unroll\_base`)  0 
THEN  RW  MonNormC  0  THEN  Auto

---

Home Index