YES Problem: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Proof: DP Processor: DPs: f#(1()) -> g#(1()) f#(1()) -> f#(g(1())) g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Usable Rule Processor: DPs: f#(1()) -> g#(1()) f#(1()) -> f#(g(1())) g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: TDG Processor: DPs: f#(1()) -> g#(1()) f#(1()) -> f#(g(1())) g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: graph: g#(0()) -> g#(f(0())) -> g#(0()) -> g#(f(0())) g#(0()) -> g#(f(0())) -> g#(0()) -> f#(0()) g#(0()) -> f#(0()) -> f#(1()) -> f#(g(1())) g#(0()) -> f#(0()) -> f#(1()) -> g#(1()) f#(1()) -> g#(1()) -> g#(0()) -> g#(f(0())) f#(1()) -> g#(1()) -> g#(0()) -> f#(0()) f#(1()) -> f#(g(1())) -> f#(1()) -> f#(g(1())) f#(1()) -> f#(g(1())) -> f#(1()) -> g#(1()) Restore Modifier: DPs: f#(1()) -> g#(1()) f#(1()) -> f#(g(1())) g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) SCC Processor: #sccs: 1 #rules: 4 #arcs: 8/16 DPs: g#(0()) -> g#(f(0())) g#(0()) -> f#(0()) f#(1()) -> g#(1()) f#(1()) -> f#(g(1())) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [f#](x0) = x0, [0] = 0, [g](x0) = 0, [f](x0) = 0, [1] = 1 orientation: g#(0()) = 0 >= 0 = g#(f(0())) g#(0()) = 0 >= 0 = f#(0()) f#(1()) = 1 >= 1 = g#(1()) f#(1()) = 1 >= 0 = f#(g(1())) f(1()) = 0 >= 0 = f(g(1())) f(f(x)) = 0 >= 0 = f(x) g(0()) = 0 >= 0 = g(f(0())) g(g(x)) = 0 >= 0 = g(x) problem: DPs: g#(0()) -> g#(f(0())) g#(0()) -> f#(0()) f#(1()) -> g#(1()) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = 0, [f#](x0) = x0, [0] = 0, [g](x0) = 0, [f](x0) = 0, [1] = 1 orientation: g#(0()) = 0 >= 0 = g#(f(0())) g#(0()) = 0 >= 0 = f#(0()) f#(1()) = 1 >= 0 = g#(1()) f(1()) = 0 >= 0 = f(g(1())) f(f(x)) = 0 >= 0 = f(x) g(0()) = 0 >= 0 = g(f(0())) g(g(x)) = 0 >= 0 = g(x) problem: DPs: g#(0()) -> g#(f(0())) g#(0()) -> f#(0()) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = 1, [f#](x0) = 0, [0] = 0, [g](x0) = 0, [f](x0) = 0, [1] = 0 orientation: g#(0()) = 1 >= 1 = g#(f(0())) g#(0()) = 1 >= 0 = f#(0()) f(1()) = 0 >= 0 = f(g(1())) f(f(x)) = 0 >= 0 = f(x) g(0()) = 0 >= 0 = g(f(0())) g(g(x)) = 0 >= 0 = g(x) problem: DPs: g#(0()) -> g#(f(0())) TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [0] = 1, [g](x0) = 0, [f](x0) = 0, [1] = 0 orientation: g#(0()) = 1 >= 0 = g#(f(0())) f(1()) = 0 >= 0 = f(g(1())) f(f(x)) = 0 >= 0 = f(x) g(0()) = 0 >= 0 = g(f(0())) g(g(x)) = 0 >= 0 = g(x) problem: DPs: TRS: f(1()) -> f(g(1())) f(f(x)) -> f(x) g(0()) -> g(f(0())) g(g(x)) -> g(x) Qed