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) Usable Rule 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))) ADG 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))) 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) Restore Modifier: 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) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/25 DPs: 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) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0 + 1, [1] = 1, [h](x0) = x0 + 1, [0] = 0, [g](x0) = x0, [d](x0) = x0, [c](x0) = x0, [f](x0) = 0 orientation: g#(h(x)) = x + 2 >= x + 1 = g#(x) f(f(x)) = 0 >= 0 = f(c(f(x))) f(f(x)) = 0 >= 0 = f(d(f(x))) g(c(x)) = x >= x = x g(d(x)) = x >= x = x g(c(h(0()))) = 1 >= 1 = g(d(1())) g(c(1())) = 1 >= 1 = g(d(h(0()))) g(h(x)) = x + 1 >= x = g(x) problem: DPs: 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) Qed