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