Certification Problem

Input (TPDB TRS_Standard/Der95/30)

The rewrite relation of the following TRS is considered.

:(:(:(:(C,x),y),z),u)

→

:(:(x,z),:(:(:(x,y),z),u))

(1)

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,x),y),z),u)	→	:^#(x,y)	(2)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(x,y),z)	(3)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(:(x,y),z),u)	(4)
:^#(:(:(:(C,x),y),z),u)	→	:^#(x,z)	(5)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(x,z),:(:(:(x,y),z),u))	(6)

1.1 Reduction Pair Processor with Usable Rules

Using the

prec(:^#)	=	0		stat(:^#)	=	lex
prec(:)	=	0		stat(:)	=	lex
prec(C)	=	0		stat(C)	=	lex

π(:^#)	=	1
π(:)	=	[1,2]
π(C)	=	[]

together with the usable rule

:(:(:(:(C,x),y),z),u)

→

:(:(x,z),:(:(:(x,y),z),u))

(1)

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

:^#(:(:(:(C,x),y),z),u)	→	:^#(x,y)	(2)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(x,y),z)	(3)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(:(x,y),z),u)	(4)
:^#(:(:(:(C,x),y),z),u)	→	:^#(x,z)	(5)
:^#(:(:(:(C,x),y),z),u)	→	:^#(:(x,z),:(:(:(x,y),z),u))	(6)

could be deleted.

1.1.1 P is empty

There are no pairs anymore.