Certification Problem

Input (TPDB TRS_Relative/INVY_15/ex4)

The relative rewrite relation R/S is considered where R is the following TRS

a → b (1)

and S is the following TRS.

c(x,c(y,z)) → c(y,c(x,z)) (2)
f(s(x)) → c(x,f(x)) (3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[a] =
1
1
[b] =
0
1
[c(x1, x2)] =
0
0
+
1 1
0 0
· x1 +
1 0
0 0
· x2
[y] =
0
0
[z] =
0
1
[f(x1)] =
0
0
+
1 1
0 0
· x1
[s(x1)] =
0
0
+
1 1
1 1
· x1
all of the following rules can be deleted.
a → b (1)

1.1 R is empty

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