Theaimofthisworkistoinvestigatemechanicalsupportforprocess algebra,bothforconcreteapplicationsandtheoreticalproperties.Twoapproaches arepresentedusingtheverificationsystemPVS.Oneapproachdeclaresprocess termsasanuninterpretedtypeandspecifiesequalityontermsbyax