Certification Problem

Input (TPDB TRS_Standard/Rubio_04/elimdupl)

The rewrite relation of the following TRS is considered.

eq(0,0)	→	true	(1)
eq(0,s(X))	→	false	(2)
eq(s(X),0)	→	false	(3)
eq(s(X),s(Y))	→	eq(X,Y)	(4)
rm(N,nil)	→	nil	(5)
rm(N,add(M,X))	→	ifrm(eq(N,M),N,add(M,X))	(6)
ifrm(true,N,add(M,X))	→	rm(N,X)	(7)
ifrm(false,N,add(M,X))	→	add(M,rm(N,X))	(8)
purge(nil)	→	nil	(9)
purge(add(N,X))	→	add(N,purge(rm(N,X)))	(10)

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.

eq^#(s(X),s(Y))	→	eq^#(X,Y)	(11)
rm^#(N,add(M,X))	→	eq^#(N,M)	(12)
rm^#(N,add(M,X))	→	ifrm^#(eq(N,M),N,add(M,X))	(13)
ifrm^#(true,N,add(M,X))	→	rm^#(N,X)	(14)
ifrm^#(false,N,add(M,X))	→	rm^#(N,X)	(15)
purge^#(add(N,X))	→	rm^#(N,X)	(16)
purge^#(add(N,X))	→	purge^#(rm(N,X))	(17)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

purge^#(add(N,X))

→

purge^#(rm(N,X))

(17)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(purge^#)	=	{ 1 }
π(ifrm)	=	{ 3, 3 }
π(add)	=	{ 1, 2, 2 }
π(rm)	=	{ 2, 2 }
π(s)	=	{ 1 }

to remove the pairs:

purge^#(add(N,X))

→

purge^#(rm(N,X))

(17)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

rm^#(N,add(M,X))	→	ifrm^#(eq(N,M),N,add(M,X))	(13)
ifrm^#(true,N,add(M,X))	→	rm^#(N,X)	(14)
ifrm^#(false,N,add(M,X))	→	rm^#(N,X)	(15)

1.1.2 Size-Change Termination

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

rm^#(N,add(M,X))	→	ifrm^#(eq(N,M),N,add(M,X))	(13)

2	≥	3
1	≥	2
ifrm^#(true,N,add(M,X))	→	rm^#(N,X)	(14)

3	>	2
2	≥	1
ifrm^#(false,N,add(M,X))	→	rm^#(N,X)	(15)

3	>	2
2	≥	1

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

The 3^rd component contains the pair
eq^#(s(X),s(Y)) → eq^#(X,Y) (11)

1.1.3 Size-Change Termination

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

eq^#(s(X),s(Y)) → eq^#(X,Y) (11)

2 > 2

1 > 1

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