; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann03.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann03.xml"
(format TRS)
(fun null 1)
(fun nil 0)
(fun true 0)
(fun add 2)
(fun false 0)
(fun tail 1)
(fun head 1)
(fun app 2)
(fun reverse 1)
(fun shuffle 1)
(fun shuff 2)
(fun if 4)
(rule (null nil) true)
(rule (null (add n x)) false)
(rule (tail (add n x)) x)
(rule (tail nil) nil)
(rule (head (add n x)) n)
(rule (app nil y) y)
(rule (app (add n x) y) (add n (app x y)))
(rule (reverse nil) nil)
(rule (reverse (add n x)) (app (reverse x) (add n nil)))
(rule (shuffle x) (shuff x nil))
(rule (shuff x y) (if (null x) x y (app y (add (head x) nil))))
(rule (if true x y z) y)
(rule (if false x y z) (shuff (reverse (tail x)) z))