; @origtpdbfilename ./TRS/secret07/cime/secret2.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/secret2.xml"
(format TRS)
(fun a 4)
(fun h 0)
(fun s 1)
(fun + 2)
(fun |1| 0)
(fun * 2)
(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 (* h x) h)
(rule (* x h) h)
(rule (* (s x) (s y)) (s (+ (+ (* x y) x) y)))