MAYBE 0.09/0.17 MAYBE 0.09/0.17 0.09/0.17 Problem: 0.09/0.17 p(0()) -> s(s(0())) 0.09/0.17 p(s(x)) -> x 0.09/0.17 p(p(s(x))) -> p(x) 0.09/0.17 le(p(s(x)),x) -> le(x,x) 0.09/0.17 le(0(),y) -> true() 0.09/0.17 le(s(x),0()) -> false() 0.09/0.17 le(s(x),s(y)) -> le(x,y) 0.09/0.17 minus(x,y) -> if(le(x,y),x,y) 0.09/0.17 if(true(),x,y) -> 0() 0.09/0.17 if(false(),x,y) -> s(minus(p(x),y)) 0.09/0.17 0.09/0.17 Proof: 0.09/0.17 Open 0.09/0.17 EOF