Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
  ↳1 QTRS Reverse (⇔)
    ↳2 QTRS
  ↳3 QTRS Reverse (⇔)
    ↳4 QTRS
  ↳5 QTRSRRRProof (⇔)
    ↳6 QTRS
    ↳7 DependencyPairsProof (⇔)
    ↳8 QDP
    ↳9 DependencyGraphProof (⇔)
    ↳10 AND
      ↳11 QDP
        ↳12 UsableRulesProof (⇔)
          ↳13 QDP
          ↳14 UsableRulesReductionPairsProof (⇔)
          ↳15 QDP
          ↳16 PisEmptyProof (⇔)
          ↳17 TRUE
        ↳18 UsableRulesProof (⇔)
          ↳19 QDP
      ↳20 QDP
        ↳21 UsableRulesProof (⇔)
          ↳22 QDP
          ↳23 UsableRulesReductionPairsProof (⇔)
          ↳24 QDP
          ↳25 PisEmptyProof (⇔)
          ↳26 TRUE
        ↳27 UsableRulesProof (⇔)
          ↳28 QDP
      ↳29 QDP
        ↳30 UsableRulesProof (⇔)
          ↳31 QDP
          ↳32 UsableRulesReductionPairsProof (⇔)
          ↳33 QDP
          ↳34 PisEmptyProof (⇔)
          ↳35 TRUE
        ↳36 UsableRulesProof (⇔)
          ↳37 QDP
      ↳38 QDP
        ↳39 UsableRulesProof (⇔)
          ↳40 QDP
          ↳41 MRRProof (⇔)
          ↳42 QDP
          ↳43 MRRProof (⇔)
          ↳44 QDP
          ↳45 QDPOrderProof (⇔)
          ↳46 QDP
          ↳47 PisEmptyProof (⇔)
          ↳48 TRUE
        ↳49 UsableRulesProof (⇔)
          ↳50 QDP

(0) Obligation:

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

top(free(x)) → top(check(new(x)))
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.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

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

Q is empty.

(3) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(4) Obligation:

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

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

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(check(x1)) = x1   
POL(free(x1)) = x1   
POL(new(x1)) = x1   
POL(old(x1)) = 1 + x1   
POL(serve) = 0   
POL(top(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

old(serve) → free(serve)


(6) Obligation:

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

top(free(x)) → top(check(new(x)))
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.

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))
TOP(free(x)) → CHECK(new(x))
TOP(free(x)) → NEW(x)
NEW(free(x)) → NEW(x)
OLD(free(x)) → OLD(x)
CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → NEW(check(x))
CHECK(new(x)) → CHECK(x)
CHECK(old(x)) → OLD(check(x))
CHECK(old(x)) → CHECK(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
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.
We have to consider all minimal (P,Q,R)-chains.

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 4 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

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

OLD(free(x)) → OLD(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
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.
We have to consider all minimal (P,Q,R)-chains.

(12) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

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

OLD(free(x)) → OLD(x)

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

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] 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:

OLD(free(x)) → OLD(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(OLD(x1)) = 2·x1   
POL(free(x1)) = 2·x1   

(15) Obligation:

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

(16) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(17) TRUE

(18) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(19) Obligation:

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

OLD(free(x)) → OLD(x)

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

(20) Obligation:

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

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

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
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.
We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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.

(23) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] 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:

NEW(free(x)) → NEW(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(NEW(x1)) = 2·x1   
POL(free(x1)) = 2·x1   

(24) Obligation:

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

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(26) TRUE

(27) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(28) Obligation:

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.

(29) Obligation:

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

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

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
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.
We have to consider all minimal (P,Q,R)-chains.

(30) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(31) Obligation:

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

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

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

(32) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] 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:

CHECK(new(x)) → CHECK(x)
CHECK(free(x)) → CHECK(x)
CHECK(old(x)) → CHECK(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(CHECK(x1)) = 2·x1   
POL(free(x1)) = 2·x1   
POL(new(x1)) = 2·x1   
POL(old(x1)) = 2·x1   

(33) Obligation:

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

(34) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(35) TRUE

(36) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(37) Obligation:

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

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

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

(38) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
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.
We have to consider all minimal (P,Q,R)-chains.

(39) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(40) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

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)
old(free(x)) → free(old(x))

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

(41) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, 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:

old(free(x)) → free(old(x))

Used ordering: Polynomial interpretation [POLO]:

POL(TOP(x1)) = x1   
POL(check(x1)) = x1   
POL(free(x1)) = 1 + x1   
POL(new(x1)) = 1 + x1   
POL(old(x1)) = 2 + 2·x1   
POL(serve) = 0   

(42) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

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.

(43) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, 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(old(x)) → old(check(x))
check(old(x)) → old(x)

Used ordering: Polynomial interpretation [POLO]:

POL(TOP(x1)) = 2·x1   
POL(check(x1)) = 2·x1   
POL(free(x1)) = 2·x1   
POL(new(x1)) = x1   
POL(old(x1)) = 2 + 2·x1   
POL(serve) = 0   

(44) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

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

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TOP(free(x)) → TOP(check(new(x)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(TOP(x1)) =
/0A\
\0A/
 +
/0A0A\
\0A1A/
·x1

POL(free(x1)) =
/1A\
\-I/
 +
/1A0A\
\-I1A/
·x1

POL(check(x1)) =
/0A\
\-I/
 +
/0A-I\
\-I-I/
·x1

POL(new(x1)) =
/0A\
\-I/
 +
/0A0A\
\-I1A/
·x1

POL(serve) =
/0A\
\1A/

The following usable rules [FROCOS05] were oriented:

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

(46) Obligation:

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

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

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

(47) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(48) TRUE

(49) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(50) Obligation:

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

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

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)
old(free(x)) → free(old(x))

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