MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 ge(x,0()) -> true() 0.08/0.18 ge(0(),s(y)) -> false() 0.08/0.18 ge(s(x),s(y)) -> ge(x,y) 0.08/0.18 minus(x,0()) -> x 0.08/0.18 minus(0(),y) -> 0() 0.08/0.18 minus(s(x),s(y)) -> minus(x,y) 0.08/0.18 id_inc(x) -> x 0.08/0.18 id_inc(x) -> s(x) 0.08/0.18 quot(x,y) -> div(x,y,0()) 0.08/0.18 div(x,y,z) -> if(ge(y,s(0())),ge(x,y),x,y,z) 0.08/0.18 if(false(),b,x,y,z) -> div_by_zero() 0.08/0.18 if(true(),false(),x,y,z) -> z 0.08/0.18 if(true(),true(),x,y,z) -> div(minus(x,y),y,id_inc(z)) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.18 EOF