MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 f(s(x)) -> f(id_inc(c(x,x))) 0.08/0.18 f(c(s(x),y)) -> g(c(x,y)) 0.08/0.18 g(c(s(x),y)) -> g(c(y,x)) 0.08/0.18 g(c(x,s(y))) -> g(c(y,x)) 0.08/0.18 g(c(x,x)) -> f(x) 0.08/0.18 id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) 0.08/0.18 id_inc(s(x)) -> s(id_inc(x)) 0.08/0.18 id_inc(0()) -> 0() 0.08/0.18 id_inc(0()) -> s(0()) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.19 EOF