(<=> (Abelian-Semigroup ?Domain ?Op ?Id) (And (Semigroup ?Domain ?Op ?Id) (Commutative ?Op ?Domain)))
(<=> (Abelian-Semigroup ?Domain ?Op ?Id) (And (Semigroup ?Domain ?Op ?Id) (Commutative ?Op ?Domain))) (<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id) (And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id) (Abelian-Semigroup ?Domain ?Mult-Op ?One-Id) (Distributes ?Mult-Op ?Plus-Op ?Domain)))