Certification Problem

Input (TPDB TRS_Standard/AProVE_04/Liveness6.3)

The rewrite relation of the following TRS is considered.

rec(rec(x)) → sent(rec(x)) (1)
rec(sent(x)) → sent(rec(x)) (2)
rec(no(x)) → sent(rec(x)) (3)
rec(bot) → up(sent(bot)) (4)
rec(up(x)) → up(rec(x)) (5)
sent(up(x)) → up(sent(x)) (6)
no(up(x)) → up(no(x)) (7)
top(rec(up(x))) → top(check(rec(x))) (8)
top(sent(up(x))) → top(check(rec(x))) (9)
top(no(up(x))) → top(check(rec(x))) (10)
check(up(x)) → up(check(x)) (11)
check(sent(x)) → sent(check(x)) (12)
check(rec(x)) → rec(check(x)) (13)
check(no(x)) → no(check(x)) (14)
check(no(x)) → no(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
[up(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[sent(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[bot] =
0 0 0
0 0 0
0 0 0
[top(x1)] =
1 1 0
0 0 0
1 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[rec(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 0 0
0 0 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[no(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
1 0 0
1 0 0
1 0 0
all of the following rules can be deleted.
rec(no(x)) → sent(rec(x)) (3)
top(no(up(x))) → top(check(rec(x))) (10)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[up(x1)] =
1 1 0
0 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[sent(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[bot] =
1 0 0
0 0 0
0 0 0
[top(x1)] =
1 0 1
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[rec(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
1 0 0
0 0 0
1 0 0
[check(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[no(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
1 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
rec(rec(x)) → sent(rec(x)) (1)
top(rec(up(x))) → top(check(rec(x))) (8)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[up(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[sent(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[bot] =
1 0 0
0 0 0
0 0 0
[top(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[rec(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[check(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[no(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
no(up(x)) → up(no(x)) (7)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[up(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[sent(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[bot] =
0 0 0
0 0 0
1 0 0
[top(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[rec(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[check(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[no(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
rec(bot) → up(sent(bot)) (4)

1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(check) = 7 weight(check) = 2
prec(top) = 5 weight(top) = 2
prec(up) = 0 weight(up) = 3
prec(no) = 6 weight(no) = 2
prec(sent) = 2 weight(sent) = 2
prec(rec) = 3 weight(rec) = 2
all of the following rules can be deleted.
rec(sent(x)) → sent(rec(x)) (2)
rec(up(x)) → up(rec(x)) (5)
sent(up(x)) → up(sent(x)) (6)
top(sent(up(x))) → top(check(rec(x))) (9)
check(up(x)) → up(check(x)) (11)
check(sent(x)) → sent(check(x)) (12)
check(rec(x)) → rec(check(x)) (13)
check(no(x)) → no(check(x)) (14)
check(no(x)) → no(x) (15)

1.1.1.1.1.1 R is empty

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