; @origtpdbfilename ./TRS/secret07/cime/secret4.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/secret4.xml"
(format TRS)
(fun a 4)
(fun h 0)
(fun s 1)
(fun + 2)
(fun |1| 0)
(fun app 2)
(fun nil 0)
(fun cons 2)
(fun sum 1)
(rule (a h h h x) (s x))
(rule (a l x (s y) h) (a l x y (s h)))
(rule (a l x (s y) (s z)) (a l x y (a l x (s y) z)))
(rule (a l (s x) h z) (a l x z z))
(rule (a (s l) h h z) (a l z h z))
(rule (+ x h) x)
(rule (+ h x) x)
(rule (+ (s x) (s y)) (s (s (+ x y))))
(rule (+ (+ x y) z) (+ x (+ y z)))
(rule (s h) |1|)
(rule (app nil k) k)
(rule (app l nil) l)
(rule (app (cons x l) k) (cons x (app l k)))
(rule (sum (cons x nil)) (cons x nil))
(rule (sum (cons x (cons y l))) (sum (cons (a x y h h) l)))