MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 f(0()) -> 0() 0.08/0.19 f(s(0())) -> s(0()) 0.08/0.19 f(s(s(x))) -> p(h(g(x))) 0.08/0.19 g(0()) -> pair(s(0()),s(0())) 0.08/0.19 g(s(x)) -> h(g(x)) 0.08/0.19 h(x) -> pair(+(p(x),q(x)),p(x)) 0.08/0.19 p(pair(x,y)) -> x 0.08/0.19 q(pair(x,y)) -> y 0.08/0.19 +(x,0()) -> x 0.08/0.19 +(x,s(y)) -> s(+(x,y)) 0.08/0.19 f(s(s(x))) -> +(p(g(x)),q(g(x))) 0.08/0.19 g(s(x)) -> pair(+(p(g(x)),q(g(x))),p(g(x))) 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.20 EOF