; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann30.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann30.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 minIter 3)
(fun if_min 4)
(fun head 1)
(fun tail 1)
(fun null 1)
(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 nil) |0|)
(rule (min (add n x)) (minIter (add n x) (add n x) |0|))
(rule (minIter nil (add n y) m) (minIter (add n y) (add n y) (s m)))
(rule (minIter (add n x) y m) (if_min (le n m) x y m))
(rule (if_min true x y m) m)
(rule (if_min false x y m) (minIter x y m))
(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 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)))