YES Problem: a__f(g(X),Y) -> a__f(mark(X),f(g(X),Y)) mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X)) -> g(mark(X)) a__f(X1,X2) -> f(X1,X2) Proof: WPO Processor: algebra: Max weight function: w0 = 0 w(f) = w(a__f) = 7 w(g) = 6 w(mark) = 0 status function: st(f) = [0, 1] st(mark) = [0] st(a__f) = [0, 1] st(g) = [0] subterm penalty function: sp(g, 0) = 4 sp(f, 1) = sp(f, 0) = sp(mark, 0) = sp(a__f, 1) = sp(a__f, 0) = 0 precedence: mark > a__f > f ~ g problem: Qed