0 QTRS
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))