MAYBE Problem: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Proof: DP Processor: DPs: cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) gr#(s(x),s(y)) -> gr#(x,y) TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Open