(format TRS)
(fun f 4)
(fun s 1)
(fun |0| 0)
(rule (f x z (s (s (s (s (s (s (s y))))))) z) (f (s (s (s x))) |0| (s (s (s (s y)))) z) )
(rule (f x z (s (s (s (s (s (s |0|)))))) z) (f x z (s (s (s (s (s (s (s (s (s (s (s x))))))))))) |0|) )