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

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

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

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

The TRS R consists of the following rules:

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

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(x, g) → A(f, a(g, a(f, x))) at position [1] we obtained the following new rules:

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



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ DependencyGraphProof

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ QDP
                  ↳ SemLabProof

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.f: 0
a: 0
g: 1
A: 0
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

A.0-1(a.0-1(f., x0), g.) → A.0-0(f., a.1-0(g., a.1-1(x0, g.)))
A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-1(x, g.) → A.0-0(f., x)
A.0-1(a.0-0(f., x0), g.) → A.0-0(f., a.1-0(g., a.0-1(x0, g.)))
A.1-1(x, g.) → A.0-1(f., x)

The TRS R consists of the following rules:

a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., x)))

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof

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

A.0-1(a.0-1(f., x0), g.) → A.0-0(f., a.1-0(g., a.1-1(x0, g.)))
A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-1(x, g.) → A.0-0(f., x)
A.0-1(a.0-0(f., x0), g.) → A.0-0(f., a.1-0(g., a.0-1(x0, g.)))
A.1-1(x, g.) → A.0-1(f., x)

The TRS R consists of the following rules:

a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesReductionPairsProof

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

A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-1(x, g.) → A.0-0(f., x)
A.1-1(x, g.) → A.0-1(f., x)

The TRS R consists of the following rules:

a.0-0(f., a.0-0(f., x)) → a.0-1(x, g.)
a.0-1(x, g.) → a.0-0(f., a.1-0(g., a.0-0(f., x)))
a.0-0(f., a.0-1(f., x)) → a.1-1(x, g.)
a.1-1(x, g.) → a.0-0(f., a.1-0(g., a.0-1(f., x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
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.

The following dependency pairs can be deleted:

A.0-0(f., a.0-1(f., x)) → A.1-1(x, g.)
A.0-0(f., a.0-0(f., x)) → A.0-1(x, g.)
A.0-1(x, g.) → A.0-0(f., x)
A.1-1(x, g.) → A.0-1(f., x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(A.0-0(x1, x2)) = 1 + x1 + x2   
POL(A.0-1(x1, x2)) = 1 + x1 + x2   
POL(A.1-1(x1, x2)) = 1 + x1 + x2   
POL(a.0-0(x1, x2)) = 1 + x1 + x2   
POL(a.0-1(x1, x2)) = 1 + x1 + x2   
POL(f.) = 0   
POL(g.) = 1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesReductionPairsProof
                            ↳ QDP
                              ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.