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