---

Step * 1 1 2 1 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] * Π(*,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|
BY
{ Auto }

---

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]  *  (E[b  -  1]  *  \mPi{}(*,e)  (b  -  1)  +  1  \mleq{}  j  <  c.  E[j]))
=  (\mPi{}(*,e)  a  \mleq{}  j  <  b  -  1.  E[j]  *  (E[b  -  1]  *  \mPi{}(*,e)  b  \mleq{}  j  <  c.  E[j]))


By

---

Latex:
Auto

---

Home Index