Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/LISTUTILITIES_nosorts_Z)

The rewrite relation of the following TRS is considered.

U11(tt,N,X,XS)	→	U12(splitAt(activate(N),activate(XS)),activate(X))	(1)
U12(pair(YS,ZS),X)	→	pair(cons(activate(X),YS),ZS)	(2)
afterNth(N,XS)	→	snd(splitAt(N,XS))	(3)
and(tt,X)	→	activate(X)	(4)
fst(pair(X,Y))	→	X	(5)
head(cons(N,XS))	→	N	(6)
natsFrom(N)	→	cons(N,n__natsFrom(s(N)))	(7)
sel(N,XS)	→	head(afterNth(N,XS))	(8)
snd(pair(X,Y))	→	Y	(9)
splitAt(0,XS)	→	pair(nil,XS)	(10)
splitAt(s(N),cons(X,XS))	→	U11(tt,N,X,activate(XS))	(11)
tail(cons(N,XS))	→	activate(XS)	(12)
take(N,XS)	→	fst(splitAt(N,XS))	(13)
natsFrom(X)	→	n__natsFrom(X)	(14)
activate(n__natsFrom(X))	→	natsFrom(X)	(15)
activate(X)	→	X	(16)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n²).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

U11^#(tt,z0,z1,z2)

→

c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))

(18)

originates from

U11(tt,z0,z1,z2)

→

U12(splitAt(activate(z0),activate(z2)),activate(z1))

(17)

U12^#(pair(z0,z1),z2)

→

c1(activate^#(z2))

(20)

originates from

U12(pair(z0,z1),z2)

→

pair(cons(activate(z2),z0),z1)

(19)

afterNth^#(z0,z1)

→

c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))

(22)

originates from

afterNth(z0,z1)

→

snd(splitAt(z0,z1))

(21)

and^#(tt,z0)

→

c3(activate^#(z0))

(24)

originates from

and(tt,z0)

→

activate(z0)

(23)

fst^#(pair(z0,z1))

→

(26)

originates from

fst(pair(z0,z1))

→

(25)

head^#(cons(z0,z1))

→

(28)

originates from

head(cons(z0,z1))

→

(27)

natsFrom^#(z0)

→

(30)

originates from

natsFrom(z0)

→

cons(z0,n__natsFrom(s(z0)))

(29)

natsFrom^#(z0)

→

(32)

originates from

natsFrom(z0)

→

n__natsFrom(z0)

(31)

sel^#(z0,z1)

→

c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))

(34)

originates from

sel(z0,z1)

→

head(afterNth(z0,z1))

(33)

snd^#(pair(z0,z1))

→

(36)

originates from

snd(pair(z0,z1))

→

(35)

splitAt^#(0,z0)

→

c10

(38)

originates from

splitAt(0,z0)

→

pair(nil,z0)

(37)

splitAt^#(s(z0),cons(z1,z2))

→

c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))

(40)

originates from

splitAt(s(z0),cons(z1,z2))

→

U11(tt,z0,z1,activate(z2))

(39)

tail^#(cons(z0,z1))

→

c12(activate^#(z1))

(42)

originates from

tail(cons(z0,z1))

→

activate(z1)

(41)

take^#(z0,z1)

→

c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))

(44)

originates from

take(z0,z1)

→

fst(splitAt(z0,z1))

(43)

activate^#(n__natsFrom(z0))

→

c14(natsFrom^#(z0))

(46)

originates from

activate(n__natsFrom(z0))

→

natsFrom(z0)

(45)

activate^#(z0)

→

c15

(48)

originates from

activate(z0)

→

(47)

Moreover, we add the following terms to the innermost strategy.

U11^#(tt,z0,z1,z2)

U12^#(pair(z0,z1),z2)

afterNth^#(z0,z1)

and^#(tt,z0)

fst^#(pair(z0,z1))

head^#(cons(z0,z1))

natsFrom^#(z0)

sel^#(z0,z1)

snd^#(pair(z0,z1))

splitAt^#(0,z0)

splitAt^#(s(z0),cons(z1,z2))

tail^#(cons(z0,z1))

take^#(z0,z1)

activate^#(n__natsFrom(z0))

activate^#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

and(tt,z0)	→	activate(z0)	(23)
fst(pair(z0,z1))	→	z0	(25)
head(cons(z0,z1))	→	z0	(27)
sel(z0,z1)	→	head(afterNth(z0,z1))	(33)
tail(cons(z0,z1))	→	activate(z1)	(41)
take(z0,z1)	→	fst(splitAt(z0,z1))	(43)

1.1.1 Rule Shifting

The rules

and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 · x₁ + 0
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 + 1 · x₁
[U11^#(x₁,...,x₄)]	=	0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	1
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 · x₂ + 0
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

1.1.1.1 Rule Shifting

The rules

snd^#(pair(z0,z1))	→	c9	(36)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	0
[activate(x₁)]	=	0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 + 1 · x₁
[U11^#(x₁,...,x₄)]	=	0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	0
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	1
[splitAt^#(x₁, x₂)]	=	0
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 · x₂ + 0
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

1.1.1.1.1 Rule Shifting

The rules

sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 + 1 · x₁
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 · x₁ + 0
[U11^#(x₁,...,x₄)]	=	0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[tail^#(x₁)]	=	1 + 1 · x₁
[take^#(x₁, x₂)]	=	1
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 · x₁ + 0

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

1.1.1.1.1.1 Rule Shifting

The rules

splitAt^#(0,z0)

→

c10

(38)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 + 1 · x₁
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 · x₁ + 0
[U11^#(x₁,...,x₄)]	=	1 · x₁ + 0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and^#(x₁, x₂)]	=	1 · x₁ + 0
[fst^#(x₁)]	=	0
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	1
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

1.1.1.1.1.1.1 Rule Shifting

The rules

afterNth^#(z0,z1)

→

c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))

(22)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 + 1 · x₁
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 · x₁ + 0
[U11^#(x₁,...,x₄)]	=	0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

splitAt^#(s(z0),cons(z1,z2))

→

c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))

(40)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 + 1 · x₁
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 · x₁ + 0
[U11^#(x₁,...,x₄)]	=	1 · x₂ + 0
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	1
[splitAt^#(x₁, x₂)]	=	1 · x₁ + 0
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1 + 1 · x₁
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)
natsFrom(z0)	→	cons(z0,n__natsFrom(s(z0)))	(29)
activate(n__natsFrom(z0))	→	natsFrom(z0)	(45)
activate(z0)	→	z0	(47)
natsFrom(z0)	→	n__natsFrom(z0)	(31)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

U12^#(pair(z0,z1),z2)

→

c1(activate^#(z2))

(20)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	1 + 1 · x₁
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 + 1 · x₁
[U11(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[afterNth(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd(x₁)]	=	1 · x₁ + 0
[U11^#(x₁,...,x₄)]	=	1 + 1 · x₂
[U12^#(x₁, x₂)]	=	1
[afterNth^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and^#(x₁, x₂)]	=	1 + 1 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[snd^#(x₁)]	=	1
[splitAt^#(x₁, x₂)]	=	1 · x₁ + 0
[tail^#(x₁)]	=	1 · x₁ + 0
[take^#(x₁, x₂)]	=	1 + 1 · x₁
[activate^#(x₁)]	=	0
[0]	=	1
[pair(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	1
[n__natsFrom(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)
natsFrom(z0)	→	cons(z0,n__natsFrom(s(z0)))	(29)
activate(n__natsFrom(z0))	→	natsFrom(z0)	(45)
activate(z0)	→	z0	(47)
natsFrom(z0)	→	n__natsFrom(z0)	(31)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

U11^#(tt,z0,z1,z2)

→

c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))

(18)

are strictly oriented by the following non-linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	0
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	0
[U11(x₁,...,x₄)]	=	1 + 2 · x₁ + 1 · x₂ + 1 · x₃ + 2 · x₁ · x₁ + 1 · x₂ · x₁ + 2 · x₃ · x₁ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[U12(x₁, x₂)]	=	1
[afterNth(x₁, x₂)]	=	0
[snd(x₁)]	=	1
[U11^#(x₁,...,x₄)]	=	1 + 2 · x₁ + 2 · x₂ + 1 · x₁ · x₁ + 1 · x₂ · x₁ + 2 · x₃ · x₁
[U12^#(x₁, x₂)]	=	0
[afterNth^#(x₁, x₂)]	=	2 · x₁ + 0
[and^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[fst^#(x₁)]	=	0
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂ · x₂ + 2 · x₁ · x₁
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	2 · x₁ + 0
[tail^#(x₁)]	=	0
[take^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₂ · x₂ + 2 · x₁ · x₁
[activate^#(x₁)]	=	0
[0]	=	2
[pair(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	1
[s(x₁)]	=	2 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	0
[n__natsFrom(x₁)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)
natsFrom(z0)	→	cons(z0,n__natsFrom(s(z0)))	(29)
activate(n__natsFrom(z0))	→	natsFrom(z0)	(45)
activate(z0)	→	z0	(47)
natsFrom(z0)	→	n__natsFrom(z0)	(31)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	0
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 · x₁ + 0
[U11(x₁,...,x₄)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃
[U12(x₁, x₂)]	=	3
[afterNth(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[snd(x₁)]	=	3
[U11^#(x₁,...,x₄)]	=	2 + 1 · x₁ + 3 · x₂
[U12^#(x₁, x₂)]	=	1
[afterNth^#(x₁, x₂)]	=	1 + 3 · x₁ + 2 · x₂
[and^#(x₁, x₂)]	=	3 + 3 · x₁
[fst^#(x₁)]	=	1
[head^#(x₁)]	=	0
[natsFrom^#(x₁)]	=	0
[sel^#(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	3 · x₁ + 0
[tail^#(x₁)]	=	3 + 3 · x₁
[take^#(x₁, x₂)]	=	1 + 3 · x₁
[activate^#(x₁)]	=	1
[0]	=	3
[pair(x₁, x₂)]	=	1 · x₂ + 0
[nil]	=	3
[s(x₁)]	=	2 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	2
[n__natsFrom(x₁)]	=	1 · x₁ + 0

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)
natsFrom(z0)	→	cons(z0,n__natsFrom(s(z0)))	(29)
activate(n__natsFrom(z0))	→	natsFrom(z0)	(45)
activate(z0)	→	z0	(47)
natsFrom(z0)	→	n__natsFrom(z0)	(31)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10]	=	0
[c11(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[splitAt(x₁, x₂)]	=	2
[activate(x₁)]	=	1 · x₁ + 0
[natsFrom(x₁)]	=	1 · x₁ + 0
[U11(x₁,...,x₄)]	=	1 · x₁ + 0
[U12(x₁, x₂)]	=	2
[afterNth(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[snd(x₁)]	=	3
[U11^#(x₁,...,x₄)]	=	2 + 3 · x₁ + 3 · x₂
[U12^#(x₁, x₂)]	=	2 · x₁ + 0
[afterNth^#(x₁, x₂)]	=	3 · x₁ + 0 + 2 · x₂
[and^#(x₁, x₂)]	=	3 + 3 · x₁
[fst^#(x₁)]	=	3
[head^#(x₁)]	=	2
[natsFrom^#(x₁)]	=	1
[sel^#(x₁, x₂)]	=	2 + 3 · x₁ + 2 · x₂
[snd^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	3 · x₁ + 0
[tail^#(x₁)]	=	3 + 3 · x₁
[take^#(x₁, x₂)]	=	3 + 3 · x₁
[activate^#(x₁)]	=	1
[0]	=	3
[pair(x₁, x₂)]	=	1
[nil]	=	3
[s(x₁)]	=	3 + 1 · x₁
[cons(x₁, x₂)]	=	0
[tt]	=	2
[n__natsFrom(x₁)]	=	1 · x₁ + 0

which has the intended complexity. Here, only the following usable rules have been considered:

U11^#(tt,z0,z1,z2)	→	c(U12^#(splitAt(activate(z0),activate(z2)),activate(z1)),splitAt^#(activate(z0),activate(z2)),activate^#(z0),activate^#(z2),activate^#(z1))	(18)
U12^#(pair(z0,z1),z2)	→	c1(activate^#(z2))	(20)
afterNth^#(z0,z1)	→	c2(snd^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(22)
and^#(tt,z0)	→	c3(activate^#(z0))	(24)
fst^#(pair(z0,z1))	→	c4	(26)
head^#(cons(z0,z1))	→	c5	(28)
natsFrom^#(z0)	→	c6	(30)
natsFrom^#(z0)	→	c7	(32)
sel^#(z0,z1)	→	c8(head^#(afterNth(z0,z1)),afterNth^#(z0,z1))	(34)
snd^#(pair(z0,z1))	→	c9	(36)
splitAt^#(0,z0)	→	c10	(38)
splitAt^#(s(z0),cons(z1,z2))	→	c11(U11^#(tt,z0,z1,activate(z2)),activate^#(z2))	(40)
tail^#(cons(z0,z1))	→	c12(activate^#(z1))	(42)
take^#(z0,z1)	→	c13(fst^#(splitAt(z0,z1)),splitAt^#(z0,z1))	(44)
activate^#(n__natsFrom(z0))	→	c14(natsFrom^#(z0))	(46)
activate^#(z0)	→	c15	(48)
U11(tt,z0,z1,z2)	→	U12(splitAt(activate(z0),activate(z2)),activate(z1))	(17)
natsFrom(z0)	→	cons(z0,n__natsFrom(s(z0)))	(29)
splitAt(0,z0)	→	pair(nil,z0)	(37)
activate(n__natsFrom(z0))	→	natsFrom(z0)	(45)
splitAt(s(z0),cons(z1,z2))	→	U11(tt,z0,z1,activate(z2))	(39)
U12(pair(z0,z1),z2)	→	pair(cons(activate(z2),z0),z1)	(19)
activate(z0)	→	z0	(47)
natsFrom(z0)	→	n__natsFrom(z0)	(31)

1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).