Certification Problem

Input (TPDB SRS_Standard/Secret_05_SRS/matchbox1)

The rewrite relation of the following TRS is considered.

r(e(x1)) → w(r(x1)) (1)
i(t(x1)) → e(r(x1)) (2)
e(w(x1)) → r(i(x1)) (3)
t(e(x1)) → r(e(x1)) (4)
w(r(x1)) → i(t(x1)) (5)
e(r(x1)) → e(w(x1)) (6)
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1)))))) (7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[r(x1)] = 1 · x1 + 2
[e(x1)] = 1 · x1 + 1
[w(x1)] = 1 · x1 + 1
[i(x1)] = 1 · x1
[t(x1)] = 1 · x1 + 3
all of the following rules can be deleted.
t(e(x1)) → r(e(x1)) (4)
e(r(x1)) → e(w(x1)) (6)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
r#(e(x1)) → w#(r(x1)) (8)
r#(e(x1)) → r#(x1) (9)
i#(t(x1)) → e#(r(x1)) (10)
i#(t(x1)) → r#(x1) (11)
e#(w(x1)) → r#(i(x1)) (12)
e#(w(x1)) → i#(x1) (13)
w#(r(x1)) → i#(t(x1)) (14)
r#(i(t(e(r(x1))))) → e#(w(r(i(t(e(x1)))))) (15)
r#(i(t(e(r(x1))))) → w#(r(i(t(e(x1))))) (16)
r#(i(t(e(r(x1))))) → r#(i(t(e(x1)))) (17)
r#(i(t(e(r(x1))))) → i#(t(e(x1))) (18)
r#(i(t(e(r(x1))))) → e#(x1) (19)

1.1.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[r(x1)] = 2 + 1 · x1
[e(x1)] = 1 + 1 · x1
[w(x1)] = 1 + 1 · x1
[i(x1)] = 1 · x1
[t(x1)] = 3 + 1 · x1
[r#(x1)] = 2 + 1 · x1
[w#(x1)] = 1 + 1 · x1
[i#(x1)] = 1 · x1
[e#(x1)] = 1 + 1 · x1
the pairs
r#(e(x1)) → r#(x1) (9)
i#(t(x1)) → r#(x1) (11)
e#(w(x1)) → i#(x1) (13)
r#(i(t(e(r(x1))))) → w#(r(i(t(e(x1))))) (16)
r#(i(t(e(r(x1))))) → r#(i(t(e(x1)))) (17)
r#(i(t(e(r(x1))))) → i#(t(e(x1))) (18)
r#(i(t(e(r(x1))))) → e#(x1) (19)
and no rules could be deleted.

1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals
[r#(x1)] =
0
-∞
-∞
+
-∞ 0 -∞
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[e(x1)] =
1
0
0
+
0 0 0
0 0 0
-∞ -∞ 0
· x1
[w#(x1)] =
-∞
-∞
-∞
+
0 0 0
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[r(x1)] =
0
0
0
+
0 -∞ 0
0 0 0
-∞ -∞ -∞
· x1
[i#(x1)] =
-∞
-∞
-∞
+
0 0 0
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[t(x1)] =
0
0
0
+
-∞ 0 0
-∞ -∞ -∞
0 0 0
· x1
[e#(x1)] =
0
-∞
-∞
+
-∞ -∞ 0
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[w(x1)] =
1
1
0
+
0 0 0
0 0 0
-∞ -∞ 0
· x1
[i(x1)] =
1
0
0
+
0 0 0
-∞ -∞ 0
-∞ 0 -∞
· x1
the pair
r#(i(t(e(r(x1))))) → e#(w(r(i(t(e(x1)))))) (15)
could be deleted.

1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals
[r#(x1)] =
1
-∞
-∞
+
1 0 -∞
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[e(x1)] =
0
1
0
+
0 0 1
-∞ 0 0
-∞ 0 0
· x1
[w#(x1)] =
-∞
-∞
-∞
+
0 0 0
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[r(x1)] =
0
-∞
0
+
0 0 1
-∞ 0 0
-∞ 0 0
· x1
[i#(x1)] =
-∞
-∞
-∞
+
0 0 -∞
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[t(x1)] =
0
0
1
+
0 0 1
-∞ 0 0
0 1 1
· x1
[e#(x1)] =
0
-∞
-∞
+
0 0 0
-∞ -∞ -∞
-∞ -∞ -∞
· x1
[w(x1)] =
-∞
1
-∞
+
0 0 1
-∞ 0 0
-∞ 0 0
· x1
[i(x1)] =
0
1
0
+
-∞ -∞ 0
-∞ 0 -∞
-∞ 0 -∞
· x1
the pair
r#(e(x1)) → w#(r(x1)) (8)
could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.