---

Step * 1 of Lemma permr_massoc_functionality


1. g : IAbMonoid@i'
2. as : |g| List@i
3. as' : |g| List@i
4. bs : |g| List@i
5. bs' : |g| List@i
6. as ≡ bs upto ~@i
7. as' ≡ bs' upto ~@i
⊢ as ≡ as' upto ~ ⇐⇒ bs ≡ bs' upto ~
BY
{ TryOnAll (Unfold `permr_massoc`) }

1
1. g : IAbMonoid@i'
2. as : |g| List@i
3. as' : |g| List@i
4. bs : |g| List@i
5. bs' : |g| List@i
6. as ≡ bs upto x,y.x ~ y @i
7. as' ≡ bs' upto x,y.x ~ y @i
⊢ as ≡ as' upto x,y.x ~ y  ⇐⇒ bs ≡ bs' upto x,y.x ~ y 

---

Latex:

---

Latex:

1.  g  :  IAbMonoid@i'
2.  as  :  |g|  List@i
3.  as'  :  |g|  List@i
4.  bs  :  |g|  List@i
5.  bs'  :  |g|  List@i
6.  as  \mequiv{}  bs  upto  \msim{}@i
7.  as'  \mequiv{}  bs'  upto  \msim{}@i
\mvdash{}  as  \mequiv{}  as'  upto  \msim{}  \mLeftarrow{}{}\mRightarrow{}  bs  \mequiv{}  bs'  upto  \msim{}


By

---

Latex:
TryOnAll  (Unfold  `permr\_massoc`)

---

Home Index