; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann17.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann17.xml"
(format TRS)
(fun sum 2)
(fun cons 2)
(fun s 1)
(fun |0| 0)
(fun nil 0)
(fun empty 1)
(fun true 0)
(fun false 0)
(fun tail 1)
(fun head 1)
(fun weight 1)
(fun if 3)
(fun weight_undefined_error 0)
(fun if2 2)
(rule (sum (cons (s n) x) (cons m y)) (sum (cons n x) (cons (s m) y)))
(rule (sum (cons |0| x) y) (sum x y))
(rule (sum nil y) y)
(rule (empty nil) true)
(rule (empty (cons n x)) false)
(rule (tail nil) nil)
(rule (tail (cons n x)) x)
(rule (head (cons n x)) n)
(rule (weight x) (if (empty x) (empty (tail x)) x))
(rule (if true b x) weight_undefined_error)
(rule (if false b x) (if2 b x))
(rule (if2 true x) (head x))
(rule (if2 false x) (weight (sum x (cons |0| (tail (tail x))))))