Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-15)

The rewrite relation of the following TRS is considered.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.