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

The program

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend