Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/gen-9)

The rewrite relation of the following TRS is considered.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

f^#(c(x,y,z))

→

f^#(b(y,z))

(6)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals

[c(x₁, x₂, x₃)]

2	0
2	0

· x₁ +

2	0
0	0

· x₂ +

0	0
2	0

· x₃ +

1	0
0	0

[f(x₁)]

0	1
2	0

· x₁ +

0	0
2	0

[a]

0	0
0	0

[f^#(x₁)]

1	2
0	0

· x₁ +

0	0
0	0

[b(x₁, x₂)]

2	0
0	0

· x₁ +

1	0
1	0

· x₂ +

0	0
0	0

together with the usable rules

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

(w.r.t. the implicit argument filter of the reduction pair), the pair

f^#(c(x,y,z))

→

f^#(b(y,z))

(6)

could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

b^#(z,b(c(a,y,a),f(f(x))))	→	c^#(c(y,a,z),z,x)	(9)
c^#(c(z,y,a),a,a)	→	b^#(z,y)	(4)
b^#(z,b(c(a,y,a),f(f(x))))	→	c^#(y,a,z)	(8)

1.1.2 Subterm Criterion Processor

We use the projection to multisets

π(b^#)	=	{ 1, 1, 1, 2 }
π(c^#)	=	{ 1, 1, 1 }
π(b)	=	{ 1, 1, 1, 2, 2 }
π(c)	=	{ 1, 1, 1, 2, 2, 2 }

to remove the pairs:

b^#(z,b(c(a,y,a),f(f(x))))	→	c^#(c(y,a,z),z,x)	(9)
c^#(c(z,y,a),a,a)	→	b^#(z,y)	(4)
b^#(z,b(c(a,y,a),f(f(x))))	→	c^#(y,a,z)	(8)

1.1.2.1 P is empty

There are no pairs anymore.