/home/nowonder/forschung/aprove/TPDB05/TRS/higher-order/Lifantsev/Ex5Sorting.trs

The program

(VAR x y f g h t l)
(RULES
  app(app(max, 0), x) -> x
  app(app(max, x), 0) -> x
  app(app(max, app(s, x)), app(s, y)) -> app(app(max, x), y)
  app(app(min, 0), x) -> 0
  app(app(min, x), 0) -> 0
  app(app(min, app(s, x)), app(s, y)) -> app(app(min, x), y)
  app(app(app(app(insert, f), g), nil), x) -> app(app(cons, x), nil)
  app(app(app(app(insert, f), g), app(app(cons, h), t)), x) -> app(app(cons, app(app(f, x), h)), app(app(app(app(insert, f), g), t), app(app(g, x), h)))
  app(app(app(sort, f), g), nil) -> nil
  app(app(app(sort, f), g), app(app(cons, h), t)) -> app(app(app(app(insert, f), g), app(app(app(sort, f), g), t)), h)
  app(ascending_sort, l) -> app(app(app(sort, min), max), l)
  app(descending_sort, l) -> app(app(app(sort, max), min), l)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend