ARS(Abstract Reduction System)って全然理解できません。
関数記号　A(２項演算子)M(２項演算子),S(単項演算子),0(定数)を用いて、書き換え規則
１．A(x,0)→x
２．A(x,S(y))→S(A(x,y))
３．M(x,0)→0
４．M(x,S(y))→A(x,M(x,y))
について、ＳＮ性とＣＲ性を持つかの証明ってどうなるんでしょうか？