Certification Problem

Input (TPDB TRS_Standard/CiME_04/filliatre3)

The rewrite relation of the following TRS is considered.

g(A) A (1)
g(B) A (2)
g(B) B (3)
g(C) A (4)
g(C) B (5)
g(C) C (6)
foldB(t,0) t (7)
foldB(t,s(n)) f(foldB(t,n),B) (8)
foldC(t,0) t (9)
foldC(t,s(n)) f(foldC(t,n),C) (10)
f(t,x) f'(t,g(x)) (11)
f'(triple(a,b,c),C) triple(a,b,s(c)) (12)
f'(triple(a,b,c),B) f(triple(a,b,c),A) (13)
f'(triple(a,b,c),A) f''(foldB(triple(s(a),0,c),b)) (14)
f''(triple(a,b,c)) foldC(triple(a,b,0),c) (15)
fold(t,x,0) t (16)
fold(t,x,s(n)) f(fold(t,x,n),x) (17)

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#(t,x) f'#(t,g(x)) (18)
foldC#(t,s(n)) f#(foldC(t,n),C) (19)
fold#(t,x,s(n)) fold#(t,x,n) (20)
foldB#(t,s(n)) foldB#(t,n) (21)
f''#(triple(a,b,c)) foldC#(triple(a,b,0),c) (22)
foldC#(t,s(n)) foldC#(t,n) (23)
foldB#(t,s(n)) f#(foldB(t,n),B) (24)
f'#(triple(a,b,c),A) foldB#(triple(s(a),0,c),b) (25)
f#(t,x) g#(x) (26)
f'#(triple(a,b,c),B) f#(triple(a,b,c),A) (27)
fold#(t,x,s(n)) f#(fold(t,x,n),x) (28)
f'#(triple(a,b,c),A) f''#(foldB(triple(s(a),0,c),b)) (29)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.