MAYBE 0.09/0.18 MAYBE 0.09/0.18 0.09/0.18 Problem: 0.09/0.18 minus(x,0()) -> x 0.09/0.18 minus(0(),y) -> 0() 0.09/0.18 minus(s(x),s(y)) -> minus(p(s(x)),p(s(y))) 0.09/0.18 minus(x,plus(y,z)) -> minus(minus(x,y),z) 0.09/0.18 p(s(s(x))) -> s(p(s(x))) 0.09/0.18 p(0()) -> s(s(0())) 0.09/0.18 div(s(x),s(y)) -> s(div(minus(x,y),s(y))) 0.09/0.18 div(plus(x,y),z) -> plus(div(x,z),div(y,z)) 0.09/0.18 plus(0(),y) -> y 0.09/0.18 plus(s(x),y) -> s(plus(y,minus(s(x),s(0())))) 0.09/0.18 0.09/0.18 Proof: 0.09/0.18 Open 0.09/0.18 EOF