Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nosorts-noand_Z)

The rewrite relation of the following TRS is considered.

U11(tt,N,XS)	→	U12(tt,activate(N),activate(XS))	(1)
U12(tt,N,XS)	→	snd(splitAt(activate(N),activate(XS)))	(2)
U21(tt,X)	→	U22(tt,activate(X))	(3)
U22(tt,X)	→	activate(X)	(4)
U31(tt,N)	→	U32(tt,activate(N))	(5)
U32(tt,N)	→	activate(N)	(6)
U41(tt,N,XS)	→	U42(tt,activate(N),activate(XS))	(7)
U42(tt,N,XS)	→	head(afterNth(activate(N),activate(XS)))	(8)
U51(tt,Y)	→	U52(tt,activate(Y))	(9)
U52(tt,Y)	→	activate(Y)	(10)
U61(tt,N,X,XS)	→	U62(tt,activate(N),activate(X),activate(XS))	(11)
U62(tt,N,X,XS)	→	U63(tt,activate(N),activate(X),activate(XS))	(12)
U63(tt,N,X,XS)	→	U64(splitAt(activate(N),activate(XS)),activate(X))	(13)
U64(pair(YS,ZS),X)	→	pair(cons(activate(X),YS),ZS)	(14)
U71(tt,XS)	→	U72(tt,activate(XS))	(15)
U72(tt,XS)	→	activate(XS)	(16)
U81(tt,N,XS)	→	U82(tt,activate(N),activate(XS))	(17)
U82(tt,N,XS)	→	fst(splitAt(activate(N),activate(XS)))	(18)
afterNth(N,XS)	→	U11(tt,N,XS)	(19)
fst(pair(X,Y))	→	U21(tt,X)	(20)
head(cons(N,XS))	→	U31(tt,N)	(21)
natsFrom(N)	→	cons(N,n__natsFrom(s(N)))	(22)
sel(N,XS)	→	U41(tt,N,XS)	(23)
snd(pair(X,Y))	→	U51(tt,Y)	(24)
splitAt(0,XS)	→	pair(nil,XS)	(25)
splitAt(s(N),cons(X,XS))	→	U61(tt,N,X,activate(XS))	(26)
tail(cons(N,XS))	→	U71(tt,activate(XS))	(27)
take(N,XS)	→	U81(tt,N,XS)	(28)
natsFrom(X)	→	n__natsFrom(X)	(29)
activate(n__natsFrom(X))	→	natsFrom(X)	(30)
activate(X)	→	X	(31)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

U11^#(tt,N,XS)	→	U12^#(tt,activate(N),activate(XS))	(32)
U11^#(tt,N,XS)	→	activate^#(N)	(33)
U11^#(tt,N,XS)	→	activate^#(XS)	(34)
U12^#(tt,N,XS)	→	snd^#(splitAt(activate(N),activate(XS)))	(35)
U12^#(tt,N,XS)	→	splitAt^#(activate(N),activate(XS))	(36)
U12^#(tt,N,XS)	→	activate^#(N)	(37)
U12^#(tt,N,XS)	→	activate^#(XS)	(38)
U21^#(tt,X)	→	U22^#(tt,activate(X))	(39)
U21^#(tt,X)	→	activate^#(X)	(40)
U22^#(tt,X)	→	activate^#(X)	(41)
U31^#(tt,N)	→	U32^#(tt,activate(N))	(42)
U31^#(tt,N)	→	activate^#(N)	(43)
U32^#(tt,N)	→	activate^#(N)	(44)
U41^#(tt,N,XS)	→	U42^#(tt,activate(N),activate(XS))	(45)
U41^#(tt,N,XS)	→	activate^#(N)	(46)
U41^#(tt,N,XS)	→	activate^#(XS)	(47)
U42^#(tt,N,XS)	→	head^#(afterNth(activate(N),activate(XS)))	(48)
U42^#(tt,N,XS)	→	afterNth^#(activate(N),activate(XS))	(49)
U42^#(tt,N,XS)	→	activate^#(N)	(50)
U42^#(tt,N,XS)	→	activate^#(XS)	(51)
U51^#(tt,Y)	→	U52^#(tt,activate(Y))	(52)
U51^#(tt,Y)	→	activate^#(Y)	(53)
U52^#(tt,Y)	→	activate^#(Y)	(54)
U61^#(tt,N,X,XS)	→	U62^#(tt,activate(N),activate(X),activate(XS))	(55)
U61^#(tt,N,X,XS)	→	activate^#(N)	(56)
U61^#(tt,N,X,XS)	→	activate^#(X)	(57)
U61^#(tt,N,X,XS)	→	activate^#(XS)	(58)
U62^#(tt,N,X,XS)	→	U63^#(tt,activate(N),activate(X),activate(XS))	(59)
U62^#(tt,N,X,XS)	→	activate^#(N)	(60)
U62^#(tt,N,X,XS)	→	activate^#(X)	(61)
U62^#(tt,N,X,XS)	→	activate^#(XS)	(62)
U63^#(tt,N,X,XS)	→	U64^#(splitAt(activate(N),activate(XS)),activate(X))	(63)
U63^#(tt,N,X,XS)	→	splitAt^#(activate(N),activate(XS))	(64)
U63^#(tt,N,X,XS)	→	activate^#(N)	(65)
U63^#(tt,N,X,XS)	→	activate^#(XS)	(66)
U63^#(tt,N,X,XS)	→	activate^#(X)	(67)
U64^#(pair(YS,ZS),X)	→	activate^#(X)	(68)
U71^#(tt,XS)	→	U72^#(tt,activate(XS))	(69)
U71^#(tt,XS)	→	activate^#(XS)	(70)
U72^#(tt,XS)	→	activate^#(XS)	(71)
U81^#(tt,N,XS)	→	U82^#(tt,activate(N),activate(XS))	(72)
U81^#(tt,N,XS)	→	activate^#(N)	(73)
U81^#(tt,N,XS)	→	activate^#(XS)	(74)
U82^#(tt,N,XS)	→	fst^#(splitAt(activate(N),activate(XS)))	(75)
U82^#(tt,N,XS)	→	splitAt^#(activate(N),activate(XS))	(76)
U82^#(tt,N,XS)	→	activate^#(N)	(77)
U82^#(tt,N,XS)	→	activate^#(XS)	(78)
afterNth^#(N,XS)	→	U11^#(tt,N,XS)	(79)
fst^#(pair(X,Y))	→	U21^#(tt,X)	(80)
head^#(cons(N,XS))	→	U31^#(tt,N)	(81)
sel^#(N,XS)	→	U41^#(tt,N,XS)	(82)
snd^#(pair(X,Y))	→	U51^#(tt,Y)	(83)
splitAt^#(s(N),cons(X,XS))	→	U61^#(tt,N,X,activate(XS))	(84)
splitAt^#(s(N),cons(X,XS))	→	activate^#(XS)	(85)
tail^#(cons(N,XS))	→	U71^#(tt,activate(XS))	(86)
tail^#(cons(N,XS))	→	activate^#(XS)	(87)
take^#(N,XS)	→	U81^#(tt,N,XS)	(88)
activate^#(n__natsFrom(X))	→	natsFrom^#(X)	(89)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U62^#(tt,N,X,XS)	→	U63^#(tt,activate(N),activate(X),activate(XS))	(59)
U63^#(tt,N,X,XS)	→	splitAt^#(activate(N),activate(XS))	(64)
splitAt^#(s(N),cons(X,XS))	→	U61^#(tt,N,X,activate(XS))	(84)
U61^#(tt,N,X,XS)	→	U62^#(tt,activate(N),activate(X),activate(XS))	(55)

1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 1 to get the following set of pairs

U63^#(tt,n__natsFrom(x0),y1,y2)	→	splitAt^#(natsFrom(x0),activate(y2))	(90)
U63^#(tt,x0,y1,y2)	→	splitAt^#(x0,activate(y2))	(91)

1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 1 to get the following set of pairs

U63^#(tt,n__natsFrom(x0),y1,y2)	→	splitAt^#(cons(x0,n__natsFrom(s(x0))),activate(y2))	(92)
U63^#(tt,n__natsFrom(x0),y1,y2)	→	splitAt^#(n__natsFrom(x0),activate(y2))	(93)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U63^#(tt,x0,y1,y2)	→	splitAt^#(x0,activate(y2))	(91)
splitAt^#(s(N),cons(X,XS))	→	U61^#(tt,N,X,activate(XS))	(84)
U61^#(tt,N,X,XS)	→	U62^#(tt,activate(N),activate(X),activate(XS))	(55)
U62^#(tt,N,X,XS)	→	U63^#(tt,activate(N),activate(X),activate(XS))	(59)

1.1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 2 to get the following set of pairs

U63^#(tt,y0,y1,n__natsFrom(x0))	→	splitAt^#(y0,natsFrom(x0))	(94)
U63^#(tt,y0,y1,x0)	→	splitAt^#(y0,x0)	(95)

1.1.1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 2 to get the following set of pairs

U63^#(tt,y0,y1,n__natsFrom(x0))	→	splitAt^#(y0,cons(x0,n__natsFrom(s(x0))))	(96)
U63^#(tt,y0,y1,n__natsFrom(x0))	→	splitAt^#(y0,n__natsFrom(x0))	(97)

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U61^#(tt,N,X,XS)	→	U62^#(tt,activate(N),activate(X),activate(XS))	(55)
U62^#(tt,N,X,XS)	→	U63^#(tt,activate(N),activate(X),activate(XS))	(59)
U63^#(tt,y0,y1,x0)	→	splitAt^#(y0,x0)	(95)
splitAt^#(s(N),cons(X,XS))	→	U61^#(tt,N,X,activate(XS))	(84)
U63^#(tt,y0,y1,n__natsFrom(x0))	→	splitAt^#(y0,cons(x0,n__natsFrom(s(x0))))	(96)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U61^#(x₁,...,x₄)]	=	2 + 2 · x₁ + x₂
[U62^#(x₁,...,x₄)]	=	2 + 2 · x₁ + x₂
[U63^#(x₁,...,x₄)]	=	1 + 2 · x₁ + x₂
[activate(x₁)]	=	x₁
[n__natsFrom(x₁)]	=	-2
[natsFrom(x₁)]	=	0
[cons(x₁, x₂)]	=	-2
[s(x₁)]	=	1 + x₁
[tt]	=	0
[splitAt^#(x₁, x₂)]	=	1 + x₁

together with the usable rules

activate(n__natsFrom(X))	→	natsFrom(X)	(30)
activate(X)	→	X	(31)
natsFrom(N)	→	cons(N,n__natsFrom(s(N)))	(22)
natsFrom(X)	→	n__natsFrom(X)	(29)

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

U62^#(tt,N,X,XS)

→

U63^#(tt,activate(N),activate(X),activate(XS))

(59)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.