; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann07.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann07.xml"
(format TRS)
(fun car 1)
(fun cons 2)
(fun cddr 1)
(fun nil 0)
(fun cadr 1)
(fun isZero 1)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun plus 2)
(fun ifplus 3)
(fun p 1)
(fun times 2)
(fun iftimes 3)
(fun shorter 2)
(fun prod 1)
(fun if 3)
(fun if2 2)
(rule (car (cons x l)) x)
(rule (cddr nil) nil)
(rule (cddr (cons x nil)) nil)
(rule (cddr (cons x (cons y l))) l)
(rule (cadr (cons x (cons y l))) y)
(rule (isZero |0|) true)
(rule (isZero (s x)) false)
(rule (plus x y) (ifplus (isZero x) x y))
(rule (ifplus true x y) y)
(rule (ifplus false x y) (s (plus (p x) y)))
(rule (times x y) (iftimes (isZero x) x y))
(rule (iftimes true x y) |0|)
(rule (iftimes false x y) (plus y (times (p x) y)))
(rule (p (s x)) x)
(rule (p |0|) |0|)
(rule (shorter nil y) true)
(rule (shorter (cons x l) |0|) false)
(rule (shorter (cons x l) (s y)) (shorter l y))
(rule (prod l) (if (shorter l |0|) (shorter l (s |0|)) l))
(rule (if true b l) (s |0|))
(rule (if false b l) (if2 b l))
(rule (if2 true l) (car l))
(rule (if2 false l) (prod (cons (times (car l) (cadr l)) (cddr l))))