Step * of Lemma itop_shift

[g:IMonoid]. ∀[a,b:ℤ].
  ∀[E:{a..b-} ⟶ |g|]. ∀[k:ℤ].  (*,e) a ≤ j < b. E[j] = Π(*,e) k ≤ j < k. E[j k] ∈ |g|) supposing a ≤ b
BY
(Auto
   THEN Assert
        ∀b:ℤ. ∀E:{a..b-} ⟶ |g|. (*,e) a ≤ j < b. E[j] = Π(*,e) k ≤ j < k. E[j k] ∈ |g|) supposing a ≤ b⋅
   }

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

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


Latex:


Latex:
\mforall{}[g:IMonoid].  \mforall{}[a,b:\mBbbZ{}].
    \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  |g|].  \mforall{}[k:\mBbbZ{}].    (\mPi{}(*,e)  a  \mleq{}  j  <  b.  E[j]  =  \mPi{}(*,e)  a  +  k  \mleq{}  j  <  b  +  k.  E[j  -  k]) 
    supposing  a  \mleq{}  b


By


Latex:
(Auto
  THEN  Assert
            \mforall{}b:\mBbbZ{}
                \mforall{}E:\{a..b\msupminus{}\}  {}\mrightarrow{}  |g|.  (\mPi{}(*,e)  a  \mleq{}  j  <  b.  E[j]  =  \mPi{}(*,e)  a  +  k  \mleq{}  j  <  b  +  k.  E[j  -  k]) 
                supposing  a  \mleq{}  b\mcdot{}
  )




Home Index