Certification Problem

Input (TPDB TRS_Standard/AProVE_04/Liveness8)

The rewrite relation of the following TRS is considered.

active(f(x)) → mark(x) (1)
top(active(c)) → top(mark(c)) (2)
top(mark(x)) → top(check(x)) (3)
check(f(x)) → f(check(x)) (4)
check(x) → start(match(f(X),x)) (5)
match(f(x),f(y)) → f(match(x,y)) (6)
match(X,x) → proper(x) (7)
proper(c) → ok(c) (8)
proper(f(x)) → f(proper(x)) (9)
f(ok(x)) → ok(f(x)) (10)
start(ok(x)) → found(x) (11)
f(found(x)) → found(f(x)) (12)
top(found(x)) → top(active(x)) (13)
active(f(x)) → f(active(x)) (14)
f(mark(x)) → mark(f(x)) (15)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[start(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[c] =
0 0 0
0 0 0
1 0 0
[check(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[ok(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[f(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[match(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 0
0 1 1
0 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[found(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[proper(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[X] =
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
f(ok(x)) → ok(f(x)) (10)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[start(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
1 0 0
0 0 0
[active(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[c] =
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[ok(x1)] =
1 1 1
0 0 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[f(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[match(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 0
0 0 1
0 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[found(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[proper(x1)] =
1 0 0
0 0 1
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[X] =
0 0 0
1 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
active(f(x)) → mark(x) (1)
active(f(x)) → f(active(x)) (14)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[start(x1)] =
1 1 0
0 0 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[c] =
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 1 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[ok(x1)] =
1 1 0
1 0 0
1 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[f(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[match(x1, x2)] =
1 0 0
1 0 0
0 0 0
· x1 +
1 0 0
0 1 1
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[found(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[proper(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[X] =
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
all of the following rules can be deleted.
check(f(x)) → f(check(x)) (4)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
[start(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[c] =
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 1 0
0 0 0
1 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[ok(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[f(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[match(x1, x2)] =
1 0 0
0 1 0
1 0 0
· x1 +
1 1 0
0 1 0
1 1 1
· x2 +
0 0 0
0 0 0
1 0 0
[found(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[proper(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[X] =
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
match(f(x),f(y)) → f(match(x,y)) (6)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[start(x1)] =
1 0 0
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[active(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
0 0 0
1 0 0
0 0 0
[c] =
0 0 0
1 0 0
1 0 0
[check(x1)] =
1 0 0
1 1 0
1 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[ok(x1)] =
1 0 0
0 0 1
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[f(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[match(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 1
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[found(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[proper(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[X] =
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
f(found(x)) → found(f(x)) (12)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[top(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[start(x1)] =
1 0 1
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[active(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[c] =
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 0 0
0 0 0
1 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[ok(x1)] =
1 0 0
0 0 0
1 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[f(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[match(x1, x2)] =
1 0 0
0 0 0
0 1 0
· x1 +
1 0 0
1 0 1
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[found(x1)] =
1 0 0
0 1 0
1 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[proper(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[X] =
0 0 0
1 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
top(active(c)) → top(mark(c)) (2)

1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(found) = 9 weight(found) = 1
prec(ok) = 6 weight(ok) = 1
prec(proper) = 8 weight(proper) = 1
prec(start) = 1 weight(start) = 1
prec(match) = 12 weight(match) = 0
prec(X) = 10 weight(X) = 1
prec(check) = 2 weight(check) = 6
prec(top) = 15 weight(top) = 2
prec(c) = 14 weight(c) = 1
prec(mark) = 3 weight(mark) = 6
prec(active) = 0 weight(active) = 1
prec(f) = 5 weight(f) = 4
all of the following rules can be deleted.
top(mark(x)) → top(check(x)) (3)
check(x) → start(match(f(X),x)) (5)
match(X,x) → proper(x) (7)
proper(c) → ok(c) (8)
proper(f(x)) → f(proper(x)) (9)
start(ok(x)) → found(x) (11)
top(found(x)) → top(active(x)) (13)
f(mark(x)) → mark(f(x)) (15)

1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.