Syntax definition crmx

Description: Extend class notation to include the Robertson-Matiyasevich X sequence.

	Ref	Expression
Assertion	crmx	$$class{X}_{\mathrm{rm}}$$