; @origtpdbfilename ./TRS/higher-order/ToyamaRTA04/Ex7Sorting.trs
; @xtcfilename "./TRS_Standard/Applicative_05/Ex7Sorting.xml"
(format TRS)
(fun app 2)
(fun |sort| 0)
(fun nil 0)
(fun cons 0)
(fun insert 0)
(fun max 0)
(fun |0| 0)
(fun s 0)
(fun min 0)
(fun asort 0)
(fun dsort 0)
(rule (app (app (app |sort| f) g) nil) nil)
(rule (app (app (app |sort| f) g) (app (app cons x) y)) (app (app (app (app insert f) g) (app (app (app |sort| f) g) y)) x))
(rule (app (app (app (app insert f) g) nil) y) (app (app cons y) nil))
(rule (app (app (app (app insert f) g) (app (app cons x) z)) y) (app (app cons (app (app f x) y)) (app (app (app (app insert f) g) z) (app (app g x) y))))
(rule (app (app max |0|) y) y)
(rule (app (app max x) |0|) x)
(rule (app (app max (app s x)) (app s y)) (app (app max x) y))
(rule (app (app min |0|) y) |0|)
(rule (app (app min x) |0|) |0|)
(rule (app (app min (app s x)) (app s y)) (app (app min x) y))
(rule (app asort z) (app (app (app |sort| min) max) z))
(rule (app dsort z) (app (app (app |sort| max) min) z))