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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Proof: DP Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) TDG Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) graph: g#(h(x)) -> g#(x) -> g#(h(x)) -> g#(x) g#(h(x)) -> g#(x) -> g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) -> g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) -> g#(h(x)) -> g#(x) g#(c(1())) -> g#(d(h(0()))) -> g#(c(1())) -> g#(d(h(0()))) g#(c(1())) -> g#(d(h(0()))) -> g#(c(h(0()))) -> g#(d(1())) g#(c(h(0()))) -> g#(d(1())) -> g#(h(x)) -> g#(x) g#(c(h(0()))) -> g#(d(1())) -> g#(c(1())) -> g#(d(h(0()))) g#(c(h(0()))) -> g#(d(1())) -> g#(c(h(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: 5 #arcs: 13/25 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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) 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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) graph: Qed DPs: g#(h(x)) -> g#(x) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) EDG Processor: DPs: g#(h(x)) -> g#(x) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) graph: g#(h(x)) -> g#(x) -> g#(c(h(0()))) -> g#(d(1())) g#(h(x)) -> g#(x) -> g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) -> g#(h(x)) -> g#(x) CDG Processor: DPs: g#(h(x)) -> g#(x) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) graph: Qed