; @origtpdbfilename ./TRS/currying/AG01/#3.6.trs
; @xtcfilename "./TRS_Standard/Applicative_first_order_05/#3.6.xml"
(format TRS)
(fun app 2)
(fun le 0)
(fun |0| 0)
(fun true 0)
(fun s 0)
(fun false 0)
(fun pred 0)
(fun minus 0)
(fun gcd 0)
(fun if_gcd 0)
(fun map 0)
(fun nil 0)
(fun cons 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 pred (app s x)) x)
(rule (app (app minus x) |0|) x)
(rule (app (app minus x) (app s y)) (app pred (app (app minus x) y)))
(rule (app (app gcd |0|) y) y)
(rule (app (app gcd (app s x)) |0|) (app s x))
(rule (app (app gcd (app s x)) (app s y)) (app (app (app if_gcd (app (app le y) x)) (app s x)) (app s y)))
(rule (app (app (app if_gcd true) (app s x)) (app s y)) (app (app gcd (app (app minus x) y)) (app s y)))
(rule (app (app (app if_gcd false) (app s x)) (app s y)) (app (app gcd (app (app minus y) x)) (app s x)))
(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))