Alphabet

mult:[N × N] ⟶ N
plus:[N × N] ⟶ N
s:[N] ⟶ N
z:N

Variables

X:N
Y:N
U:N
V:N
W:N
P:N
X1:N
Y1:N
U1:N
V1:N
W1:N
P1:N

Rules

plus(z, X)⇒X
plus(s(Y), U)⇒plus(Y, s(U))
plus(plus(V, W), P)⇒plus(V, plus(W, P))
mult(z, X1)⇒z
mult(s(Y1), U1)⇒plus(mult(Y1, U1), U1)
mult(plus(V1, W1), P1)⇒plus(mult(V1, P1), mult(W1, P1))