---

Step * of Lemma permr_massoc_functionality

∀g:IAbMonoid. ∀as,as',bs,bs':|g| List.  (as ≡ bs upto ~ ⇒ as' ≡ bs' upto ~ ⇒ (as ≡ as' upto ~ ⇐⇒ bs ≡ bs' upto ~))
BY
{ ((UnivCD) THENA Auto) }

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 ~@i
7. as' ≡ bs' upto ~@i
⊢ as ≡ as' upto ~ ⇐⇒ bs ≡ bs' upto ~

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}as,as',bs,bs':|g|  List.
    (as  \mequiv{}  bs  upto  \msim{}  {}\mRightarrow{}  as'  \mequiv{}  bs'  upto  \msim{}  {}\mRightarrow{}  (as  \mequiv{}  as'  upto  \msim{}  \mLeftarrow{}{}\mRightarrow{}  bs  \mequiv{}  bs'  upto  \msim{}))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index