---

Step * 1 2 of Lemma mon_itop_perm_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. p : Sym(n)
5. (Π 0 ≤ j < n. E (p.f j)) = (Π 0 ≤ j < n. E j) ∈ |g|
6. i : ℕ+n
⊢ (Π 0 ≤ j < n. E (p O txpose_perm(i;0).f j)) = (Π 0 ≤ j < n. E j) ∈ |g|
BY
{ (((% For technical reasons, this fails here:
      RWH (RevLemmaWithC [`x',i] `mon_itop_txpose_invar`) 0
     
     So intead:%
     InstLemma `mon_itop_txpose_invar` [g; n; λ2j.E (p.f j); i]
    THENM OnClauses [0; 7] AbReduce
    )
    THEN Auto
    )
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
4.  p  :  Sym(n)
5.  (\mPi{}  0  \mleq{}  j  <  n.  E  (p.f  j))  =  (\mPi{}  0  \mleq{}  j  <  n.  E  j)
6.  i  :  \mBbbN{}\msupplus{}n
\mvdash{}  (\mPi{}  0  \mleq{}  j  <  n.  E  (p  O  txpose\_perm(i;0).f  j))  =  (\mPi{}  0  \mleq{}  j  <  n.  E  j)


By

---

Latex:
(((\%  For  technical  reasons,  this  fails  here:
        RWH  (RevLemmaWithC  [`x',i]  `mon\_itop\_txpose\_invar`)  0
     
      So  intead:\%
      InstLemma  `mon\_itop\_txpose\_invar`  [g;  n;  \mlambda{}\msubtwo{}j.E  (p.f  j);  i]
    THENM  OnClauses  [0;  7]  AbReduce
    )
    THEN  Auto
    )
  THEN  Auto
  )

---

Home Index