; @origtpdbfilename ./TRS/currying/AG01/#3.57.trs
; @xtcfilename "./TRS_Standard/Applicative_first_order_05/#3.57.xml"
(format TRS)
(fun |app'| 2)
(fun minus 0)
(fun |0| 0)
(fun s 0)
(fun plus 0)
(fun quot 0)
(fun app 0)
(fun nil 0)
(fun cons 0)
(fun sum 0)
(fun map 0)
(fun filter 0)
(fun filter2 0)
(fun true 0)
(fun false 0)
(rule (|app'| (|app'| minus x) |0|) x)
(rule (|app'| (|app'| minus (|app'| s x)) (|app'| s y)) (|app'| (|app'| minus x) y))
(rule (|app'| (|app'| minus (|app'| (|app'| minus x) y)) z) (|app'| (|app'| minus x) (|app'| (|app'| plus y) z)))
(rule (|app'| (|app'| quot |0|) (|app'| s y)) |0|)
(rule (|app'| (|app'| quot (|app'| s x)) (|app'| s y)) (|app'| s (|app'| (|app'| quot (|app'| (|app'| minus x) y)) (|app'| s y))))
(rule (|app'| (|app'| plus |0|) y) y)
(rule (|app'| (|app'| plus (|app'| s x)) y) (|app'| s (|app'| (|app'| plus x) y)))
(rule (|app'| (|app'| app nil) k) k)
(rule (|app'| (|app'| app l) nil) l)
(rule (|app'| (|app'| app (|app'| (|app'| cons x) l)) k) (|app'| (|app'| cons x) (|app'| (|app'| app l) k)))
(rule (|app'| sum (|app'| (|app'| cons x) nil)) (|app'| (|app'| cons x) nil))
(rule (|app'| sum (|app'| (|app'| cons x) (|app'| (|app'| cons y) l))) (|app'| sum (|app'| (|app'| cons (|app'| (|app'| plus x) y)) l)))
(rule (|app'| sum (|app'| (|app'| app l) (|app'| (|app'| cons x) (|app'| (|app'| cons y) k)))) (|app'| sum (|app'| (|app'| app l) (|app'| sum (|app'| (|app'| cons x) (|app'| (|app'| cons y) k))))))
(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))