---

Step * 1 1 of Lemma mon_reduce_eq_itop


1. g : IMonoid
⊢ (Π []) = (Π 0 ≤ i < ||[]||. [][i]) ∈ |g|
BY
{ ((AbReduce 0 THEN RewriteWith [] ``mon_itop_unroll_base`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IMonoid
\mvdash{}  (\mPi{}  [])  =  (\mPi{}  0  \mleq{}  i  <  ||[]||.  [][i])


By

---

Latex:
((AbReduce  0  THEN  RewriteWith  []  ``mon\_itop\_unroll\_base``  0)  THEN  Auto)

---

Home Index