Termination w.r.t. Q proof of /tmp/tmpohnWxT/z03.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

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

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

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

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

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

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

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

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ UsableRulesReductionPairsProof

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
First, we A-transformed [17] the QDP-Problem. Then we obtain the following A-transformed DP problem.
The pairs P are:

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

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

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

Q is empty.

By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(f(x₁)) = x₁
POL(f1(x₁)) = x₁
POL(g(x₁)) = x₁
POL(g1(x₁)) = x₁

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ UsableRulesReductionPairsProof

        ↳ QDP

          ↳ RFCMatchBoundsDPProof

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 2.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

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

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

40, 41, 42, 43, 45, 46, 44, 48, 47, 49, 51, 50, 53, 54, 52, 57, 55, 56, 60, 58, 59, 62, 63, 61

Node 40 is start node and node 41 is final node.

Those nodes are connect through the following edges:

40 to 42 labelled g1_1(0)
40 to 44 labelled f1_1(0)
40 to 47 labelled f1_1(0)
40 to 49 labelled g1_1(0)
41 to 41 labelled #_1(0)
42 to 43 labelled g_1(0)
42 to 55 labelled g_1(1)
43 to 41 labelled f_1(0)
43 to 52 labelled f_1(1)
45 to 46 labelled g_1(0)
45 to 55 labelled g_1(1)
46 to 41 labelled f_1(0)
46 to 52 labelled f_1(1)
44 to 45 labelled g_1(0)
48 to 41 labelled g_1(0)
48 to 55 labelled g_1(1)
47 to 48 labelled f_1(0)
47 to 52 labelled f_1(1)
49 to 50 labelled f_1(0)
51 to 41 labelled g_1(0)
51 to 55 labelled g_1(1)
50 to 51 labelled f_1(0)
50 to 52 labelled f_1(1)
53 to 54 labelled g_1(1)
53 to 55 labelled g_1(1)
53 to 58 labelled g_1(2)
54 to 41 labelled f_1(1)
54 to 52 labelled f_1(1)
52 to 53 labelled g_1(1)
57 to 41 labelled g_1(1)
57 to 55 labelled g_1(1)
55 to 56 labelled f_1(1)
56 to 57 labelled f_1(1)
56 to 52 labelled f_1(1)
56 to 61 labelled f_1(2)
60 to 53 labelled g_1(2)
58 to 59 labelled f_1(2)
59 to 60 labelled f_1(2)
62 to 63 labelled g_1(2)
63 to 56 labelled f_1(2)
61 to 62 labelled g_1(2)