; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann35.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann35.xml"
(format TRS)
(fun a 2)
(fun append 0)
(fun nil 0)
(fun cons 0)
(fun filter 0)
(fun if 0)
(fun le 0)
(fun |0| 0)
(fun true 0)
(fun s 0)
(fun false 0)
(fun not 0)
(fun not2 0)
(fun qs 0)
(rule (a (a append nil) ys) ys)
(rule (a (a append (a (a cons x) xs)) ys) (a (a cons x) (a (a append xs) ys)))
(rule (a (a filter f) nil) nil)
(rule (a (a filter f) (a (a cons x) xs)) (a (a (a if (a f x)) x) (a (a filter f) xs)))
(rule (a (a le |0|) y) true)
(rule (a (a le (a s x)) |0|) false)
(rule (a (a le (a s x)) (a s y)) (a (a le x) y))
(rule (a (a (a if true) x) xs) (a (a cons x) xs))
(rule (a (a (a if false) x) xs) xs)
(rule (a (a not f) b) (a not2 (a f b)))
(rule (a not2 true) false)
(rule (a not2 false) true)
(rule (a qs nil) nil)
(rule (a qs (a (a cons x) xs)) (a (a append (a qs (a (a filter (a le x)) xs))) (a (a cons x) (a qs (a (a filter (a not (a le x))) xs)))))