---

Step * 1 of Lemma mon_itop_split_el


1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. c : ℤ
5. a ≤ b
6. b < c
7. E : {a..c-} ⟶ |g|
⊢ (Π a ≤ j < c. E[j]) = ((Π a ≤ j < b. E[j]) * (E[b] * (Π b + 1 ≤ j < c. E[j]))) ∈ |g|
BY
{ RWN 1 (LemmaWithC [`b',b] `mon_itop_split`) 0 
THENM RWN 2 (LemmaC `mon_itop_unroll_lo`) 0 
THEN Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
RWN  1  (LemmaWithC  [`b',b]  `mon\_itop\_split`)  0 
THENM  RWN  2  (LemmaC  `mon\_itop\_unroll\_lo`)  0 
THEN  Auto

---

Home Index