---

Step * 1 of Lemma mon_reduce_eq_itop


1. g : IMonoid
2. as : |g| List
⊢ (Π as) = (Π 0 ≤ i < ||as||. as[i]) ∈ |g|
BY
{ ListInd 2 }

1
1. g : IMonoid
⊢ (Π []) = (Π 0 ≤ i < ||[]||. [][i]) ∈ |g|

2
1. g : IMonoid
2. u : |g|
3. v : |g| List
4. (Π v) = (Π 0 ≤ i < ||v||. v[i]) ∈ |g|
⊢ (Π [u / v]) = (Π 0 ≤ i < ||[u / v]||. [u / v][i]) ∈ |g|

---

Latex:

---

Latex:

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


By

---

Latex:
ListInd  2

---

Home Index