MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) 0.08/0.18 times(x,0()) -> 0() 0.08/0.18 times(x,s(y)) -> plus(times(x,y),x) 0.08/0.18 plus(x,0()) -> x 0.08/0.18 plus(x,s(y)) -> s(plus(x,y)) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.19 EOF