YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 38 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 8 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 QDPSizeChangeProof (⇔, 0 ms)
↳23 YES
↳24 QDP
↳25 UsableRulesProof (⇔, 0 ms)
↳26 QDP
↳27 QDPOrderProof (⇔, 10 ms)
↳28 QDP
↳29 PisEmptyProof (⇔, 0 ms)
↳30 YES
top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
serve'(old(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(check(x1)) = x1
POL(free(x1)) = x1
POL(new(x1)) = x1
POL(old(x1)) = 1 + x1
POL(serve'(x1)) = x1
POL(top(x1)) = x1
serve'(old(x)) → serve'(free(x))
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
FREE(top(x)) → NEW(check(top(x)))
FREE(new(x)) → NEW(free(x))
FREE(new(x)) → FREE(x)
FREE(old(x)) → OLD(free(x))
FREE(old(x)) → FREE(x)
SERVE'(new(x)) → SERVE'(free(x))
SERVE'(new(x)) → FREE(x)
FREE(check(x)) → FREE(x)
NEW(check(x)) → NEW(x)
OLD(check(x)) → OLD(x)
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
OLD(check(x)) → OLD(x)
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
OLD(check(x)) → OLD(x)
From the DPs we obtained the following set of size-change graphs:
NEW(check(x)) → NEW(x)
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
NEW(check(x)) → NEW(x)
From the DPs we obtained the following set of size-change graphs:
FREE(old(x)) → FREE(x)
FREE(new(x)) → FREE(x)
FREE(check(x)) → FREE(x)
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
FREE(old(x)) → FREE(x)
FREE(new(x)) → FREE(x)
FREE(check(x)) → FREE(x)
From the DPs we obtained the following set of size-change graphs:
SERVE'(new(x)) → SERVE'(free(x))
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
SERVE'(new(x)) → SERVE'(free(x))
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
free(check(x)) → check(free(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
new(check(x)) → check(new(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SERVE'(new(x)) → SERVE'(free(x))
POL(SERVE'(x1)) = x1
POL(check(x1)) = 0
POL(free(x1)) = x1
POL(new(x1)) = 1 + x1
POL(old(x1)) = 0
POL(top(x1)) = 1
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
free(check(x)) → check(free(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
new(check(x)) → check(new(x))
free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
free(check(x)) → check(free(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)
new(check(x)) → check(new(x))