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