Certification Problem

Input (TPDB TRS_Standard/Various_04/12)

The rewrite relation of the following TRS is considered.

O(0) 0 (1)
+(0,x) x (2)
+(x,0) x (3)
+(O(x),O(y)) O(+(x,y)) (4)
+(O(x),I(y)) I(+(x,y)) (5)
+(I(x),O(y)) I(+(x,y)) (6)
+(I(x),I(y)) O(+(+(x,y),I(0))) (7)
*(0,x) 0 (8)
*(x,0) 0 (9)
*(O(x),y) O(*(x,y)) (10)
*(I(x),y) +(O(*(x,y)),y) (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
+#(O(x),O(y)) +#(x,y) (12)
+#(O(x),O(y)) O#(+(x,y)) (13)
+#(O(x),I(y)) +#(x,y) (14)
+#(I(x),O(y)) +#(x,y) (15)
+#(I(x),I(y)) +#(x,y) (16)
+#(I(x),I(y)) +#(+(x,y),I(0)) (17)
+#(I(x),I(y)) O#(+(+(x,y),I(0))) (18)
*#(O(x),y) *#(x,y) (19)
*#(O(x),y) O#(*(x,y)) (20)
*#(I(x),y) *#(x,y) (21)
*#(I(x),y) O#(*(x,y)) (22)
*#(I(x),y) +#(O(*(x,y)),y) (23)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.