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) TDG 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) 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()) EDG 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) graph: Qed