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:

f(s(a), s(b), x) → f(x, x, x)
g(f(s(x), s(y), z)) → g(f(x, y, z))
cons(x, y) → x
cons(x, y) → y

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)



↳ QTRS
  ↳ DependencyPairsProof

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

f(s(a), s(b), x) → f(x, x, x)
g(f(s(x), s(y), z)) → g(f(x, y, z))
cons(x, y) → x
cons(x, y) → y

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)


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

G(f(s(x), s(y), z)) → G(f(x, y, z))
G(f(s(x), s(y), z)) → F(x, y, z)
F(s(a), s(b), x) → F(x, x, x)

The TRS R consists of the following rules:

f(s(a), s(b), x) → f(x, x, x)
g(f(s(x), s(y), z)) → g(f(x, y, z))
cons(x, y) → x
cons(x, y) → y

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)

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:

G(f(s(x), s(y), z)) → G(f(x, y, z))
G(f(s(x), s(y), z)) → F(x, y, z)
F(s(a), s(b), x) → F(x, x, x)

The TRS R consists of the following rules:

f(s(a), s(b), x) → f(x, x, x)
g(f(s(x), s(y), z)) → g(f(x, y, z))
cons(x, y) → x
cons(x, y) → y

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)

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
          ↳ UsableRulesProof

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

G(f(s(x), s(y), z)) → G(f(x, y, z))

The TRS R consists of the following rules:

f(s(a), s(b), x) → f(x, x, x)
g(f(s(x), s(y), z)) → g(f(x, y, z))
cons(x, y) → x
cons(x, y) → y

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)

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

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

G(f(s(x), s(y), z)) → G(f(x, y, z))

The TRS R consists of the following rules:

f(s(a), s(b), x) → f(x, x, x)

The set Q consists of the following terms:

g(f(s(x0), s(x1), x2))
f(s(a), s(b), x0)
cons(x0, x1)

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.

g(f(s(x0), s(x1), x2))
cons(x0, x1)



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

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

G(f(s(x), s(y), z)) → G(f(x, y, z))

The TRS R consists of the following rules:

f(s(a), s(b), x) → f(x, x, x)

The set Q consists of the following terms:

f(s(a), s(b), x0)

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.a: 0
f: 0
s: x0
b: 1
G: 0
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

G.0(f.1-1-1(s.1(x), s.1(y), z)) → G.0(f.1-1-1(x, y, z))
G.0(f.1-1-0(s.1(x), s.1(y), z)) → G.0(f.1-1-0(x, y, z))
G.0(f.0-0-0(s.0(x), s.0(y), z)) → G.0(f.0-0-0(x, y, z))
G.0(f.1-0-0(s.1(x), s.0(y), z)) → G.0(f.1-0-0(x, y, z))
G.0(f.0-0-1(s.0(x), s.0(y), z)) → G.0(f.0-0-1(x, y, z))
G.0(f.0-1-0(s.0(x), s.1(y), z)) → G.0(f.0-1-0(x, y, z))
G.0(f.0-1-1(s.0(x), s.1(y), z)) → G.0(f.0-1-1(x, y, z))
G.0(f.1-0-1(s.1(x), s.0(y), z)) → G.0(f.1-0-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

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

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

G.0(f.1-1-1(s.1(x), s.1(y), z)) → G.0(f.1-1-1(x, y, z))
G.0(f.1-1-0(s.1(x), s.1(y), z)) → G.0(f.1-1-0(x, y, z))
G.0(f.0-0-0(s.0(x), s.0(y), z)) → G.0(f.0-0-0(x, y, z))
G.0(f.1-0-0(s.1(x), s.0(y), z)) → G.0(f.1-0-0(x, y, z))
G.0(f.0-0-1(s.0(x), s.0(y), z)) → G.0(f.0-0-1(x, y, z))
G.0(f.0-1-0(s.0(x), s.1(y), z)) → G.0(f.0-1-0(x, y, z))
G.0(f.0-1-1(s.0(x), s.1(y), z)) → G.0(f.0-1-1(x, y, z))
G.0(f.1-0-1(s.1(x), s.0(y), z)) → G.0(f.1-0-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

G.0(f.1-1-1(s.1(x), s.1(y), z)) → G.0(f.1-1-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.1-1-1(s.1(x), s.1(y), z)) → G.0(f.1-1-1(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.1-1-1(x1, x2, x3)) = x1 + x2 + x3   
POL(s.1(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

G.0(f.1-1-0(s.1(x), s.1(y), z)) → G.0(f.1-1-0(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.1-1-0(s.1(x), s.1(y), z)) → G.0(f.1-1-0(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.1-1-0(x1, x2, x3)) = x1 + x2 + x3   
POL(s.1(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

G.0(f.1-0-1(s.1(x), s.0(y), z)) → G.0(f.1-0-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.1-0-1(s.1(x), s.0(y), z)) → G.0(f.1-0-1(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.1-0-1(x1, x2, x3)) = x1 + x2 + x3   
POL(s.0(x1)) = x1   
POL(s.1(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

G.0(f.1-0-0(s.1(x), s.0(y), z)) → G.0(f.1-0-0(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.1-0-0(s.1(x), s.0(y), z)) → G.0(f.1-0-0(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.1-0-0(x1, x2, x3)) = x1 + x2 + x3   
POL(s.0(x1)) = x1   
POL(s.1(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

G.0(f.0-0-1(s.0(x), s.0(y), z)) → G.0(f.0-0-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.0-0-1(s.0(x), s.0(y), z)) → G.0(f.0-0-1(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.0-0-1(x1, x2, x3)) = x1 + x2 + x3   
POL(s.0(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                          ↳ QDP
                          ↳ QDP

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

G.0(f.0-0-0(s.0(x), s.0(y), z)) → G.0(f.0-0-0(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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:

G.0(f.0-0-0(s.0(x), s.0(y), z)) → G.0(f.0-0-0(x, y, z))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(f.0-0-0(x1, x2, x3)) = x1 + x2 + x3   
POL(s.0(x1)) = x1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP

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

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof
                          ↳ QDP

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

G.0(f.0-1-1(s.0(x), s.1(y), z)) → G.0(f.0-1-1(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


G.0(f.0-1-1(s.0(x), s.1(y), z)) → G.0(f.0-1-1(x, y, z))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(a.) = 0   
POL(b.) = 0   
POL(f.0-1-1(x1, x2, x3)) = x2 + x3   
POL(f.1-1-1(x1, x2, x3)) = 0   
POL(s.0(x1)) = 0   
POL(s.1(x1)) = 1 + x1   

The following usable rules [17] were oriented:

f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof

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

G.0(f.0-1-0(s.0(x), s.1(y), z)) → G.0(f.0-1-0(x, y, z))

The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


G.0(f.0-1-0(s.0(x), s.1(y), z)) → G.0(f.0-1-0(x, y, z))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(G.0(x1)) = x1   
POL(a.) = 0   
POL(b.) = 0   
POL(f.0-0-0(x1, x2, x3)) = 0   
POL(f.0-1-0(x1, x2, x3)) = x2 + x3   
POL(s.0(x1)) = 0   
POL(s.1(x1)) = 1 + x1   

The following usable rules [17] were oriented:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ QReductionProof
                ↳ QDP
                  ↳ SemLabProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f.0-1-0(s.0(a.), s.1(b.), x) → f.0-0-0(x, x, x)
f.0-1-1(s.0(a.), s.1(b.), x) → f.1-1-1(x, x, x)

The set Q consists of the following terms:

f.0-1-0(s.0(a.), s.1(b.), x0)
f.0-1-1(s.0(a.), s.1(b.), x0)

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