Term Rewriting System R:

   [X, Y, X1, X2]
   a__f(g(X), Y) -> a__f(mark(X), f(g(X), Y))
   a__f(X1, X2) -> f(X1, X2)
   mark(f(X1, X2)) -> a__f(mark(X1), X2)
   mark(g(X)) -> g(mark(X))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   MARK(f(X1, X2)) -> A__F(mark(X1), X2)
   MARK(f(X1, X2)) -> MARK(X1)
   MARK(g(X)) -> MARK(X)
   A__F(g(X), Y) -> A__F(mark(X), f(g(X), Y))
   A__F(g(X), Y) -> MARK(X)

Furthermore, R contains one SCC.


SCC1:

MARK(g(X)) -> MARK(X)
MARK(f(X1, X2)) -> MARK(X1)
A__F(g(X), Y) -> MARK(X)
A__F(g(X), Y) -> A__F(mark(X), f(g(X), Y))
MARK(f(X1, X2)) -> A__F(mark(X1), X2)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__f(g(X), Y) -> a__f(mark(X), f(g(X), Y))
   a__f(X1, X2) -> f(X1, X2)
   mark(f(X1, X2)) -> a__f(mark(X1), X2)
   mark(g(X)) -> g(mark(X))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(g(x_1)) = 1 + x_1
POL(a__f(x_1, x_2)) = 1 + x_1
POL(A__F(x_1, x_2)) = x_1
POL(mark(x_1)) = x_1
POL(MARK(x_1)) = x_1
POL(f(x_1, x_2)) = 1 + x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.602 seconds.