---

Step * 1 1 2 1 of Lemma itop_split


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

1
1. g : IMonoid
2. a : ℤ
3. c : ℤ
4. b : {a + 1...}
5. b ≤ c
6. E : {a..c-} ⟶ |g|
⊢ (Π(*,e) a ≤ j < b - 1. E[j] * (E[b - 1] * Π(*,e) (b - 1) + 1 ≤ j < c. E[j]))
= (Π(*,e) a ≤ j < b - 1. E[j] * (E[b - 1] * Π(*,e) b ≤ j < c. E[j]))
∈ |g|

---

Latex:

---

Latex:

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


By

---

Latex:
RWN  2  (LemmaC  `itop\_unroll\_lo`)  0 
THENM  RWN  3  (LemmaC  `itop\_unroll\_hi`)  0 
THENM  RW  MonNormC  0  THENA  Auto

---

Home Index