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:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof

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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

old(serve) → free(serve)
Used ordering:
Polynomial interpretation [25]:

POL(check(x1)) = x1   
POL(free(x1)) = x1   
POL(new(x1)) = x1   
POL(old(x1)) = 1 + 2·x1   
POL(serve) = 0   
POL(top1(x1, x2)) = x1 + x2   
POL(top2(x1, x2)) = x1 + x2   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof

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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

old(free(x)) → free(old(x))
Used ordering:
Polynomial interpretation [25]:

POL(check(x1)) = x1   
POL(free(x1)) = 1 + x1   
POL(new(x1)) = 1 + x1   
POL(old(x1)) = 2 + 2·x1   
POL(serve) = 0   
POL(top1(x1, x2)) = x1 + x2   
POL(top2(x1, x2)) = x1 + x2   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof

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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(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:

TOP1(free(x), y) → CHECK(y)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
CHECK(free(x)) → CHECK(x)
TOP2(x, free(y)) → TOP1(check(new(x)), y)
TOP1(free(x), y) → CHECK(new(x))
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP2(x, free(y)) → NEW(x)
TOP2(x, free(y)) → CHECK(new(x))
TOP2(x, free(y)) → CHECK(y)
TOP1(free(x), y) → NEW(y)
TOP1(free(x), y) → CHECK(x)
TOP1(free(x), y) → NEW(x)
TOP1(free(x), y) → CHECK(new(y))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(x, free(y)) → NEW(y)
CHECK(new(x)) → CHECK(x)
TOP2(x, free(y)) → CHECK(x)
CHECK(old(x)) → CHECK(x)
TOP2(x, free(y)) → CHECK(new(y))
CHECK(new(x)) → NEW(check(x))
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(x, free(y)) → TOP1(new(x), check(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))
NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

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

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof

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

TOP1(free(x), y) → CHECK(y)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
CHECK(free(x)) → CHECK(x)
TOP2(x, free(y)) → TOP1(check(new(x)), y)
TOP1(free(x), y) → CHECK(new(x))
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP2(x, free(y)) → NEW(x)
TOP2(x, free(y)) → CHECK(new(x))
TOP2(x, free(y)) → CHECK(y)
TOP1(free(x), y) → NEW(y)
TOP1(free(x), y) → CHECK(x)
TOP1(free(x), y) → NEW(x)
TOP1(free(x), y) → CHECK(new(y))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(x, free(y)) → NEW(y)
CHECK(new(x)) → CHECK(x)
TOP2(x, free(y)) → CHECK(x)
CHECK(old(x)) → CHECK(x)
TOP2(x, free(y)) → CHECK(new(y))
CHECK(new(x)) → NEW(check(x))
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(x, free(y)) → TOP1(new(x), check(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))
NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

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

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ UsableRulesProof
                  ↳ QDP
                  ↳ QDP

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

NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

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

NEW(free(x)) → NEW(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                  ↳ QDP

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

CHECK(old(x)) → CHECK(x)
CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)

The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                  ↳ QDP

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

CHECK(old(x)) → CHECK(x)
CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof

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

TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(x, free(y)) → TOP1(check(new(x)), y)
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP2(x, free(y)) → TOP1(new(x), check(y))

The TRS R consists of the following rules:

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing

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

TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(x, free(y)) → TOP1(check(new(x)), y)
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(x, free(y)) → TOP1(new(x), check(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP1(free(x), y) → TOP2(x, check(new(y)))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP2(x, free(y)) → TOP1(check(new(x)), y) at position [0] we obtained the following new rules:

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing

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

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP2(x, free(y)) → TOP1(new(x), check(y))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP1(free(x), y) → TOP2(x, check(new(y))) at position [1] we obtained the following new rules:

TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing

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

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
TOP2(x, free(y)) → TOP1(check(x), new(y))
TOP2(x, free(y)) → TOP1(new(x), check(y))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP1(free(x), y) → TOP2(check(x), new(y)) at position [1] we obtained the following new rules:

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing

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

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
TOP2(x, free(y)) → TOP1(new(x), check(y))
TOP2(x, free(y)) → TOP1(check(x), new(y))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP2(x, free(y)) → TOP1(check(x), new(y)) at position [0] we obtained the following new rules:

TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(old(x0), free(y1)) → TOP1(old(x0), new(y1))
TOP2(old(x0), free(y1)) → TOP1(old(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof

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

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(old(x0), free(y1)) → TOP1(old(check(x0)), new(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(old(x0), free(y1)) → TOP1(old(x0), new(y1))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
TOP2(x, free(y)) → TOP1(new(x), check(y))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

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
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing

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

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
TOP2(x, free(y)) → TOP1(new(x), check(y))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP2(x, free(y)) → TOP1(new(x), check(y)) at position [0] we obtained the following new rules:

TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing

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

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP1(free(x), y) → TOP2(new(x), check(y)) at position [1] we obtained the following new rules:

TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP1(free(y0), old(x0)) → TOP2(new(y0), old(check(x0)))
TOP1(free(y0), old(x0)) → TOP2(new(y0), old(x0))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof

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

TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), old(x0)) → TOP2(new(y0), old(x0))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP1(free(y0), old(x0)) → TOP2(new(y0), old(check(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

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
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof

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

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
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.


TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
The remaining pairs can at least be oriented weakly.

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
Used ordering: Polynomial interpretation [25]:

POL(TOP1(x1, x2)) = x1   
POL(TOP2(x1, x2)) = x1   
POL(check(x1)) = 0   
POL(free(x1)) = x1   
POL(new(x1)) = x1   
POL(old(x1)) = 0   
POL(serve) = 1   

The following usable rules [17] were oriented:

new(free(x)) → free(new(x))
check(old(x)) → old(x)
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(old(x)) → old(check(x))
check(new(x)) → new(check(x))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof

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

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

Q is empty.
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.


TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
The remaining pairs can at least be oriented weakly.

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
Used ordering: Polynomial interpretation [25]:

POL(TOP1(x1, x2)) = x2   
POL(TOP2(x1, x2)) = x2   
POL(check(x1)) = 0   
POL(free(x1)) = x1   
POL(new(x1)) = x1   
POL(old(x1)) = 0   
POL(serve) = 1   

The following usable rules [17] were oriented:

new(free(x)) → free(new(x))
check(old(x)) → old(x)
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(old(x)) → old(check(x))
check(new(x)) → new(check(x))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof

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

TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

The TRS R consists of the following rules:

check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
new(free(x)) → free(new(x))
new(serve) → free(serve)

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.TOP2: 0
check: 0
new: x0
serve: 1
TOP1: 0
old: 0
free: x0
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.0-1(check.1(free.1(new.1(x0))), y1)
TOP2.0-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), y1)
TOP1.1-0(free.1(x), y) → TOP2.0-0(check.1(new.1(x)), y)
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-0(new.0(y0), free.0(check.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(check.0(free.0(new.0(x0))), y1)
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.0-1(check.1(y0), free.1(new.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(check.0(x0)), new.0(y1))
TOP1.0-0(free.0(x), y) → TOP2.0-0(check.0(new.0(x)), y)
TOP2.1-1(x, free.1(y)) → TOP1.1-0(x, check.1(new.1(y)))
TOP2.0-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), y1)
TOP1.1-0(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.0(x0)))
TOP2.0-1(new.0(x0), free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), new.1(y1))
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.1-0(new.1(y0), free.0(check.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(new.0(x0)), check.0(y1))
TOP1.1-1(free.1(x), y) → TOP2.0-1(check.1(new.1(x)), y)
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-0(free.0(new.0(x0)), check.1(y1))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(free.0(check.0(x0)), new.1(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(y0, check.0(free.0(new.0(x0))))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.0-0(check.1(y0), free.0(new.0(x0)))
TOP1.0-1(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.1(x0)))
TOP2.0-1(x, free.1(y)) → TOP1.0-0(x, check.1(new.1(y)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(check.0(y0), free.0(new.0(x0)))
TOP1.0-1(free.0(y0), new.1(x0)) → TOP2.0-0(new.0(y0), new.0(check.1(x0)))
TOP2.1-0(serve., free.0(y1)) → TOP1.1-0(free.1(serve.), check.0(y1))
TOP1.1-1(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.1(x0)))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(check.0(free.0(new.0(x0))), y1)
TOP2.1-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.1(x0)), y1)
TOP1.1-1(free.1(y0), serve.) → TOP2.0-1(check.1(y0), free.1(serve.))
TOP1.0-1(free.0(x), y) → TOP2.0-1(check.0(new.0(x)), y)
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(new.0(y0), free.0(check.0(x0)))
TOP2.0-0(new.0(x0), free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), new.0(y1))
TOP2.1-0(new.1(x0), free.0(y1)) → TOP1.0-0(new.0(check.1(x0)), new.0(y1))
TOP1.0-0(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.0(x0)))
TOP2.1-1(new.1(x0), free.1(y1)) → TOP1.0-1(new.0(check.1(x0)), new.1(y1))
TOP2.1-0(x, free.0(y)) → TOP1.1-0(x, check.0(new.0(y)))
TOP1.0-1(free.0(y0), serve.) → TOP2.0-1(check.0(y0), free.1(serve.))
TOP2.1-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.1(x0)), y1)
TOP2.0-0(x, free.0(y)) → TOP1.0-0(x, check.0(new.0(y)))
TOP1.0-0(free.0(y0), new.0(x0)) → TOP2.0-0(new.0(y0), new.0(check.0(x0)))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-0(y0, check.1(free.1(new.1(x0))))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.0-0(free.0(check.1(x0)), new.0(y1))
TOP1.1-0(free.1(y0), new.0(x0)) → TOP2.1-0(new.1(y0), new.0(check.0(x0)))
TOP2.1-1(serve., free.1(y1)) → TOP1.1-0(free.1(serve.), check.1(y1))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(y0, check.0(free.0(new.0(x0))))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.1-0(free.1(new.1(x0)), check.0(y1))
TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.0-1(free.0(check.1(x0)), new.1(y1))
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.1-0(y0, check.1(free.1(new.1(x0))))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(check.0(y0), free.1(new.1(x0)))
TOP1.1-1(free.1(y0), new.1(x0)) → TOP2.1-0(new.1(y0), new.0(check.1(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(new.1(y0), free.0(check.0(x0)))
TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.1-0(free.1(new.1(x0)), check.1(y1))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.0-0(check.1(free.1(new.1(x0))), y1)

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
check.0(old.1(x)) → old.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(x))

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

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof

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

TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.0-1(check.1(free.1(new.1(x0))), y1)
TOP2.0-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), y1)
TOP1.1-0(free.1(x), y) → TOP2.0-0(check.1(new.1(x)), y)
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-0(new.0(y0), free.0(check.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(check.0(free.0(new.0(x0))), y1)
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.0-1(check.1(y0), free.1(new.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(check.0(x0)), new.0(y1))
TOP1.0-0(free.0(x), y) → TOP2.0-0(check.0(new.0(x)), y)
TOP2.1-1(x, free.1(y)) → TOP1.1-0(x, check.1(new.1(y)))
TOP2.0-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), y1)
TOP1.1-0(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.0(x0)))
TOP2.0-1(new.0(x0), free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), new.1(y1))
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.1-0(new.1(y0), free.0(check.1(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(new.0(x0)), check.0(y1))
TOP1.1-1(free.1(x), y) → TOP2.0-1(check.1(new.1(x)), y)
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-0(free.0(new.0(x0)), check.1(y1))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(free.0(check.0(x0)), new.1(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(y0, check.0(free.0(new.0(x0))))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.0-0(check.1(y0), free.0(new.0(x0)))
TOP1.0-1(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.1(x0)))
TOP2.0-1(x, free.1(y)) → TOP1.0-0(x, check.1(new.1(y)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(check.0(y0), free.0(new.0(x0)))
TOP1.0-1(free.0(y0), new.1(x0)) → TOP2.0-0(new.0(y0), new.0(check.1(x0)))
TOP2.1-0(serve., free.0(y1)) → TOP1.1-0(free.1(serve.), check.0(y1))
TOP1.1-1(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.1(x0)))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(check.0(free.0(new.0(x0))), y1)
TOP2.1-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.1(x0)), y1)
TOP1.1-1(free.1(y0), serve.) → TOP2.0-1(check.1(y0), free.1(serve.))
TOP1.0-1(free.0(x), y) → TOP2.0-1(check.0(new.0(x)), y)
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(new.0(y0), free.0(check.0(x0)))
TOP2.0-0(new.0(x0), free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), new.0(y1))
TOP2.1-0(new.1(x0), free.0(y1)) → TOP1.0-0(new.0(check.1(x0)), new.0(y1))
TOP1.0-0(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.0(x0)))
TOP2.1-1(new.1(x0), free.1(y1)) → TOP1.0-1(new.0(check.1(x0)), new.1(y1))
TOP2.1-0(x, free.0(y)) → TOP1.1-0(x, check.0(new.0(y)))
TOP1.0-1(free.0(y0), serve.) → TOP2.0-1(check.0(y0), free.1(serve.))
TOP2.1-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.1(x0)), y1)
TOP2.0-0(x, free.0(y)) → TOP1.0-0(x, check.0(new.0(y)))
TOP1.0-0(free.0(y0), new.0(x0)) → TOP2.0-0(new.0(y0), new.0(check.0(x0)))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-0(y0, check.1(free.1(new.1(x0))))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.0-0(free.0(check.1(x0)), new.0(y1))
TOP1.1-0(free.1(y0), new.0(x0)) → TOP2.1-0(new.1(y0), new.0(check.0(x0)))
TOP2.1-1(serve., free.1(y1)) → TOP1.1-0(free.1(serve.), check.1(y1))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(y0, check.0(free.0(new.0(x0))))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.1-0(free.1(new.1(x0)), check.0(y1))
TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.0-1(free.0(check.1(x0)), new.1(y1))
TOP1.1-1(free.1(y0), free.1(x0)) → TOP2.1-0(y0, check.1(free.1(new.1(x0))))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(check.0(y0), free.1(new.1(x0)))
TOP1.1-1(free.1(y0), new.1(x0)) → TOP2.1-0(new.1(y0), new.0(check.1(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(new.1(y0), free.0(check.0(x0)))
TOP2.1-1(free.1(x0), free.1(y1)) → TOP1.1-0(free.1(new.1(x0)), check.1(y1))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.0-0(check.1(free.1(new.1(x0))), y1)

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
check.0(old.1(x)) → old.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(x))

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

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                          ↳ UsableRulesReductionPairsProof
                                                                        ↳ QDP
                                                                        ↳ QDP

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

TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(check.0(free.0(new.0(x0))), y1)
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(check.0(y0), free.0(new.0(x0)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(new.0(y0), free.0(check.0(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(check.0(x0)), new.0(y1))
TOP1.0-0(free.0(x), y) → TOP2.0-0(check.0(new.0(x)), y)
TOP2.0-0(new.0(x0), free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), new.0(y1))
TOP2.0-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), y1)
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(new.0(x0)), check.0(y1))
TOP1.0-0(free.0(y0), new.0(x0)) → TOP2.0-0(new.0(y0), new.0(check.0(x0)))
TOP2.0-0(x, free.0(y)) → TOP1.0-0(x, check.0(new.0(y)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(y0, check.0(free.0(new.0(x0))))
TOP1.0-0(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.0(x0)))

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
check.0(old.1(x)) → old.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(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.

No dependency pairs are removed.

The following rules are removed from R:

check.1(new.1(x)) → new.0(check.1(x))
check.1(free.1(x)) → free.0(check.1(x))
Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.0-0(x1, x2)) = x1 + x2   
POL(TOP2.0-0(x1, x2)) = x1 + x2   
POL(check.0(x1)) = x1   
POL(check.1(x1)) = 1 + x1   
POL(free.0(x1)) = x1   
POL(free.1(x1)) = 1 + x1   
POL(new.0(x1)) = x1   
POL(new.1(x1)) = 1 + x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = 1 + x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                          ↳ UsableRulesReductionPairsProof
                                                                            ↳ QDP
                                                                              ↳ RuleRemovalProof
                                                                        ↳ QDP
                                                                        ↳ QDP

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

TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(check.0(free.0(new.0(x0))), y1)
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(check.0(y0), free.0(new.0(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(check.0(x0)), new.0(y1))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(new.0(y0), free.0(check.0(x0)))
TOP1.0-0(free.0(x), y) → TOP2.0-0(check.0(new.0(x)), y)
TOP2.0-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), y1)
TOP2.0-0(new.0(x0), free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), new.0(y1))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(new.0(x0)), check.0(y1))
TOP2.0-0(x, free.0(y)) → TOP1.0-0(x, check.0(new.0(y)))
TOP1.0-0(free.0(y0), new.0(x0)) → TOP2.0-0(new.0(y0), new.0(check.0(x0)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(y0, check.0(free.0(new.0(x0))))
TOP1.0-0(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.0(x0)))

The TRS R consists of the following rules:

check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.0(old.1(x)) → old.0(check.1(x))
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(check.0(free.0(new.0(x0))), y1)
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(check.0(y0), free.0(new.0(x0)))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(check.0(x0)), new.0(y1))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(new.0(y0), free.0(check.0(x0)))
TOP1.0-0(free.0(x), y) → TOP2.0-0(check.0(new.0(x)), y)
TOP2.0-0(x0, free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), y1)
TOP2.0-0(new.0(x0), free.0(y1)) → TOP1.0-0(new.0(check.0(x0)), new.0(y1))
TOP2.0-0(free.0(x0), free.0(y1)) → TOP1.0-0(free.0(new.0(x0)), check.0(y1))
TOP2.0-0(x, free.0(y)) → TOP1.0-0(x, check.0(new.0(y)))
TOP1.0-0(free.0(y0), new.0(x0)) → TOP2.0-0(new.0(y0), new.0(check.0(x0)))
TOP1.0-0(free.0(y0), free.0(x0)) → TOP2.0-0(y0, check.0(free.0(new.0(x0))))
TOP1.0-0(free.0(y0), x0) → TOP2.0-0(y0, new.0(check.0(x0)))

Strictly oriented rules of the TRS R:

check.0(old.1(x)) → old.0(check.1(x))

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.0-0(x1, x2)) = 1 + x1 + x2   
POL(TOP2.0-0(x1, x2)) = 1 + x1 + x2   
POL(check.0(x1)) = x1   
POL(check.1(x1)) = x1   
POL(free.0(x1)) = 1 + x1   
POL(new.0(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = 1 + x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                          ↳ UsableRulesReductionPairsProof
                                                                            ↳ QDP
                                                                              ↳ RuleRemovalProof
                                                                                ↳ QDP
                                                                                  ↳ PisEmptyProof
                                                                        ↳ QDP
                                                                        ↳ QDP

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

check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
new.0(free.0(x)) → free.0(new.0(x))

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.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof
                                                                        ↳ QDP

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

TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.1-0(free.1(new.1(x0)), check.0(y1))
TOP2.1-0(x, free.0(y)) → TOP1.1-0(x, check.0(new.0(y)))
TOP1.1-0(free.1(y0), new.0(x0)) → TOP2.1-0(new.1(y0), new.0(check.0(x0)))
TOP2.1-0(serve., free.0(y1)) → TOP1.1-0(free.1(serve.), check.0(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(y0, check.0(free.0(new.0(x0))))
TOP1.1-0(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.0(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(new.1(y0), free.0(check.0(x0)))

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
check.0(old.1(x)) → old.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

check.0(old.1(x)) → old.0(check.1(x))

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.1-0(x1, x2)) = x1 + x2   
POL(TOP2.1-0(x1, x2)) = x1 + x2   
POL(check.0(x1)) = x1   
POL(check.1(x1)) = x1   
POL(free.0(x1)) = x1   
POL(free.1(x1)) = x1   
POL(new.0(x1)) = x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = 1 + x1   
POL(serve.) = 0   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesReductionPairsProof
                                                                        ↳ QDP

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

TOP2.1-0(x, free.0(y)) → TOP1.1-0(x, check.0(new.0(y)))
TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.1-0(free.1(new.1(x0)), check.0(y1))
TOP1.1-0(free.1(y0), new.0(x0)) → TOP2.1-0(new.1(y0), new.0(check.0(x0)))
TOP2.1-0(serve., free.0(y1)) → TOP1.1-0(free.1(serve.), check.0(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(y0, check.0(free.0(new.0(x0))))
TOP1.1-0(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.0(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(new.1(y0), free.0(check.0(x0)))

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(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:

TOP1.1-0(free.1(y0), new.0(x0)) → TOP2.1-0(new.1(y0), new.0(check.0(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(y0, check.0(free.0(new.0(x0))))
TOP1.1-0(free.1(y0), x0) → TOP2.1-0(y0, new.0(check.0(x0)))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(new.1(y0), free.0(check.0(x0)))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.1-0(x1, x2)) = 1 + x1 + x2   
POL(TOP2.1-0(x1, x2)) = x1 + x2   
POL(check.0(x1)) = x1   
POL(free.0(x1)) = 1 + x1   
POL(free.1(x1)) = x1   
POL(new.0(x1)) = x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesReductionPairsProof
                                                                                ↳ QDP
                                                                                  ↳ DependencyGraphProof
                                                                        ↳ QDP

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

TOP2.1-0(free.1(x0), free.0(y1)) → TOP1.1-0(free.1(new.1(x0)), check.0(y1))
TOP2.1-0(x, free.0(y)) → TOP1.1-0(x, check.0(new.0(y)))
TOP2.1-0(serve., free.0(y1)) → TOP1.1-0(free.1(serve.), check.0(y1))

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
new.1(serve.) → free.1(serve.)
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
new.0(free.0(x)) → free.0(new.0(x))

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

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof

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

TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(free.0(check.0(x0)), new.1(y1))
TOP1.0-1(free.0(x), y) → TOP2.0-1(check.0(new.0(x)), y)
TOP1.0-1(free.0(y0), serve.) → TOP2.0-1(check.0(y0), free.1(serve.))
TOP2.0-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), y1)
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(check.0(y0), free.1(new.1(x0)))
TOP2.0-1(new.0(x0), free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), new.1(y1))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(check.0(free.0(new.0(x0))), y1)

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
check.0(old.1(x)) → old.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

check.0(old.1(x)) → old.0(check.1(x))

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.0-1(x1, x2)) = x1 + x2   
POL(TOP2.0-1(x1, x2)) = x1 + x2   
POL(check.0(x1)) = x1   
POL(check.1(x1)) = x1   
POL(free.0(x1)) = x1   
POL(free.1(x1)) = x1   
POL(new.0(x1)) = x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = 1 + x1   
POL(serve.) = 0   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesReductionPairsProof

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

TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(free.0(check.0(x0)), new.1(y1))
TOP1.0-1(free.0(x), y) → TOP2.0-1(check.0(new.0(x)), y)
TOP1.0-1(free.0(y0), serve.) → TOP2.0-1(check.0(y0), free.1(serve.))
TOP2.0-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), y1)
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(check.0(y0), free.1(new.1(x0)))
TOP2.0-1(new.0(x0), free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), new.1(y1))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(check.0(free.0(new.0(x0))), y1)

The TRS R consists of the following rules:

new.1(free.1(x)) → free.1(new.1(x))
check.1(new.1(x)) → new.0(check.1(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
check.1(free.1(x)) → free.0(check.1(x))
new.1(serve.) → free.1(serve.)
new.0(free.0(x)) → free.0(new.0(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:

TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(free.0(check.0(x0)), new.1(y1))
TOP2.0-1(x0, free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), y1)
TOP2.0-1(new.0(x0), free.1(y1)) → TOP1.0-1(new.0(check.0(x0)), new.1(y1))
TOP2.0-1(free.0(x0), free.1(y1)) → TOP1.0-1(check.0(free.0(new.0(x0))), y1)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP1.0-1(x1, x2)) = x1 + x2   
POL(TOP2.0-1(x1, x2)) = 1 + x1 + x2   
POL(check.0(x1)) = x1   
POL(free.0(x1)) = 1 + x1   
POL(free.1(x1)) = x1   
POL(new.0(x1)) = x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ DependencyPairsProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ UsableRulesProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ Narrowing
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ DependencyGraphProof
                                                      ↳ QDP
                                                        ↳ QDPOrderProof
                                                          ↳ QDP
                                                            ↳ QDPOrderProof
                                                              ↳ QDP
                                                                ↳ SemLabProof
                                                                  ↳ QDP
                                                                    ↳ DependencyGraphProof
                                                                      ↳ AND
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                        ↳ QDP
                                                                          ↳ RuleRemovalProof
                                                                            ↳ QDP
                                                                              ↳ UsableRulesReductionPairsProof
                                                                                ↳ QDP
                                                                                  ↳ DependencyGraphProof

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

TOP1.0-1(free.0(x), y) → TOP2.0-1(check.0(new.0(x)), y)
TOP1.0-1(free.0(y0), serve.) → TOP2.0-1(check.0(y0), free.1(serve.))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(check.0(y0), free.1(new.1(x0)))

The TRS R consists of the following rules:

new.0(free.0(x)) → free.0(new.0(x))
check.0(old.0(x)) → old.0(x)
check.0(old.0(x)) → old.0(check.0(x))
check.0(new.0(x)) → new.0(check.0(x))
check.0(free.0(x)) → free.0(check.0(x))
check.0(old.1(x)) → old.1(x)
new.1(free.1(x)) → free.1(new.1(x))
new.1(serve.) → free.1(serve.)

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