Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-22)

The rewrite relation of the following TRS is considered.

b(a,b(c(z,x,y),a)) b(b(z,c(y,z,a)),x) (1)
f(c(a,b(b(z,a),y),x)) f(c(x,b(z,x),y)) (2)
c(f(c(a,y,a)),x,z) f(b(b(z,z),f(b(y,b(x,a))))) (3)

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.
b#(a,b(c(z,x,y),a)) c#(y,z,a) (4)
b#(a,b(c(z,x,y),a)) b#(z,c(y,z,a)) (5)
b#(a,b(c(z,x,y),a)) b#(b(z,c(y,z,a)),x) (6)
f#(c(a,b(b(z,a),y),x)) b#(z,x) (7)
f#(c(a,b(b(z,a),y),x)) c#(x,b(z,x),y) (8)
f#(c(a,b(b(z,a),y),x)) f#(c(x,b(z,x),y)) (9)
c#(f(c(a,y,a)),x,z) b#(x,a) (10)
c#(f(c(a,y,a)),x,z) b#(y,b(x,a)) (11)
c#(f(c(a,y,a)),x,z) f#(b(y,b(x,a))) (12)
c#(f(c(a,y,a)),x,z) b#(z,z) (13)
c#(f(c(a,y,a)),x,z) b#(b(z,z),f(b(y,b(x,a)))) (14)
c#(f(c(a,y,a)),x,z) f#(b(b(z,z),f(b(y,b(x,a))))) (15)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.