Certification Problem

Input (TPDB TRS_Standard/TCT_12/recursion-10)

The rewrite relation of the following TRS is considered.

f_0(x) → a (1)
f_1(x) → g_1(x,x) (2)
g_1(s(x),y) → b(f_0(y),g_1(x,y)) (3)
f_2(x) → g_2(x,x) (4)
g_2(s(x),y) → b(f_1(y),g_2(x,y)) (5)
f_3(x) → g_3(x,x) (6)
g_3(s(x),y) → b(f_2(y),g_3(x,y)) (7)
f_4(x) → g_4(x,x) (8)
g_4(s(x),y) → b(f_3(y),g_4(x,y)) (9)
f_5(x) → g_5(x,x) (10)
g_5(s(x),y) → b(f_4(y),g_5(x,y)) (11)
f_6(x) → g_6(x,x) (12)
g_6(s(x),y) → b(f_5(y),g_6(x,y)) (13)
f_7(x) → g_7(x,x) (14)
g_7(s(x),y) → b(f_6(y),g_7(x,y)) (15)
f_8(x) → g_8(x,x) (16)
g_8(s(x),y) → b(f_7(y),g_8(x,y)) (17)
f_9(x) → g_9(x,x) (18)
g_9(s(x),y) → b(f_8(y),g_9(x,y)) (19)
f_10(x) → g_10(x,x) (20)
g_10(s(x),y) → b(f_9(y),g_10(x,y)) (21)

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.
f_3#(x) → g_3#(x,x) (22)
f_2#(x) → g_2#(x,x) (23)
g_4#(s(x),y) → g_4#(x,y) (24)
g_3#(s(x),y) → g_3#(x,y) (25)
f_6#(x) → g_6#(x,x) (26)
f_10#(x) → g_10#(x,x) (27)
g_1#(s(x),y) → f_0#(y) (28)
f_8#(x) → g_8#(x,x) (29)
g_3#(s(x),y) → f_2#(y) (30)
f_5#(x) → g_5#(x,x) (31)
f_9#(x) → g_9#(x,x) (32)
g_1#(s(x),y) → g_1#(x,y) (33)
g_9#(s(x),y) → g_9#(x,y) (34)
g_5#(s(x),y) → f_4#(y) (35)
f_7#(x) → g_7#(x,x) (36)
g_4#(s(x),y) → f_3#(y) (37)
g_7#(s(x),y) → g_7#(x,y) (38)
g_10#(s(x),y) → g_10#(x,y) (39)
g_7#(s(x),y) → f_6#(y) (40)
g_8#(s(x),y) → f_7#(y) (41)
g_9#(s(x),y) → f_8#(y) (42)
f_4#(x) → g_4#(x,x) (43)
g_10#(s(x),y) → f_9#(y) (44)
g_2#(s(x),y) → g_2#(x,y) (45)
g_6#(s(x),y) → f_5#(y) (46)
f_1#(x) → g_1#(x,x) (47)
g_5#(s(x),y) → g_5#(x,y) (48)
g_2#(s(x),y) → f_1#(y) (49)
g_6#(s(x),y) → g_6#(x,y) (50)
g_8#(s(x),y) → g_8#(x,y) (51)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.