Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-28)

The rewrite relation of the following TRS is considered.

b(y,z) f(c(c(y,z,z),a,a)) (1)
b(b(z,y),a) z (2)
c(f(z),f(c(a,x,a)),y) c(f(b(x,z)),c(z,y,a),a) (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.
b#(y,z) c#(c(y,z,z),a,a) (4)
b#(y,z) c#(y,z,z) (5)
c#(f(z),f(c(a,x,a)),y) c#(f(b(x,z)),c(z,y,a),a) (6)
c#(f(z),f(c(a,x,a)),y) b#(x,z) (7)
c#(f(z),f(c(a,x,a)),y) c#(z,y,a) (8)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.