; @origtpdbfilename ./TRS/currying/Ste92/minsort.trs
; @xtcfilename "./TRS_Standard/Applicative_first_order_05/minsort.xml"
(format TRS)
(fun app 2)
(fun le 0)
(fun |0| 0)
(fun true 0)
(fun s 0)
(fun false 0)
(fun eq 0)
(fun if 0)
(fun minsort 0)
(fun nil 0)
(fun cons 0)
(fun min 0)
(fun del 0)
(fun map 0)
(fun filter 0)
(fun filter2 0)
(rule (app (app le |0|) y) true)
(rule (app (app le (app s x)) |0|) false)
(rule (app (app le (app s x)) (app s y)) (app (app le x) y))
(rule (app (app eq |0|) |0|) true)
(rule (app (app eq |0|) (app s y)) false)
(rule (app (app eq (app s x)) |0|) false)
(rule (app (app eq (app s x)) (app s y)) (app (app eq x) y))
(rule (app (app (app if true) x) y) x)
(rule (app (app (app if false) x) y) y)
(rule (app minsort nil) nil)
(rule (app minsort (app (app cons x) y)) (app (app cons (app (app min x) y)) (app minsort (app (app del (app (app min x) y)) (app (app cons x) y)))))
(rule (app (app min x) nil) x)
(rule (app (app min x) (app (app cons y) z)) (app (app (app if (app (app le x) y)) (app (app min x) z)) (app (app min y) z)))
(rule (app (app del x) nil) nil)
(rule (app (app del x) (app (app cons y) z)) (app (app (app if (app (app eq x) y)) z) (app (app cons y) (app (app del x) z))))
(rule (app (app map f) nil) nil)
(rule (app (app map f) (app (app cons x) xs)) (app (app cons (app f x)) (app (app map f) xs)))
(rule (app (app filter f) nil) nil)
(rule (app (app filter f) (app (app cons x) xs)) (app (app (app (app filter2 (app f x)) f) x) xs))
(rule (app (app (app (app filter2 true) f) x) xs) (app (app cons x) (app (app filter f) xs)))
(rule (app (app (app (app filter2 false) f) x) xs) (app (app filter f) xs))