Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-1)

The rewrite relation of the following TRS is considered.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.