Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)))
A(f, a(f, a(g, a(g, x)))) → A(f, x)

The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

We have to consider all minimal (P,Q,R)-chains.

(7) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)

The TRS R consists of the following rules:

f(f(g(g(x)))) → g(g(g(f(f(f(x))))))

The set Q consists of the following terms:

f(f(g(g(x0))))

We have to consider all minimal (P,Q,R)-chains.

(9) RFCMatchBoundsDPProof (EQUIVALENT transformation)

Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)

To find matches we regarded all rules of R and P:

f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1144691, 1144692, 1144693, 1144694, 1144695, 1144696, 1144697, 1144701, 1144699, 1144700, 1144698, 1144702, 1144703, 1144707, 1144708, 1144704, 1144705, 1144706, 1144710, 1144711, 1144713, 1144709, 1144712, 1144715, 1144714, 1144717, 1144718, 1144716, 1144720, 1144719, 1144722, 1144723, 1144721, 1144725, 1144724, 1144726, 1144727, 1144728, 1144729, 1144730

Node 1144691 is start node and node 1144692 is final node.

Those nodes are connect through the following edges:

• 1144691 to 1144693 labelled f1_1(0)
• 1144691 to 1144694 labelled f1_1(0)
• 1144691 to 1144692 labelled f1_1(0), f1_1(1)
• 1144691 to 1144695 labelled f1_1(1)
• 1144691 to 1144696 labelled f1_1(1)
• 1144691 to 1144700 labelled f1_1(1)
• 1144691 to 1144701 labelled f1_1(1)
• 1144691 to 1144698 labelled f1_1(1), f1_1(2)
• 1144691 to 1144702 labelled f1_1(2)
• 1144691 to 1144703 labelled f1_1(2)
• 1144691 to 1144712 labelled f1_1(2)
• 1144691 to 1144713 labelled f1_1(2)
• 1144691 to 1144704 labelled f1_1(2)
• 1144691 to 1144714 labelled f1_1(3)
• 1144691 to 1144715 labelled f1_1(3)
• 1144691 to 1144706 labelled f1_1(3)
• 1144691 to 1144710 labelled f1_1(3)
• 1144691 to 1144729 labelled f1_1(4)
• 1144691 to 1144730 labelled f1_1(4)
• 1144691 to 1144722 labelled f1_1(4)
• 1144692 to 1144692 labelled #_1(0)
• 1144693 to 1144694 labelled f_1(0)
• 1144693 to 1144697 labelled g_1(1)
• 1144694 to 1144692 labelled f_1(0)
• 1144694 to 1144697 labelled g_1(1)
• 1144695 to 1144696 labelled f_1(1)
• 1144695 to 1144697 labelled g_1(1)
• 1144696 to 1144692 labelled f_1(1)
• 1144696 to 1144697 labelled g_1(1)
• 1144697 to 1144698 labelled g_1(1)
• 1144701 to 1144692 labelled f_1(1)
• 1144701 to 1144697 labelled g_1(1)
• 1144701 to 1144698 labelled f_1(1)
• 1144699 to 1144700 labelled f_1(1)
• 1144699 to 1144704 labelled g_1(2)
• 1144700 to 1144701 labelled f_1(1)
• 1144700 to 1144697 labelled g_1(1)
• 1144700 to 1144709 labelled g_1(2)
• 1144698 to 1144699 labelled g_1(1)
• 1144702 to 1144703 labelled f_1(2)
• 1144702 to 1144709 labelled g_1(2)
• 1144703 to 1144698 labelled f_1(2)
• 1144707 to 1144708 labelled f_1(2)
• 1144707 to 1144709 labelled g_1(2)
• 1144708 to 1144698 labelled f_1(2)
• 1144704 to 1144705 labelled g_1(2)
• 1144705 to 1144706 labelled g_1(2)
• 1144706 to 1144707 labelled f_1(2)
• 1144710 to 1144711 labelled g_1(2)
• 1144711 to 1144712 labelled f_1(2)
• 1144713 to 1144704 labelled f_1(2)
• 1144709 to 1144710 labelled g_1(2)
• 1144712 to 1144713 labelled f_1(2)
• 1144712 to 1144716 labelled g_1(3)
• 1144715 to 1144706 labelled f_1(3)
• 1144715 to 1144710 labelled f_1(3)
• 1144715 to 1144721 labelled g_1(3)
• 1144714 to 1144715 labelled f_1(3)
• 1144717 to 1144718 labelled g_1(3)
• 1144718 to 1144719 labelled f_1(3)
• 1144718 to 1144726 labelled g_1(4)
• 1144716 to 1144717 labelled g_1(3)
• 1144720 to 1144706 labelled f_1(3)
• 1144720 to 1144721 labelled g_1(3)
• 1144719 to 1144720 labelled f_1(3)
• 1144722 to 1144723 labelled g_1(3)
• 1144723 to 1144724 labelled f_1(3)
• 1144721 to 1144722 labelled g_1(3)
• 1144725 to 1144710 labelled f_1(3)
• 1144724 to 1144725 labelled f_1(3)
• 1144726 to 1144727 labelled g_1(4)
• 1144727 to 1144728 labelled g_1(4)
• 1144728 to 1144729 labelled f_1(4)
• 1144729 to 1144730 labelled f_1(4)
• 1144730 to 1144722 labelled f_1(4)

(10) TRUE