MAYBE Problem: nonZero(0()) -> false() nonZero(s(x)) -> true() p(0()) -> 0() p(s(x)) -> x id_inc(x) -> x id_inc(x) -> s(x) random(x) -> rand(x,0()) rand(x,y) -> if(nonZero(x),x,y) if(false(),x,y) -> y if(true(),x,y) -> rand(p(x),id_inc(y)) Proof: DP Processor: DPs: random#(x) -> rand#(x,0()) rand#(x,y) -> nonZero#(x) rand#(x,y) -> if#(nonZero(x),x,y) if#(true(),x,y) -> id_inc#(y) if#(true(),x,y) -> p#(x) if#(true(),x,y) -> rand#(p(x),id_inc(y)) TRS: nonZero(0()) -> false() nonZero(s(x)) -> true() p(0()) -> 0() p(s(x)) -> x id_inc(x) -> x id_inc(x) -> s(x) random(x) -> rand(x,0()) rand(x,y) -> if(nonZero(x),x,y) if(false(),x,y) -> y if(true(),x,y) -> rand(p(x),id_inc(y)) Open