Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/Ex6_9_Luc02c_GM)

The rewrite relation of the following TRS is considered.

a__2nd(cons1(X,cons(Y,Z))) → mark(Y) (1)
a__2nd(cons(X,X1)) → a__2nd(cons1(mark(X),mark(X1))) (2)
a__from(X) → cons(mark(X),from(s(X))) (3)
mark(2nd(X)) → a__2nd(mark(X)) (4)
mark(from(X)) → a__from(mark(X)) (5)
mark(cons(X1,X2)) → cons(mark(X1),X2) (6)
mark(s(X)) → s(mark(X)) (7)
mark(cons1(X1,X2)) → cons1(mark(X1),mark(X2)) (8)
a__2nd(X) → 2nd(X) (9)
a__from(X) → from(X) (10)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a__2nd#(cons1(X,cons(Y,Z))) → mark#(Y) (11)
a__2nd#(cons(X,X1)) → a__2nd#(cons1(mark(X),mark(X1))) (12)
a__2nd#(cons(X,X1)) → mark#(X) (13)
a__2nd#(cons(X,X1)) → mark#(X1) (14)
a__from#(X) → mark#(X) (15)
mark#(2nd(X)) → a__2nd#(mark(X)) (16)
mark#(2nd(X)) → mark#(X) (17)
mark#(from(X)) → a__from#(mark(X)) (18)
mark#(from(X)) → mark#(X) (19)
mark#(cons(X1,X2)) → mark#(X1) (20)
mark#(s(X)) → mark#(X) (21)
mark#(cons1(X1,X2)) → mark#(X1) (22)
mark#(cons1(X1,X2)) → mark#(X2) (23)

1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[a__2nd#(x1)] =
-∞
+
0
· x1
[cons1(x1, x2)] =
1
+
0
· x1 +
0
· x2
[cons(x1, x2)] =
1
+
0
· x1 +
0
· x2
[mark#(x1)] =
1
+
0
· x1
[mark(x1)] =
-∞
+
0
· x1
[a__from#(x1)] =
1
+
0
· x1
[2nd(x1)] =
-∞
+
1
· x1
[from(x1)] =
1
+
0
· x1
[s(x1)] =
-∞
+
0
· x1
[a__2nd(x1)] =
-∞
+
1
· x1
[a__from(x1)] =
1
+
0
· x1
the pair
mark#(2nd(X)) → a__2nd#(mark(X)) (16)
could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.