; @origtpdbfilename ./TRS/AG01/#3.10.trs
; @xtcfilename "./TRS_Standard/AG01/#3.10.xml"
(format TRS)
(fun eq 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun le 2)
(fun app 2)
(fun nil 0)
(fun add 2)
(fun min 1)
(fun if_min 2)
(fun rm 2)
(fun if_rm 3)
(fun minsort 2)
(fun if_minsort 3)
(rule (eq |0| |0|) true)
(rule (eq |0| (s x)) false)
(rule (eq (s x) |0|) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (le |0| y) true)
(rule (le (s x) |0|) false)
(rule (le (s x) (s y)) (le x y))
(rule (app nil y) y)
(rule (app (add n x) y) (add n (app x y)))
(rule (min (add n nil)) n)
(rule (min (add n (add m x))) (if_min (le n m) (add n (add m x))))
(rule (if_min true (add n (add m x))) (min (add n x)))
(rule (if_min false (add n (add m x))) (min (add m x)))
(rule (rm n nil) nil)
(rule (rm n (add m x)) (if_rm (eq n m) n (add m x)))
(rule (if_rm true n (add m x)) (rm n x))
(rule (if_rm false n (add m x)) (add m (rm n x)))
(rule (minsort nil nil) nil)
(rule (minsort (add n x) y) (if_minsort (eq n (min (add n x))) (add n x) y))
(rule (if_minsort true (add n x) y) (add n (minsort (app (rm n x) y) nil)))
(rule (if_minsort false (add n x) y) (minsort x (add n y)))