---

Step * 1 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 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 
BY
{ Sel (-1) (BLemma `permr_upto_functionality_wrt_permr_upto`) 
THEN Auto }

---

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  x,y.x  \msim{}  y  @i
7.  as'  \mequiv{}  bs'  upto  x,y.x  \msim{}  y  @i
\mvdash{}  as  \mequiv{}  as'  upto  x,y.x  \msim{}  y    \mLeftarrow{}{}\mRightarrow{}  bs  \mequiv{}  bs'  upto  x,y.x  \msim{}  y 


By

---

Latex:
Sel  (-1)  (BLemma  `permr\_upto\_functionality\_wrt\_permr\_upto`) 
THEN  Auto

---

Home Index