YES Problem: a__f(f(a())) -> a__f(g(f(a()))) mark(f(X)) -> a__f(X) mark(a()) -> a() mark(g(X)) -> g(mark(X)) a__f(X) -> f(X) Proof: DP Processor: DPs: a__f#(f(a())) -> a__f#(g(f(a()))) mark#(f(X)) -> a__f#(X) mark#(g(X)) -> mark#(X) TRS: a__f(f(a())) -> a__f(g(f(a()))) mark(f(X)) -> a__f(X) mark(a()) -> a() mark(g(X)) -> g(mark(X)) a__f(X) -> f(X) TDG Processor: DPs: a__f#(f(a())) -> a__f#(g(f(a()))) mark#(f(X)) -> a__f#(X) mark#(g(X)) -> mark#(X) TRS: a__f(f(a())) -> a__f(g(f(a()))) mark(f(X)) -> a__f(X) mark(a()) -> a() mark(g(X)) -> g(mark(X)) a__f(X) -> f(X) graph: mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(g(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(X) mark#(f(X)) -> a__f#(X) -> a__f#(f(a())) -> a__f#(g(f(a()))) a__f#(f(a())) -> a__f#(g(f(a()))) -> a__f#(f(a())) -> a__f#(g(f(a()))) EDG Processor: DPs: a__f#(f(a())) -> a__f#(g(f(a()))) mark#(f(X)) -> a__f#(X) mark#(g(X)) -> mark#(X) TRS: a__f(f(a())) -> a__f(g(f(a()))) mark(f(X)) -> a__f(X) mark(a()) -> a() mark(g(X)) -> g(mark(X)) a__f(X) -> f(X) graph: mark#(g(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(X) mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X) mark#(f(X)) -> a__f#(X) -> a__f#(f(a())) -> a__f#(g(f(a()))) CDG Processor: DPs: a__f#(f(a())) -> a__f#(g(f(a()))) mark#(f(X)) -> a__f#(X) mark#(g(X)) -> mark#(X) TRS: a__f(f(a())) -> a__f(g(f(a()))) mark(f(X)) -> a__f(X) mark(a()) -> a() mark(g(X)) -> g(mark(X)) a__f(X) -> f(X) graph: Qed