0 QTRS
active(f(X, X)) → mark(f(a, b)) active(b) → mark(a) mark(f(X1, X2)) → active(f(mark(X1), X2)) mark(a) → active(a) mark(b) → active(b) f(mark(X1), X2) → f(X1, X2) f(X1, mark(X2)) → f(X1, X2) f(active(X1), X2) → f(X1, X2) f(X1, active(X2)) → f(X1, X2)