YES Termination w.r.t. Q proof of AProVE_04_Liveness6.4.ari

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

0 QTRS
↳1 QTRSRRRProof (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 1 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 4 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 TransformationProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 TransformationProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 TransformationProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 DependencyGraphProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 TransformationProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 DependencyGraphProof (⇔, 0 ms)
        ↳33 QDP
        ↳34 TransformationProof (⇔, 0 ms)
        ↳35 QDP
        ↳36 TransformationProof (⇔, 0 ms)
        ↳37 QDP
        ↳38 QDPOrderProof (⇔, 50 ms)
        ↳39 QDP
        ↳40 SemLabProof (⇒, 1337 ms)
        ↳41 QDP
        ↳42 DependencyGraphProof (⇔, 0 ms)
        ↳43 AND
            ↳44 QDP
                ↳45 UsableRulesReductionPairsProof (⇔, 0 ms)
                ↳46 QDP
                ↳47 PisEmptyProof (⇔, 0 ms)
                ↳48 YES
            ↳49 QDP
                ↳50 MRRProof (⇔, 0 ms)
                ↳51 QDP
                ↳52 UsableRulesReductionPairsProof (⇔, 0 ms)
                ↳53 QDP
                ↳54 MRRProof (⇔, 0 ms)
                ↳55 QDP
                ↳56 DependencyGraphProof (⇔, 0 ms)
                ↳57 TRUE
            ↳58 QDP
                ↳59 MRRProof (⇔, 5 ms)
                ↳60 QDP
                ↳61 UsableRulesReductionPairsProof (⇔, 0 ms)
                ↳62 QDP
                ↳63 MRRProof (⇔, 0 ms)
                ↳64 QDP
                ↳65 DependencyGraphProof (⇔, 0 ms)
                ↳66 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)) = 2 + x1   
POL(new(x1)) = 2 + x1   
POL(old(x1)) = 1 + 2·x1   
POL(serve) = 1   
POL(top1(x1, x2)) = 2·x1 + 2·x2   
POL(top2(x1, x2)) = 2·x1 + 2·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))


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

(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 + x1   
POL(serve) = 0   
POL(top1(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(top2(x1, x2)) = 2 + 2·x1 + 2·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)


(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) YES

(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) YES

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


The following pairs can be oriented strictly and are deleted.


TOP2(serve, free(y1)) → TOP1(check(free(serve)), y1)
TOP1(free(y0), serve) → TOP2(y0, check(free(serve)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( TOP1(x1, x2) ) = 2x1 + x2 + 2

POL( TOP2(x1, x2) ) = 2x1 + x2 + 2

POL( new(x1) ) = x1

POL( free(x1) ) = x1

POL( serve ) = 2

POL( check(x1) ) = 0

POL( old(x1) ) = max{0, -2}


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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)

(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)
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) SemLabProof (SOUND transformation)

We found the following model for the rules of the TRSs R and P. Interpretation over the domain with elements from 0 to 1.
old: 1
new: x0
TOP2: 0
serve: 0
check: 1
free: x0
TOP1: 0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.

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

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

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

(42) DependencyGraphProof (EQUIVALENT transformation)

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

(43) Complex Obligation (AND)

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

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

(45) 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-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 following rules are removed from R:

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

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

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

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

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

(50) 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   

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

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

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

(52) 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(free.0(x)) → free.1(check.0(x))
check.0(new.0(x)) → new.1(check.0(x))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(TOP1.1-0(x1, x2)) = x1 + x2   
POL(TOP2.1-0(x1, x2)) = x1 + x2   
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)) = x1   
POL(serve.) = 0   

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

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

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


Used ordering: 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   

(55) Obligation:

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

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

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

(56) DependencyGraphProof (EQUIVALENT transformation)

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

(57) TRUE

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

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

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

(59) 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   

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

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

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

(61) 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(free.0(x)) → free.1(check.0(x))
check.0(new.0(x)) → new.1(check.0(x))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(TOP1.0-1(x1, x2)) = x1 + x2   
POL(TOP2.0-1(x1, x2)) = x1 + x2   
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)) = x1   
POL(serve.) = 0   

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

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

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

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

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)))
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))))


Used ordering: Polynomial interpretation [POLO]:

POL(TOP1.0-1(x1, x2)) = 1 + x1 + x2   
POL(TOP2.0-1(x1, x2)) = 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   

(64) Obligation:

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

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

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

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

(65) DependencyGraphProof (EQUIVALENT transformation)

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

(66) TRUE