; @origtpdbfilename ./TRS/currying/AG01/#3.10.trs
; @xtcfilename "./TRS_Standard/Applicative_first_order_05/#3.10.xml"
(format TRS)
(fun |app'| 2)
(fun eq 0)
(fun |0| 0)
(fun true 0)
(fun s 0)
(fun false 0)
(fun le 0)
(fun app 0)
(fun nil 0)
(fun add 0)
(fun min 0)
(fun if_min 0)
(fun rm 0)
(fun if_rm 0)
(fun minsort 0)
(fun if_minsort 0)
(fun map 0)
(fun filter 0)
(fun filter2 0)
(rule (|app'| (|app'| eq |0|) |0|) true)
(rule (|app'| (|app'| eq |0|) (|app'| s x)) false)
(rule (|app'| (|app'| eq (|app'| s x)) |0|) false)
(rule (|app'| (|app'| eq (|app'| s x)) (|app'| s y)) (|app'| (|app'| eq x) 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'| min (|app'| (|app'| add n) nil)) n)
(rule (|app'| min (|app'| (|app'| add n) (|app'| (|app'| add m) x))) (|app'| (|app'| if_min (|app'| (|app'| le n) m)) (|app'| (|app'| add n) (|app'| (|app'| add m) x))))
(rule (|app'| (|app'| if_min true) (|app'| (|app'| add n) (|app'| (|app'| add m) x))) (|app'| min (|app'| (|app'| add n) x)))
(rule (|app'| (|app'| if_min false) (|app'| (|app'| add n) (|app'| (|app'| add m) x))) (|app'| min (|app'| (|app'| add m) x)))
(rule (|app'| (|app'| rm n) nil) nil)
(rule (|app'| (|app'| rm n) (|app'| (|app'| add m) x)) (|app'| (|app'| (|app'| if_rm (|app'| (|app'| eq n) m)) n) (|app'| (|app'| add m) x)))
(rule (|app'| (|app'| (|app'| if_rm true) n) (|app'| (|app'| add m) x)) (|app'| (|app'| rm n) x))
(rule (|app'| (|app'| (|app'| if_rm false) n) (|app'| (|app'| add m) x)) (|app'| (|app'| add m) (|app'| (|app'| rm n) x)))
(rule (|app'| (|app'| minsort nil) nil) nil)
(rule (|app'| (|app'| minsort (|app'| (|app'| add n) x)) y) (|app'| (|app'| (|app'| if_minsort (|app'| (|app'| eq n) (|app'| min (|app'| (|app'| add n) x)))) (|app'| (|app'| add n) x)) y))
(rule (|app'| (|app'| (|app'| if_minsort true) (|app'| (|app'| add n) x)) y) (|app'| (|app'| add n) (|app'| (|app'| minsort (|app'| (|app'| app (|app'| (|app'| rm n) x)) y)) nil)))
(rule (|app'| (|app'| (|app'| if_minsort false) (|app'| (|app'| add n) x)) y) (|app'| (|app'| minsort x) (|app'| (|app'| add n) y)))
(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))