; @xtcfilename "./TRS_Standard/Hydras/lepper_0.xml"
(format TRS)
(fun a 1)
(fun o 1)
(fun l 1)
(fun S 1)
(fun + 2)
(fun P 1)
(fun M 1)
(fun |0| 0)
(rule (a x1) x1)
(rule (o x1) x1)
(rule (l x1) x1)
(rule (S x1) x1)
(rule (+ x1 x2) x2)
(rule (+ x1 x2) x1)
(rule (P x1) x1)
(rule (M x1) x1)
(rule (P |0|) (S |0|))
(rule (+ x (S y)) (S (+ x y)))
(rule (a (l x)) (l (a (a x))))
(rule (l (o x)) (o (l (l x))))
(rule (o x) (l x))
(rule (l x) (a x))
(rule (a (S x)) (S (l x)))
(rule (a (+ x y)) (+ (l x) y))
(rule (a (+ x y)) (+ x (l y)))
(rule (a (P x1)) (P (l x1)))
(rule (+ x (o y)) (o (+ x y)))
(rule (P (o x1)) (o (P x1)))
(rule (M (l y)) (+ (M y) (P y)))
(rule (a (S x)) (o x))
(rule (P (S y)) (o (M y)))
(rule (P (P y)) (o (M y)))