Step
*
1
1
2
1
of Lemma
itop_shift
1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. E : {a..b-} ⟶ |g|
6. k : ℤ
7. b1 : {a + 1...}
8. ∀E:{a..b1 - 1-} ⟶ |g|. (Π(*,e) a ≤ j < b1 - 1. E[j] = Π(*,e) a + k ≤ j < (b1 - 1) + k. E[j - k] ∈ |g|)
9. E1 : {a..b1-} ⟶ |g|
⊢ (Π(*,e) a ≤ j < b1 - 1. E1[j] * E1[b1 - 1])
= (Π(*,e) a + k ≤ j < (b1 + k) - 1. E1[j - k] * E1[(b1 + k) - 1 - k])
∈ |g|
BY
{ RW (HigherC (HypC (-2))) 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.  b1  :  \{a  +  1...\}
8.  \mforall{}E:\{a..b1  -  1\msupminus{}\}  {}\mrightarrow{}  |g|.  (\mPi{}(*,e)  a  \mleq{}  j  <  b1  -  1.  E[j]  =  \mPi{}(*,e)  a  +  k  \mleq{}  j  <  (b1  -  1)  +  k.  E[j  -  k])
9.  E1  :  \{a..b1\msupminus{}\}  {}\mrightarrow{}  |g|
\mvdash{}  (\mPi{}(*,e)  a  \mleq{}  j  <  b1  -  1.  E1[j]  *  E1[b1  -  1])
=  (\mPi{}(*,e)  a  +  k  \mleq{}  j  <  (b1  +  k)  -  1.  E1[j  -  k]  *  E1[(b1  +  k)  -  1  -  k])
By
Latex:
RW  (HigherC  (HypC  (-2)))  0  THEN  Auto'
Home
Index