; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann18.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann18.xml"
(format TRS)
(fun eq 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun le 2)
(fun min 1)
(fun cons 2)
(fun nil 0)
(fun if_min 2)
(fun replace 3)
(fun if_replace 4)
(fun empty 1)
(fun head 1)
(fun tail 1)
(fun |sort| 1)
(fun sortIter 2)
(fun if 4)
(fun append 2)
(rule (eq |0| |0|) true)
(rule (eq |0| (s m)) false)
(rule (eq (s n) |0|) false)
(rule (eq (s n) (s m)) (eq n m))
(rule (le |0| m) true)
(rule (le (s n) |0|) false)
(rule (le (s n) (s m)) (le n m))
(rule (min (cons x nil)) x)
(rule (min (cons n (cons m x))) (if_min (le n m) (cons n (cons m x))))
(rule (if_min true (cons n (cons m x))) (min (cons n x)))
(rule (if_min false (cons n (cons m x))) (min (cons m x)))
(rule (replace n m nil) nil)
(rule (replace n m (cons k x)) (if_replace (eq n k) n m (cons k x)))
(rule (if_replace true n m (cons k x)) (cons m x))
(rule (if_replace false n m (cons k x)) (cons k (replace n m x)))
(rule (empty nil) true)
(rule (empty (cons n x)) false)
(rule (head (cons n x)) n)
(rule (tail nil) nil)
(rule (tail (cons n x)) x)
(rule (|sort| x) (sortIter x nil))
(rule (sortIter x y) (if (empty x) x y (append y (cons (min x) nil))))
(rule (if true x y z) y)
(rule (if false x y z) (sortIter (replace (min x) (head x) (tail x)) z))