YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 UsableRulesProof (⇔, 0 ms)
↳17 QDP
↳18 QDPSizeChangeProof (⇔, 0 ms)
↳19 YES
↳20 QDP
↳21 UsableRulesProof (⇔, 0 ms)
↳22 QDP
↳23 QDPSizeChangeProof (⇔, 0 ms)
↳24 YES
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 QDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 14 ms)
↳34 QDP
↳35 MRRProof (⇔, 0 ms)
↳36 QDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 QDP
↳39 MRRProof (⇔, 0 ms)
↳40 QDP
↳41 PisEmptyProof (⇔, 0 ms)
↳42 YES
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
TOP(active(c)) → TOP(mark(c))
TOP(mark(x)) → TOP(check(x))
TOP(mark(x)) → CHECK(x)
CHECK(f(x)) → F(check(x))
CHECK(f(x)) → CHECK(x)
CHECK(x) → START(match(f(X), x))
CHECK(x) → MATCH(f(X), x)
CHECK(x) → F(X)
MATCH(f(x), f(y)) → F(match(x, y))
MATCH(f(x), f(y)) → MATCH(x, y)
MATCH(X, x) → PROPER(x)
PROPER(f(x)) → F(proper(x))
PROPER(f(x)) → PROPER(x)
F(ok(x)) → F(x)
F(found(x)) → F(x)
TOP(found(x)) → TOP(active(x))
TOP(found(x)) → ACTIVE(x)
ACTIVE(f(x)) → F(active(x))
ACTIVE(f(x)) → ACTIVE(x)
F(mark(x)) → F(x)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
F(found(x)) → F(x)
F(ok(x)) → F(x)
F(mark(x)) → F(x)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
F(found(x)) → F(x)
F(ok(x)) → F(x)
F(mark(x)) → F(x)
From the DPs we obtained the following set of size-change graphs:
ACTIVE(f(x)) → ACTIVE(x)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
ACTIVE(f(x)) → ACTIVE(x)
From the DPs we obtained the following set of size-change graphs:
PROPER(f(x)) → PROPER(x)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
PROPER(f(x)) → PROPER(x)
From the DPs we obtained the following set of size-change graphs:
MATCH(f(x), f(y)) → MATCH(x, y)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
MATCH(f(x), f(y)) → MATCH(x, y)
From the DPs we obtained the following set of size-change graphs:
CHECK(f(x)) → CHECK(x)
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
CHECK(f(x)) → CHECK(x)
From the DPs we obtained the following set of size-change graphs:
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
TOP(active(c)) → TOP(mark(c))
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
TOP(active(c)) → TOP(mark(c))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
start(ok(x)) → found(x)
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(active(c)) → TOP(mark(c))
TOP1 > [c, proper] > [mark, check, f]
X > [c, proper] > [mark, check, f]
TOP1: [1]
mark: multiset
check: multiset
c: multiset
f: multiset
X: multiset
proper: multiset
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
match(f(x), f(y)) → f(match(x, y))
start(ok(x)) → found(x)
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
start(ok(x)) → found(x)
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
match(f(x), f(y)) → f(match(x, y))
POL(TOP(x1)) = x1
POL(X) = 0
POL(active(x1)) = x1
POL(c) = 1
POL(check(x1)) = 1 + x1
POL(f(x1)) = 1 + x1
POL(found(x1)) = x1
POL(mark(x1)) = 1 + x1
POL(match(x1, x2)) = x1 + x2
POL(ok(x1)) = x1
POL(proper(x1)) = x1
POL(start(x1)) = x1
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
start(ok(x)) → found(x)
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
TOP(mark(x)) → TOP(check(x))
TOP(found(x)) → TOP(active(x))
active(f(x)) → mark(x)
active(f(x)) → f(active(x))
f(ok(x)) → ok(f(x))
f(found(x)) → found(f(x))
f(mark(x)) → mark(f(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
active1 > X > check1 > start1 > f1 > mark1 > TOP1 > match2 > found1 > ok1
X=1
active_1=3
f_1=5
mark_1=8
ok_1=1
found_1=4
check_1=7
start_1=1
TOP_1=1
match_2=0