MAYBE Problem: f(g(x),h(x),y,x) -> f(y,y,y,x) f(x,y,z,0()) -> 2() g(0()) -> 2() h(0()) -> 2() Proof: DP Processor: DPs: f#(g(x),h(x),y,x) -> f#(y,y,y,x) TRS: f(g(x),h(x),y,x) -> f(y,y,y,x) f(x,y,z,0()) -> 2() g(0()) -> 2() h(0()) -> 2() Open