MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 check(0()) -> zero() 0.08/0.19 check(s(0())) -> odd() 0.08/0.19 check(s(s(0()))) -> even() 0.08/0.19 check(s(s(s(x)))) -> check(s(x)) 0.08/0.19 half(0()) -> 0() 0.08/0.19 half(s(0())) -> 0() 0.08/0.19 half(s(s(x))) -> s(half(x)) 0.08/0.19 plus(0(),y) -> y 0.08/0.19 plus(s(x),y) -> s(plus(x,y)) 0.08/0.19 times(x,y) -> timesIter(x,y,0()) 0.08/0.19 timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y)) 0.08/0.19 p(s(x)) -> x 0.08/0.19 p(0()) -> 0() 0.08/0.19 if(zero(),x,y,z,u) -> z 0.08/0.19 if(odd(),x,y,z,u) -> timesIter(p(x),y,u) 0.08/0.19 if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z)))) 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF