Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret2)

The rewrite relation of the following TRS is considered.

a(h,h,h,x) s(x) (1)
a(l,x,s(y),h) a(l,x,y,s(h)) (2)
a(l,x,s(y),s(z)) a(l,x,y,a(l,x,s(y),z)) (3)
a(l,s(x),h,z) a(l,x,z,z) (4)
a(s(l),h,h,z) a(l,z,h,z) (5)
+(x,h) x (6)
+(h,x) x (7)
+(s(x),s(y)) s(s(+(x,y))) (8)
+(+(x,y),z) +(x,+(y,z)) (9)
s(h) 1 (10)
*(h,x) h (11)
*(x,h) h (12)
*(s(x),s(y)) s(+(+(*(x,y),x),y)) (13)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a#(l,x,s(y),h) s#(h) (14)
*#(s(x),s(y)) *#(x,y) (15)
+#(s(x),s(y)) s#(s(+(x,y))) (16)
a#(s(l),h,h,z) a#(l,z,h,z) (17)
a#(l,x,s(y),s(z)) a#(l,x,s(y),z) (18)
a#(h,h,h,x) s#(x) (19)
+#(s(x),s(y)) s#(+(x,y)) (20)
+#(+(x,y),z) +#(x,+(y,z)) (21)
a#(l,x,s(y),s(z)) a#(l,x,y,a(l,x,s(y),z)) (22)
*#(s(x),s(y)) +#(*(x,y),x) (23)
a#(l,s(x),h,z) a#(l,x,z,z) (24)
*#(s(x),s(y)) s#(+(+(*(x,y),x),y)) (25)
a#(l,x,s(y),h) a#(l,x,y,s(h)) (26)
+#(+(x,y),z) +#(y,z) (27)
+#(s(x),s(y)) +#(x,y) (28)
*#(s(x),s(y)) +#(+(*(x,y),x),y) (29)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.