---

Step * of Lemma nim-grp_wf

nim-grp() ∈ AbDGrp
BY
{ (((MemTypeCD THENW Auto)
    THENL [((MemTypeCD THENW Auto)
            THENL [((MemTypeCD THENW Auto) THENL [(MemTypeCD THENW Auto); (RepUR ``nim-grp inverse`` 0 THEN Auto)])
                  ; (RepUR ``nim-grp comm`` 0 THEN Auto)]
          )
          ; (RepUR ``nim-grp eqfun_p`` 0 THEN Auto)]
   )
   THEN RepUR ``nim-grp grp_sig monoid_p assoc ident`` 0
   THEN Auto) }

---

Latex:

---

Latex:
nim-grp()  \mmember{}  AbDGrp


By

---

Latex:
(((MemTypeCD  THENW  Auto)
    THENL  [((MemTypeCD  THENW  Auto)
                    THENL  [((MemTypeCD  THENW  Auto)
                                    THENL  [(MemTypeCD  THENW  Auto);  (RepUR  ``nim-grp  inverse``  0  THEN  Auto)]
                                )
                                ;  (RepUR  ``nim-grp  comm``  0  THEN  Auto)]
                )
                ;  (RepUR  ``nim-grp  eqfun\_p``  0  THEN  Auto)]
  )
  THEN  RepUR  ``nim-grp  grp\_sig  monoid\_p  assoc  ident``  0
  THEN  Auto)

---

Home Index