Term Rewriting System R:
[x]
a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

A(f, a(f, a(g, a(g, x)))) -> A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) -> A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) -> A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, a(f, x)))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) -> A(f, x)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, x)))) -> A(f, x)
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, a(f, x)))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, a(f, x)))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, x'')))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, a(g, a(g, x'')))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) -> A(f, x)


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, x'')))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, x)
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Forward Instantiation Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, x)
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, x)))) -> A(f, x)
four new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 9
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 10
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 11
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 12
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 13
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 14
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 15
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 16
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 17
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x''))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 18
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 19
                 ↳Narrowing Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x')))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x')))))))))))))))))))
two new Dependency Pairs are created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 20
                 ↳Rewriting Transformation


Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))))))))))))))))))
one new Dependency Pair is created:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 21
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''))))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x''))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x')))))))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'')))))))))))) -> A(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x''')))))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(g, a(g, x'))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x'))))))))))))))))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))))) -> A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, x'''))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))))) -> A(f, a(f, a(g, a(g, a(f, a(g, a(g, x'''')))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, x''))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x''))))))) -> A(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x''))))))))
A(f, a(f, a(g, a(g, x)))) -> A(f, a(f, x))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, a(g, x'')))))))))))))) -> A(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, x'')))))))))))))))))))))))


Rule:


a(f, a(f, a(g, a(g, x)))) -> a(g, a(g, a(g, a(f, a(f, a(f, x))))))


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:09 minutes