Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret4)

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)
app(nil,k)	→	k	(11)
app(l,nil)	→	l	(12)
app(cons(x,l),k)	→	cons(x,app(l,k))	(13)
sum(cons(x,nil))	→	cons(x,nil)	(14)
sum(cons(x,cons(y,l)))	→	sum(cons(a(x,y,h,h),l))	(15)

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)	(16)
a^#(l,x,s(y),h)	→	s^#(h)	(17)
a^#(l,x,s(y),h)	→	a^#(l,x,y,s(h))	(18)
a^#(l,x,s(y),s(z))	→	a^#(l,x,s(y),z)	(19)
a^#(l,x,s(y),s(z))	→	a^#(l,x,y,a(l,x,s(y),z))	(20)
a^#(l,s(x),h,z)	→	a^#(l,x,z,z)	(21)
a^#(s(l),h,h,z)	→	a^#(l,z,h,z)	(22)
+^#(s(x),s(y))	→	+^#(x,y)	(23)
+^#(s(x),s(y))	→	s^#(+(x,y))	(24)
+^#(s(x),s(y))	→	s^#(s(+(x,y)))	(25)
+^#(+(x,y),z)	→	+^#(y,z)	(26)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(27)
app^#(cons(x,l),k)	→	app^#(l,k)	(28)
sum^#(cons(x,cons(y,l)))	→	a^#(x,y,h,h)	(29)
sum^#(cons(x,cons(y,l)))	→	sum^#(cons(a(x,y,h,h),l))	(30)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

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

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

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

1.1.1 Size-Change Termination

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

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

2 ≥ 2

1 > 1

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

1 > 1

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

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
app^#(cons(x,l),k) → app^#(l,k) (28)

1.1.2 Size-Change Termination

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

app^#(cons(x,l),k) → app^#(l,k) (28)

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

sum^#(cons(x,cons(y,l)))

→

sum^#(cons(a(x,y,h,h),l))

(30)

1.1.3 Subterm Criterion Processor

We use the projection to multisets

π(sum^#)	=	{ 1 }
π(cons)	=	{ 2, 2, 2 }

to remove the pairs:

sum^#(cons(x,cons(y,l)))

→

sum^#(cons(a(x,y,h,h),l))

(30)

1.1.3.1 P is empty

There are no pairs anymore.

The 4^th component contains the pair

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

1.1.4 Size-Change Termination

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

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

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

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))	(20)

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

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

3	>	3
2	≥	2
1	≥	1

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