MAYBE 0.09/0.17 MAYBE 0.09/0.17 0.09/0.17 Problem: 0.09/0.17 times(x,y) -> help(x,y,0()) 0.09/0.17 help(x,y,c) -> if(lt(c,y),x,y,c) 0.09/0.17 if(true(),x,y,c) -> plus(x,help(x,y,s(c))) 0.09/0.17 if(false(),x,y,c) -> 0() 0.09/0.17 lt(0(),s(x)) -> true() 0.09/0.17 lt(s(x),0()) -> false() 0.09/0.17 lt(s(x),s(y)) -> lt(x,y) 0.09/0.17 plus(x,0()) -> x 0.09/0.17 plus(0(),x) -> x 0.09/0.17 plus(x,s(y)) -> s(plus(x,y)) 0.09/0.17 plus(s(x),y) -> s(plus(x,y)) 0.09/0.17 0.09/0.17 Proof: 0.09/0.17 Open 0.09/0.19 EOF