/home/nowonder/forschung/aprove/TPDB05/TRS/Ste92/perfect.trs

The program

(from Ste92 example 10)
(VAR u x y z)
(RULES
perfectp(0) -> false
perfectp(s(x)) -> f(x,s(0),s(x),s(x))
f(0,y,0,u) -> true
f(0,y,s(z),u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x,y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend