; @origtpdbfilename ./TRS/currying/AG01/#3.55.trs
; @xtcfilename "./TRS_Standard/Applicative_first_order_05/#3.55.xml"
(format TRS)
(fun |app'| 2)
(fun minus 0)
(fun |0| 0)
(fun s 0)
(fun quot 0)
(fun le 0)
(fun true 0)
(fun false 0)
(fun app 0)
(fun nil 0)
(fun add 0)
(fun low 0)
(fun if_low 0)
(fun high 0)
(fun if_high 0)
(fun quicksort 0)
(fun map 0)
(fun filter 0)
(fun filter2 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'| 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'| 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'| app nil) y) y)
(rule (|app'| (|app'| app (|app'| (|app'| add n) x)) y) (|app'| (|app'| add n) (|app'| (|app'| app x) y)))
(rule (|app'| (|app'| low n) nil) nil)
(rule (|app'| (|app'| low n) (|app'| (|app'| add m) x)) (|app'| (|app'| (|app'| if_low (|app'| (|app'| le m) n)) n) (|app'| (|app'| add m) x)))
(rule (|app'| (|app'| (|app'| if_low true) n) (|app'| (|app'| add m) x)) (|app'| (|app'| add m) (|app'| (|app'| low n) x)))
(rule (|app'| (|app'| (|app'| if_low false) n) (|app'| (|app'| add m) x)) (|app'| (|app'| low n) x))
(rule (|app'| (|app'| high n) nil) nil)
(rule (|app'| (|app'| high n) (|app'| (|app'| add m) x)) (|app'| (|app'| (|app'| if_high (|app'| (|app'| le m) n)) n) (|app'| (|app'| add m) x)))
(rule (|app'| (|app'| (|app'| if_high true) n) (|app'| (|app'| add m) x)) (|app'| (|app'| high n) x))
(rule (|app'| (|app'| (|app'| if_high false) n) (|app'| (|app'| add m) x)) (|app'| (|app'| add m) (|app'| (|app'| high n) x)))
(rule (|app'| quicksort nil) nil)
(rule (|app'| quicksort (|app'| (|app'| add n) x)) (|app'| (|app'| app (|app'| quicksort (|app'| (|app'| low n) x))) (|app'| (|app'| add n) (|app'| quicksort (|app'| (|app'| high n) x)))))
(rule (|app'| (|app'| map f) nil) nil)
(rule (|app'| (|app'| map f) (|app'| (|app'| add x) xs)) (|app'| (|app'| add (|app'| f x)) (|app'| (|app'| map f) xs)))
(rule (|app'| (|app'| filter f) nil) nil)
(rule (|app'| (|app'| filter f) (|app'| (|app'| add 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'| add x) (|app'| (|app'| filter f) xs)))
(rule (|app'| (|app'| (|app'| (|app'| filter2 false) f) x) xs) (|app'| (|app'| filter f) xs))