YES Problem: f(0(),1(),X) -> f(X,X,X) g(X,Y) -> X g(X,Y) -> Y Proof: DP Processor: DPs: f#(0(),1(),X) -> f#(X,X,X) TRS: f(0(),1(),X) -> f(X,X,X) g(X,Y) -> X g(X,Y) -> Y EDG Processor: DPs: f#(0(),1(),X) -> f#(X,X,X) TRS: f(0(),1(),X) -> f(X,X,X) g(X,Y) -> X g(X,Y) -> Y graph: Qed