(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
mark(p(X)) → active(p(mark(X)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(leq(X1, X2)) → active(leq(mark(X1), mark(X2)))
mark(true) → active(true)
mark(false) → active(false)
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
mark(diff(X1, X2)) → active(diff(mark(X1), mark(X2)))
p(mark(X)) → p(X)
p(active(X)) → p(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
leq(mark(X1), X2) → leq(X1, X2)
leq(X1, mark(X2)) → leq(X1, X2)
leq(active(X1), X2) → leq(X1, X2)
leq(X1, active(X2)) → leq(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
diff(mark(X1), X2) → diff(X1, X2)
diff(X1, mark(X2)) → diff(X1, X2)
diff(active(X1), X2) → diff(X1, X2)
diff(X1, active(X2)) → diff(X1, X2)
Q is empty.