MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 nonZero(0()) -> false() 0.08/0.18 nonZero(s(x)) -> true() 0.08/0.18 p(s(0())) -> 0() 0.08/0.18 p(s(s(x))) -> s(p(s(x))) 0.08/0.18 id_inc(x) -> x 0.08/0.18 id_inc(x) -> s(x) 0.08/0.18 random(x) -> rand(x,0()) 0.08/0.18 rand(x,y) -> if(nonZero(x),x,y) 0.08/0.18 if(false(),x,y) -> y 0.08/0.18 if(true(),x,y) -> rand(p(x),id_inc(y)) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.18 EOF