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