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

0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 QTRSRRRProof (⇔)
↳4 QTRS
↳5 DependencyPairsProof (⇔)
↳6 QDP
↳7 DependencyGraphProof (⇔)
↳8 AND
  ↳9 QDP
    ↳10 UsableRulesProof (⇔)
    ↳11 QDP
    ↳12 QDPSizeChangeProof (⇔)
    ↳13 TRUE
  ↳14 QDP
    ↳15 UsableRulesProof (⇔)
    ↳16 QDP
    ↳17 QDPSizeChangeProof (⇔)
    ↳18 TRUE
  ↳19 QDP
    ↳20 UsableRulesProof (⇔)
    ↳21 QDP
    ↳22 Narrowing (⇔)
    ↳23 QDP
    ↳24 Narrowing (⇔)
    ↳25 QDP
    ↳26 Narrowing (⇔)
    ↳27 QDP
    ↳28 DependencyGraphProof (⇔)
    ↳29 QDP
    ↳30 Narrowing (⇔)
    ↳31 QDP
    ↳32 DependencyGraphProof (⇔)
    ↳33 QDP
    ↳34 Narrowing (⇔)
    ↳35 QDP
    ↳36 Narrowing (⇔)
    ↳37 QDP
    ↳38 QDPOrderProof (⇔)
    ↳39 QDP
    ↳40 QDPOrderProof (⇔)
    ↳41 QDP
    ↳42 SemLabProof (⇐)
    ↳43 QDP
    ↳44 DependencyGraphProof (⇔)
    ↳45 AND
      ↳46 QDP
        ↳47 UsableRulesReductionPairsProof (⇔)
        ↳48 QDP
        ↳49 MRRProof (⇔)
        ↳50 QDP
        ↳51 MRRProof (⇔)
        ↳52 QDP
        ↳53 PisEmptyProof (⇔)
        ↳54 TRUE
      ↳55 QDP
        ↳56 MRRProof (⇔)
        ↳57 QDP
        ↳58 DependencyGraphProof (⇔)
        ↳59 QDP
        ↳60 MRRProof (⇔)
        ↳61 QDP
        ↳62 UsableRulesReductionPairsProof (⇔)
        ↳63 QDP
        ↳64 DependencyGraphProof (⇔)
        ↳65 TRUE
      ↳66 QDP
        ↳67 MRRProof (⇔)
        ↳68 QDP
        ↳69 DependencyGraphProof (⇔)
        ↳70 QDP
        ↳71 MRRProof (⇔)
        ↳72 QDP
        ↳73 UsableRulesReductionPairsProof (⇔)
        ↳74 QDP
        ↳75 DependencyGraphProof (⇔)
        ↳76 TRUE

(0) Obligation:

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.

(1) 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(top1(x1, x2)) = x1 + x2   
POL(top2(x1, x2)) = x1 + x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

old(serve) → free(serve)


(2) Obligation:

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.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

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   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

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


(4) Obligation:

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.

(5) DependencyPairsProof (EQUIVALENT transformation)

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

(6) Obligation:

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

TOP1(free(x), y) → TOP2(check(new(x)), y)
TOP1(free(x), y) → CHECK(new(x))
TOP1(free(x), y) → NEW(x)
TOP1(free(x), y) → TOP2(new(x), check(y))
TOP1(free(x), y) → CHECK(y)
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP1(free(x), y) → CHECK(x)
TOP1(free(x), y) → NEW(y)
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP1(free(x), y) → CHECK(new(y))
TOP2(x, free(y)) → TOP1(check(new(x)), y)
TOP2(x, free(y)) → CHECK(new(x))
TOP2(x, free(y)) → NEW(x)
TOP2(x, free(y)) → TOP1(new(x), check(y))
TOP2(x, free(y)) → CHECK(y)
TOP2(x, free(y)) → TOP1(check(x), new(y))
TOP2(x, free(y)) → CHECK(x)
TOP2(x, free(y)) → NEW(y)
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP2(x, free(y)) → CHECK(new(y))
NEW(free(x)) → NEW(x)
CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → NEW(check(x))
CHECK(new(x)) → CHECK(x)
CHECK(old(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.

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) 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:

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.

(10) 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.

(11) 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.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • NEW(free(x)) → NEW(x)
    The graph contains the following edges 1 > 1

(13) TRUE

(14) 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:

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.

(15) 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.

(16) 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.

(17) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • CHECK(new(x)) → CHECK(x)
    The graph contains the following edges 1 > 1

  • CHECK(free(x)) → CHECK(x)
    The graph contains the following edges 1 > 1

  • CHECK(old(x)) → CHECK(x)
    The graph contains the following edges 1 > 1

(18) TRUE

(19) Obligation:

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

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))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(x, check(new(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.

(20) 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.

(21) Obligation:

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

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))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(x, check(new(y)))

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.

(22) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP2(x, free(y)) → TOP1(check(new(x)), y) at position [0] we obtained the following new rules [LPAR04]:

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

(23) Obligation:

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

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))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)

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.

(24) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP2(x, free(y)) → TOP1(new(x), check(y)) at position [0] we obtained the following new rules [LPAR04]:

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

(25) Obligation:

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

TOP1(free(x), y) → TOP2(check(new(x)), 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))
TOP2(x, free(y)) → TOP1(x, check(new(y)))
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))

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.

(26) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP1(free(x), y) → TOP2(new(x), check(y)) at position [1] we obtained the following new rules [LPAR04]:

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

(27) Obligation:

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

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

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.

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(29) Obligation:

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

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

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.

(30) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP2(x, free(y)) → TOP1(check(x), new(y)) at position [0] we obtained the following new rules [LPAR04]:

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

(31) Obligation:

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

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

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.

(32) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(33) Obligation:

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(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP1(free(x), y) → TOP2(check(x), new(y))
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))

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.

(34) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP1(free(x), y) → TOP2(check(x), new(y)) at position [1] we obtained the following new rules [LPAR04]:

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

(35) Obligation:

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(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(x), y) → TOP2(x, check(new(y)))
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))

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.

(36) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TOP1(free(x), y) → TOP2(x, check(new(y))) at position [1] we obtained the following new rules [LPAR04]:

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

(37) Obligation:

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(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))

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.

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


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.
Used ordering: Matrix interpretation [MATRO]:

POL(TOP2(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(free(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(TOP1(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(check(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(new(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(serve) =
/0\
\1/

POL(old(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

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

(39) Obligation:

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(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

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.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


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.
Used ordering: Matrix interpretation [MATRO]:

POL(TOP2(x1, x2)) =
/0\
\0/
 +
/01\
\00/
·x1 +
/00\
\00/
·x2

POL(free(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(TOP1(x1, x2)) =
/0\
\0/
 +
/01\
\00/
·x1 +
/00\
\00/
·x2

POL(check(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

POL(new(x1)) =
/0\
\0/
 +
/01\
\01/
·x1

POL(serve) =
/0\
\1/

POL(old(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

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

(41) Obligation:

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(x0, free(y1)) → TOP1(new(check(x0)), y1)
TOP2(free(x0), free(y1)) → TOP1(check(free(new(x0))), y1)
TOP1(free(y0), free(x0)) → TOP2(new(y0), free(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(new(x0)), check(y1))
TOP1(free(y0), new(x0)) → TOP2(new(y0), new(check(x0)))
TOP2(free(x0), free(y1)) → TOP1(free(check(x0)), new(y1))
TOP2(new(x0), free(y1)) → TOP1(new(check(x0)), new(y1))
TOP2(serve, free(y1)) → TOP1(free(serve), check(y1))
TOP1(free(y0), free(x0)) → TOP2(check(y0), free(new(x0)))
TOP1(free(y0), serve) → TOP2(check(y0), free(serve))
TOP1(free(y0), x0) → TOP2(y0, new(check(x0)))
TOP1(free(y0), free(x0)) → TOP2(y0, check(free(new(x0))))

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.

(42) SemLabProof (SOUND transformation)

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: 1
new: x0
serve: 0
TOP1: 0
old: 1
free: x0
By semantic labelling [SEMLAB] we obtain the following labelled TRS.

(43) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) Complex Obligation (AND)

(46) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(47) 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.

No dependency pairs are removed.

The following rules are removed from R:

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

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

(48) Obligation:

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

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

The TRS R consists of the following rules:

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

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

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

Used ordering: Polynomial interpretation [POLO]:

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

(50) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(51) 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 dependency pairs:

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


Used ordering: Polynomial interpretation [POLO]:

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

(52) Obligation:

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

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

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

(53) PisEmptyProof (EQUIVALENT transformation)

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

(54) TRUE

(55) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(56) 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 dependency pairs:

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

Strictly oriented rules of the TRS R:

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

Used ordering: Polynomial interpretation [POLO]:

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)) = 1 + x1   
POL(free.1(x1)) = 1 + x1   
POL(new.0(x1)) = 1 + x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   

(57) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(58) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(59) Obligation:

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(check.1(x0)), new.0(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(check.1(y0), free.0(new.0(x0)))
TOP2.1-0(new.1(x0), free.0(y1)) → TOP1.1-0(new.1(check.1(x0)), new.0(y1))

The TRS R consists of the following rules:

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

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

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

Used ordering: Polynomial interpretation [POLO]:

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)) = 1 + x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   

(61) Obligation:

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(check.1(x0)), new.0(y1))
TOP1.1-0(free.1(y0), free.0(x0)) → TOP2.1-0(check.1(y0), free.0(new.0(x0)))
TOP2.1-0(new.1(x0), free.0(y1)) → TOP1.1-0(new.1(check.1(x0)), new.0(y1))

The TRS R consists of the following rules:

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

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

(62) 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:

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

Used ordering: POLO with Polynomial interpretation [POLO]:

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

(63) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(64) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(65) TRUE

(66) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(67) 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 dependency pairs:

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

Strictly oriented rules of the TRS R:

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

Used ordering: Polynomial interpretation [POLO]:

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)) = 1 + x1   
POL(free.1(x1)) = 1 + x1   
POL(new.0(x1)) = 1 + x1   
POL(new.1(x1)) = x1   
POL(old.0(x1)) = x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   

(68) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(69) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(70) Obligation:

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(new.0(x0)), check.1(y1))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(new.0(y0), free.1(check.1(x0)))
TOP1.0-1(free.0(y0), new.1(x0)) → TOP2.0-1(new.0(y0), new.1(check.1(x0)))

The TRS R consists of the following rules:

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

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

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

Used ordering: Polynomial interpretation [POLO]:

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)) = 1 + x1   
POL(old.1(x1)) = x1   
POL(serve.) = 0   

(72) Obligation:

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(new.0(x0)), check.1(y1))
TOP1.0-1(free.0(y0), free.1(x0)) → TOP2.0-1(new.0(y0), free.1(check.1(x0)))
TOP1.0-1(free.0(y0), new.1(x0)) → TOP2.0-1(new.0(y0), new.1(check.1(x0)))

The TRS R consists of the following rules:

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

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

(73) 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:

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

Used ordering: POLO with Polynomial interpretation [POLO]:

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

(74) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(75) DependencyGraphProof (EQUIVALENT transformation)

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

(76) TRUE