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))) SCC Processor: #sccs: 2 #rules: 4 #arcs: 8/16 DPs: f#(f(x)) -> f#(d(f(x))) f#(f(x)) -> f#(c(f(x))) 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())) EDG Processor: DPs: f#(f(x)) -> f#(d(f(x))) f#(f(x)) -> f#(c(f(x))) 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 DPs: g#(c(1())) -> g#(d(0())) g#(c(0())) -> g#(d(1())) 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())) EDG Processor: DPs: g#(c(1())) -> g#(d(0())) g#(c(0())) -> g#(d(1())) 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