; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann02.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann02.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 head 1)
(fun tail 1)
(fun null 1)
(fun rm 2)
(fun if_rm 3)
(fun minsort 1)
(fun mins 3)
(fun if 4)
(fun if2 4)
(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 (head (add n x)) n)
(rule (tail (add n x)) x)
(rule (tail nil) nil)
(rule (null nil) true)
(rule (null (add n x)) false)
(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 x) (mins x nil nil))
(rule (mins x y z) (if (null x) x y z))
(rule (if true x y z) z)
(rule (if false x y z) (if2 (eq (head x) (min x)) x y z))
(rule (if2 true x y z) (mins (app (rm (head x) (tail x)) y) nil (app z (add (head x) nil))))
(rule (if2 false x y z) (mins (tail x) (add (head x) y) z))