import peano.trs

Mx0       → x
M(Sx)(Sy) → Mxy
Q0(Sy)    → 0
Q(Sx)(Sy) → S(Q(Mxy)(Sy))