Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret2)

The rewrite relation of the following TRS is considered.

a(h,h,h,x)	→	s(x)	(1)
a(l,x,s(y),h)	→	a(l,x,y,s(h))	(2)
a(l,x,s(y),s(z))	→	a(l,x,y,a(l,x,s(y),z))	(3)
a(l,s(x),h,z)	→	a(l,x,z,z)	(4)
a(s(l),h,h,z)	→	a(l,z,h,z)	(5)
+(x,h)	→	x	(6)
+(h,x)	→	x	(7)
+(s(x),s(y))	→	s(s(+(x,y)))	(8)
+(+(x,y),z)	→	+(x,+(y,z))	(9)
s(h)	→	1	(10)
*(h,x)	→	h	(11)
*(x,h)	→	h	(12)
*(s(x),s(y))	→	s(+(+(*(x,y),x),y))	(13)

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.

a^#(h,h,h,x)	→	s^#(x)	(14)
a^#(l,x,s(y),h)	→	s^#(h)	(15)
a^#(l,x,s(y),h)	→	a^#(l,x,y,s(h))	(16)
a^#(l,x,s(y),s(z))	→	a^#(l,x,s(y),z)	(17)
a^#(l,x,s(y),s(z))	→	a^#(l,x,y,a(l,x,s(y),z))	(18)
a^#(l,s(x),h,z)	→	a^#(l,x,z,z)	(19)
a^#(s(l),h,h,z)	→	a^#(l,z,h,z)	(20)
+^#(s(x),s(y))	→	+^#(x,y)	(21)
+^#(s(x),s(y))	→	s^#(+(x,y))	(22)
+^#(s(x),s(y))	→	s^#(s(+(x,y)))	(23)
+^#(+(x,y),z)	→	+^#(y,z)	(24)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(25)
*^#(s(x),s(y))	→	*^#(x,y)	(26)
*^#(s(x),s(y))	→	+^#(*(x,y),x)	(27)
*^#(s(x),s(y))	→	+^#(+(*(x,y),x),y)	(28)
*^#(s(x),s(y))	→	s^#(+(+(*(x,y),x),y))	(29)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

a^#(s(l),h,h,z)	→	a^#(l,z,h,z)	(20)
a^#(l,s(x),h,z)	→	a^#(l,x,z,z)	(19)
a^#(l,x,s(y),s(z))	→	a^#(l,x,y,a(l,x,s(y),z))	(18)
a^#(l,x,s(y),s(z))	→	a^#(l,x,s(y),z)	(17)
a^#(l,x,s(y),h)	→	a^#(l,x,y,s(h))	(16)

1.1.1 Subterm Criterion Processor

We use the projection

π(a^#)

=

1

and remove the pairs:

a^#(s(l),h,h,z)

→

a^#(l,z,h,z)

(20)

1.1.1.1 Size-Change Termination

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

a^#(l,s(x),h,z)	→	a^#(l,x,z,z)	(19)

4	≥	4
4	≥	3
2	>	2
1	≥	1
a^#(l,x,s(y),s(z))	→	a^#(l,x,y,a(l,x,s(y),z))	(18)

3	>	3
2	≥	2
1	≥	1
a^#(l,x,s(y),s(z))	→	a^#(l,x,s(y),z)	(17)

4	>	4
3	≥	3
2	≥	2
1	≥	1
a^#(l,x,s(y),h)	→	a^#(l,x,y,s(h))	(16)

3	>	3
2	≥	2
1	≥	1

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

The 2^nd component contains the pair
*^#(s(x),s(y)) → *^#(x,y) (26)

1.1.2 Size-Change Termination

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

*^#(s(x),s(y)) → *^#(x,y) (26)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair

+^#(+(x,y),z) → +^#(x,+(y,z)) (25)

+^#(+(x,y),z) → +^#(y,z) (24)

+^#(s(x),s(y)) → +^#(x,y) (21)

1.1.3 Size-Change Termination

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

+^#(+(x,y),z) → +^#(x,+(y,z)) (25)

1 > 1

+^#(+(x,y),z) → +^#(y,z) (24)

2 ≥ 2

1 > 1

+^#(s(x),s(y)) → +^#(x,y) (21)

2 > 2

1 > 1

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