Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-25)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c#(c(z,x,a),a,y) f#(f(c(y,a,f(c(z,y,x))))) (4)
c#(c(z,x,a),a,y) f#(c(y,a,f(c(z,y,x)))) (5)
c#(c(z,x,a),a,y) c#(y,a,f(c(z,y,x))) (6)
c#(c(z,x,a),a,y) f#(c(z,y,x)) (7)
c#(c(z,x,a),a,y) c#(z,y,x) (8)
f#(f(c(a,y,z))) b#(y,b(z,z)) (9)
f#(f(c(a,y,z))) b#(z,z) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.