(VAR k l m n )
(RULES 
        f(0, n) -> g(0, n)
        f(m, 0) -> g(m, 0)
        f(s(m), s(n)) -> h(m, n, f(m, p(m, n)), f(s(m), n))
        g(n, m) -> bot
        p(m, n) -> bot
        h(k, l, m, n) -> bot
        
)