Step
*
of Lemma
mon_itop_unroll_base
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = e ∈ |g|) supposing i = j ∈ ℤ
BY
{ ProveSpecializedLemma `itop_unroll_base` 0 [parm{i}] (FoldC `mon_itop`) }
Latex:
Latex:
\mforall{}[g:IMonoid]. \mforall{}[i,j:\mBbbZ{}]. \mforall{}[E:\{i..j\msupminus{}\} {}\mrightarrow{} |g|]. ((\mPi{} i \mleq{} k < j. E[k]) = e) supposing i = j
By
Latex:
ProveSpecializedLemma `itop\_unroll\_base` 0 [parm\{i\}] (FoldC `mon\_itop`)
Home
Index