; @xtcfilename "./TRS_Standard/Hydras/lepper_1.xml"
(format TRS)
(fun a 1)
(fun o 1)
(fun l 1)
(fun S 1)
(fun + 2)
(fun P 2)
(fun M 2)
(fun J1 2)
(fun Q11 2)
(fun R1 3)
(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 x2) x2)
(rule (P x1 x2) x1)
(rule (M x1 x2) x2)
(rule (M x1 x2) x1)
(rule (J1 x1 x2) x2)
(rule (J1 x1 x2) x1)
(rule (Q11 x1 x2) x2)
(rule (Q11 x1 x2) x1)
(rule (R1 x1 x2 x3) x3)
(rule (R1 x1 x2 x3) x2)
(rule (R1 x1 x2 x3) x1)
(rule (P |0| |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 x2)) (P x1 (l x2)))
(rule (a (P x1 x2)) (P (l x1) x2))
(rule (+ x (o y)) (o (+ x y)))
(rule (P x1 (o x2)) (o (P x1 x2)))
(rule (P (o x1) x2) (o (P x1 x2)))
(rule (M x1 (l y)) (+ (M x1 y) (P x1 y)))
(rule (J1 (l x1) y) (P (J1 x1 y) |0|))
(rule (a (S x)) (o x))
(rule (P |0| (S y)) (o (M |0| y)))
(rule (P |0| (P x1 y)) (o (M x1 y)))
(rule (P (S x1) y) (o (J1 x1 y)))
(rule (P (S x1) (S y)) (o (J1 x1 (P (S x1) y))))
(rule (a (P x1 |0|)) (Q11 (a x1) x1))
(rule (Q11 (o x1) y) (o (P x1 y)))
(rule (a (P x1 (S y))) (R1 (a x1) x1 y))
(rule (R1 (o x1) y z) (o (P x1 (P y z))))