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

The program

(VAR y x u z)
(RULES
  app(app(minus, 0), y) -> 0
  app(app(minus, app(s, x)), 0) -> app(s, x)
  app(app(minus, app(s, x)), app(s, y)) -> app(app(minus, x), y)
  app(app(le, 0), y) -> true
  app(app(le, app(s, x)), 0) -> false
  app(app(le, app(s, x)), app(s, y)) -> app(app(le, x), y)
  app(app(app(if, true), x), y) -> x
  app(app(app(if, false), x), y) -> y
  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