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