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