; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann14.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann14.xml"
(format TRS)
(fun empty 1)
(fun nil 0)
(fun true 0)
(fun cons 2)
(fun false 0)
(fun tail 1)
(fun head 1)
(fun zero 1)
(fun |0| 0)
(fun s 1)
(fun p 1)
(fun intlist 1)
(fun if_intlist 2)
(fun int 2)
(fun if_int 4)
(fun if1 3)
(fun if2 3)
(rule (empty nil) true)
(rule (empty (cons x y)) false)
(rule (tail nil) nil)
(rule (tail (cons x y)) y)
(rule (head (cons x y)) x)
(rule (zero |0|) true)
(rule (zero (s x)) false)
(rule (p |0|) |0|)
(rule (p (s |0|)) |0|)
(rule (p (s (s x))) (s (p (s x))))
(rule (intlist x) (if_intlist (empty x) x))
(rule (if_intlist true x) nil)
(rule (if_intlist false x) (cons (s (head x)) (intlist (tail x))))
(rule (int x y) (if_int (zero x) (zero y) x y))
(rule (if_int true b x y) (if1 b x y))
(rule (if_int false b x y) (if2 b x y))
(rule (if1 true x y) (cons |0| nil))
(rule (if1 false x y) (cons |0| (int (s |0|) y)))
(rule (if2 true x y) nil)
(rule (if2 false x y) (intlist (int (p x) (p y))))