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

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

f(n__a, X, X) → f(activate(X), b, n__b)
ba
an__a
bn__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a



QTRS
  ↳ DependencyPairsProof

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

f(n__a, X, X) → f(activate(X), b, n__b)
ba
an__a
bn__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a


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

F(n__a, X, X) → B
F(n__a, X, X) → ACTIVATE(X)
ACTIVATE(n__a) → A
ACTIVATE(n__b) → B
F(n__a, X, X) → F(activate(X), b, n__b)
BA

The TRS R consists of the following rules:

f(n__a, X, X) → f(activate(X), b, n__b)
ba
an__a
bn__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a

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:

F(n__a, X, X) → B
F(n__a, X, X) → ACTIVATE(X)
ACTIVATE(n__a) → A
ACTIVATE(n__b) → B
F(n__a, X, X) → F(activate(X), b, n__b)
BA

The TRS R consists of the following rules:

f(n__a, X, X) → f(activate(X), b, n__b)
ba
an__a
bn__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP
          ↳ UsableRulesProof
          ↳ UsableRulesProof

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

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

f(n__a, X, X) → f(activate(X), b, n__b)
ba
an__a
bn__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
QDP
              ↳ QReductionProof
          ↳ UsableRulesProof

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

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(n__a, x0, x0)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
QDP
                  ↳ Narrowing
          ↳ UsableRulesProof

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

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
a

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, X, X) → F(activate(X), b, n__b) at position [0] we obtained the following new rules:

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
QDP
                      ↳ DependencyGraphProof
          ↳ UsableRulesProof

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

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
a

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
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
QDP
                          ↳ UsableRulesProof
          ↳ UsableRulesProof

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

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
a

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
          ↳ UsableRulesProof

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

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
a

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

activate(x0)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ Narrowing
          ↳ UsableRulesProof

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

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, x0, x0) → F(x0, b, n__b) at position [1] we obtained the following new rules:

F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
QDP
                                      ↳ Rewriting
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(n__a, y0, y0) → F(y0, a, n__b) at position [1] we obtained the following new rules:

F(n__a, y0, y0) → F(y0, n__a, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
QDP
                                          ↳ DependencyGraphProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, y0, y0) → F(y0, n__a, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

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
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
QDP
                                              ↳ Narrowing
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, n__b, n__b) → F(b, b, n__b) at position [0] we obtained the following new rules:

F(n__a, n__b, n__b) → F(n__b, b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
QDP
                                                  ↳ DependencyGraphProof
          ↳ UsableRulesProof

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

F(n__a, n__b, n__b) → F(n__b, b, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

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
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
QDP
                                                      ↳ Rewriting
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(n__a, n__b, n__b) → F(a, b, n__b) at position [0] we obtained the following new rules:

F(n__a, n__b, n__b) → F(n__a, b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
QDP
                                                          ↳ Narrowing
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, n__b, n__b) → F(n__a, b, n__b) at position [1] we obtained the following new rules:

F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
QDP
                                                              ↳ UsableRulesProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:

ba
bn__b
an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
QDP
                                                                  ↳ QReductionProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:

an__a

The set Q consists of the following terms:

b
a

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

b



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
QDP
                                                                      ↳ Rewriting
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:

an__a

The set Q consists of the following terms:

a

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(n__a, n__b, n__b) → F(n__a, a, n__b) at position [1] we obtained the following new rules:

F(n__a, n__b, n__b) → F(n__a, n__a, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
QDP
                                                                          ↳ DependencyGraphProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:

an__a

The set Q consists of the following terms:

a

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
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ DependencyGraphProof
QDP
                                                                              ↳ UsableRulesProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:

an__a

The set Q consists of the following terms:

a

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ DependencyGraphProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesProof
QDP
                                                                                  ↳ QReductionProof
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

R is empty.
The set Q consists of the following terms:

a

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

a



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ DependencyGraphProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesProof
                                                                                ↳ QDP
                                                                                  ↳ QReductionProof
QDP
                                                                                      ↳ Instantiation
          ↳ UsableRulesProof

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

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule F(n__a, y0, y0) → F(y0, n__b, n__b) we obtained the following new rules:

F(n__a, n__b, n__b) → F(n__b, n__b, n__b)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ DependencyGraphProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesProof
                                                                                ↳ QDP
                                                                                  ↳ QReductionProof
                                                                                    ↳ QDP
                                                                                      ↳ Instantiation
QDP
                                                                                          ↳ DependencyGraphProof
          ↳ UsableRulesProof

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

F(n__a, n__b, n__b) → F(n__b, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

R is empty.
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
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Narrowing
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ Narrowing
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Narrowing
                                                            ↳ QDP
                                                              ↳ UsableRulesProof
                                                                ↳ QDP
                                                                  ↳ QReductionProof
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ DependencyGraphProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesProof
                                                                                ↳ QDP
                                                                                  ↳ QReductionProof
                                                                                    ↳ QDP
                                                                                      ↳ Instantiation
                                                                                        ↳ QDP
                                                                                          ↳ DependencyGraphProof
QDP
                                                                                              ↳ NonTerminationProof
          ↳ UsableRulesProof

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

F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

The TRS R consists of the following rules:none


s = F(n__a, n__b, n__b) evaluates to t =F(n__a, n__b, n__b)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from F(n__a, n__b, n__b) to F(n__a, n__b, n__b).




As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
          ↳ UsableRulesProof
QDP
              ↳ QReductionProof

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

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
f(n__a, x0, x0)
a

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(n__a, x0, x0)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
QDP
                  ↳ NonTerminationProof

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

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a

The set Q consists of the following terms:

activate(x0)
b
a

We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the right:

The TRS P consists of the following rules:

F(n__a, X, X) → F(activate(X), b, n__b)

The TRS R consists of the following rules:

activate(n__a) → a
activate(n__b) → b
activate(X) → X
ba
bn__b
an__a


s = F(n__a, n__b, n__b) evaluates to t =F(n__a, n__b, n__b)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

F(n__a, n__b, n__b)F(activate(n__b), b, n__b)
with rule F(n__a, X, X) → F(activate(X), b, n__b) and matcher [X / n__b].

F(activate(n__b), b, n__b)F(b, b, n__b)
with rule activate(n__b) → b at position [0] and matcher [ ]

F(b, b, n__b)F(a, b, n__b)
with rule ba at position [0] and matcher [ ]

F(a, b, n__b)F(n__a, b, n__b)
with rule an__a at position [0] and matcher [ ]

F(n__a, b, n__b)F(n__a, n__b, n__b)
with rule bn__b at position [1] and matcher [ ]

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.