---

Step * 1 1 1 of Lemma mon_itop_txpose_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ ((Π 0 ≤ j < x. E[swap{n}(x;0) j]) * (E[swap{n}(x;0) x] * (Π x + 1 ≤ j < n. E[swap{n}(x;0) j])))
= ((Π 0 ≤ j < x. E[j]) * (E[x] * (Π x + 1 ≤ j < n. E[j])))
∈ |g|
BY
{ (RW (NthsC [1; 3] (LemmaC `mon_itop_unroll_lo`)) 0 THENA Auto) }

1
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ ((E[swap{n}(x;0) 0] * (Π 0 + 1 ≤ j < x. E[swap{n}(x;0) j])) 
   * 
   (E[swap{n}(x;0) x] * (Π x + 1 ≤ j < n. E[swap{n}(x;0) j])))
= ((E[0] * (Π 0 + 1 ≤ j < x. E[j])) * (E[x] * (Π x + 1 ≤ j < n. E[j])))
∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
4.  x  :  \mBbbN{}\msupplus{}n
\mvdash{}  ((\mPi{}  0  \mleq{}  j  <  x.  E[swap\{n\}(x;0)  j])  *  (E[swap\{n\}(x;0)  x]  *  (\mPi{}  x  +  1  \mleq{}  j  <  n.  E[swap\{n\}(x;0)  j])))
=  ((\mPi{}  0  \mleq{}  j  <  x.  E[j])  *  (E[x]  *  (\mPi{}  x  +  1  \mleq{}  j  <  n.  E[j])))


By

---

Latex:
(RW  (NthsC  [1;  3]  (LemmaC  `mon\_itop\_unroll\_lo`))  0  THENA  Auto)

---

Home Index