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 ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(y,z)	→	c^#(y,z,z)	(4)
b^#(y,z)	→	c^#(c(y,z,z),a,a)	(5)
c^#(f(z),f(c(a,x,a)),y)	→	c^#(z,y,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^#(f(b(x,z)),c(z,y,a),a)	(8)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

c^#(f(z),f(c(a,x,a)),y) → c^#(z,y,a) (6)

c^#(f(z),f(c(a,x,a)),y) → b^#(x,z) (7)

b^#(y,z) → c^#(y,z,z) (4)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

c^#(f(z),f(c(a,x,a)),y) → c^#(z,y,a) (6)

3 ≥ 2

2 > 3

1 > 1

c^#(f(z),f(c(a,x,a)),y) → b^#(x,z) (7)

2 > 1

1 > 2

b^#(y,z) → c^#(y,z,z) (4)

2 ≥ 3

2 ≥ 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.