; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann39.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann39.xml"
(format TRS)
(fun a 2)
(fun divides 0)
(fun |0| 0)
(fun s 0)
(fun true 0)
(fun div2 0)
(fun false 0)
(fun filter 0)
(fun nil 0)
(fun cons 0)
(fun if 0)
(fun not 0)
(fun not2 0)
(fun sieve 0)
(rule (a (a divides |0|) (a s y)) true)
(rule (a (a divides (a s x)) (a s y)) (a (a (a div2 x) (a s y)) y))
(rule (a (a (a div2 x) y) |0|) (a (a divides x) y))
(rule (a (a (a div2 |0|) y) (a s z)) false)
(rule (a (a (a div2 (a s x)) y) (a s z)) (a (a (a div2 x) y) z))
(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 (a if true) x) xs) (a (a cons x) xs))
(rule (a (a (a if false) x) xs) xs)
(rule (a (a not f) x) (a not2 (a f x)))
(rule (a not2 true) false)
(rule (a not2 false) true)
(rule (a sieve nil) nil)
(rule (a sieve (a (a cons x) xs)) (a (a cons x) (a sieve (a (a filter (a not (a divides x))) xs))))