Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex8_BLR02_C)

The rewrite relation of the following TRS is considered.

active(fib(N))	→	mark(sel(N,fib1(s(0),s(0))))	(1)
active(fib1(X,Y))	→	mark(cons(X,fib1(Y,add(X,Y))))	(2)
active(add(0,X))	→	mark(X)	(3)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(4)
active(sel(0,cons(X,XS)))	→	mark(X)	(5)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(6)
active(fib(X))	→	fib(active(X))	(7)
active(sel(X1,X2))	→	sel(active(X1),X2)	(8)
active(sel(X1,X2))	→	sel(X1,active(X2))	(9)
active(fib1(X1,X2))	→	fib1(active(X1),X2)	(10)
active(fib1(X1,X2))	→	fib1(X1,active(X2))	(11)
active(s(X))	→	s(active(X))	(12)
active(cons(X1,X2))	→	cons(active(X1),X2)	(13)
active(add(X1,X2))	→	add(active(X1),X2)	(14)
active(add(X1,X2))	→	add(X1,active(X2))	(15)
fib(mark(X))	→	mark(fib(X))	(16)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
s(mark(X))	→	mark(s(X))	(21)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
proper(fib(X))	→	fib(proper(X))	(25)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
proper(fib1(X1,X2))	→	fib1(proper(X1),proper(X2))	(27)
proper(s(X))	→	s(proper(X))	(28)
proper(0)	→	ok(0)	(29)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(30)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(31)
fib(ok(X))	→	ok(fib(X))	(32)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
s(ok(X))	→	ok(s(X))	(35)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(37)
top(mark(X))	→	top(proper(X))	(38)
top(ok(X))	→	top(active(X))	(39)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

active^#(fib1(X,Y))	→	fib1^#(Y,add(X,Y))	(40)
proper^#(fib1(X1,X2))	→	proper^#(X2)	(41)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(42)
active^#(fib1(X1,X2))	→	active^#(X1)	(43)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(44)
proper^#(fib1(X1,X2))	→	proper^#(X1)	(45)
proper^#(fib1(X1,X2))	→	fib1^#(proper(X1),proper(X2))	(46)
proper^#(s(X))	→	s^#(proper(X))	(47)
proper^#(sel(X1,X2))	→	sel^#(proper(X1),proper(X2))	(48)
active^#(fib(N))	→	sel^#(N,fib1(s(0),s(0)))	(49)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
active^#(sel(X1,X2))	→	active^#(X1)	(51)
active^#(add(s(X),Y))	→	s^#(add(X,Y))	(52)
proper^#(s(X))	→	proper^#(X)	(53)
top^#(mark(X))	→	top^#(proper(X))	(54)
active^#(add(X1,X2))	→	add^#(X1,active(X2))	(55)
active^#(fib(N))	→	s^#(0)	(56)
fib1^#(ok(X1),ok(X2))	→	fib1^#(X1,X2)	(57)
s^#(mark(X))	→	s^#(X)	(58)
active^#(fib1(X1,X2))	→	fib1^#(X1,active(X2))	(59)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(60)
active^#(sel(X1,X2))	→	sel^#(X1,active(X2))	(61)
active^#(sel(X1,X2))	→	sel^#(active(X1),X2)	(62)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(63)
active^#(add(X1,X2))	→	active^#(X1)	(64)
fib^#(ok(X))	→	fib^#(X)	(65)
active^#(sel(X1,X2))	→	active^#(X2)	(66)
active^#(fib(X))	→	active^#(X)	(67)
active^#(fib(N))	→	s^#(0)	(56)
active^#(fib1(X1,X2))	→	active^#(X2)	(68)
active^#(add(s(X),Y))	→	add^#(X,Y)	(69)
active^#(fib(X))	→	fib^#(active(X))	(70)
fib^#(mark(X))	→	fib^#(X)	(71)
proper^#(sel(X1,X2))	→	proper^#(X2)	(72)
proper^#(cons(X1,X2))	→	proper^#(X1)	(73)
proper^#(add(X1,X2))	→	proper^#(X1)	(74)
top^#(mark(X))	→	proper^#(X)	(75)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(76)
active^#(cons(X1,X2))	→	active^#(X1)	(77)
top^#(ok(X))	→	active^#(X)	(78)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(79)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(80)
proper^#(fib(X))	→	proper^#(X)	(81)
active^#(add(X1,X2))	→	add^#(active(X1),X2)	(82)
active^#(fib1(X1,X2))	→	fib1^#(active(X1),X2)	(83)
proper^#(fib(X))	→	fib^#(proper(X))	(84)
active^#(add(X1,X2))	→	active^#(X2)	(85)
active^#(s(X))	→	s^#(active(X))	(86)
top^#(ok(X))	→	top^#(active(X))	(87)
proper^#(add(X1,X2))	→	add^#(proper(X1),proper(X2))	(88)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(89)
proper^#(cons(X1,X2))	→	proper^#(X2)	(90)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(91)
proper^#(add(X1,X2))	→	proper^#(X2)	(92)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(93)
active^#(fib1(X,Y))	→	add^#(X,Y)	(94)
active^#(fib1(X,Y))	→	cons^#(X,fib1(Y,add(X,Y)))	(95)
active^#(fib(N))	→	fib1^#(s(0),s(0))	(96)
active^#(sel(s(N),cons(X,XS)))	→	sel^#(N,XS)	(97)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(98)
s^#(ok(X))	→	s^#(X)	(99)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(100)
active^#(s(X))	→	active^#(X)	(101)

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(87)
top^#(mark(X))	→	top^#(proper(X))	(54)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	2
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(active)	=	1
π(active^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(fib1^#)	=	0	status(fib1^#)	=	[]	list-extension(fib1^#)	=	Lex
prec(fib1)	=	3	status(fib1)	=	[2, 1]	list-extension(fib1)	=	Lex
prec(fib)	=	5	status(fib)	=	[1]	list-extension(fib)	=	Lex
prec(0)	=	5	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(sel)	=	3	status(sel)	=	[1, 2]	list-extension(sel)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(mark)	=	1	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(cons)	=	2	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(add^#)	=	0	status(add^#)	=	[1, 2]	list-extension(add^#)	=	Lex
prec(add)	=	5	status(add)	=	[1, 2]	list-extension(add)	=	Lex
prec(fib^#)	=	0	status(fib^#)	=	[]	list-extension(fib^#)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[top(x₁)]	=	1
[fib1^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[fib1(x₁, x₂)]	=	max(x₁ + 36413, x₂ + 36413, 0)
[fib(x₁)]	=	x₁ + 43294
[0]	=	1
[sel^#(x₁, x₂)]	=	x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 6879
[s^#(x₁)]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 36413, x₂ + 0, 0)
[add^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[fib^#(x₁)]	=	1

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(4)
active(add(X1,X2))	→	add(X1,active(X2))	(15)
active(sel(X1,X2))	→	sel(active(X1),X2)	(8)
active(fib(N))	→	mark(sel(N,fib1(s(0),s(0))))	(1)
active(add(0,X))	→	mark(X)	(3)
fib(mark(X))	→	mark(fib(X))	(16)
s(mark(X))	→	mark(s(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
proper(fib1(X1,X2))	→	fib1(proper(X1),proper(X2))	(27)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
active(sel(0,cons(X,XS)))	→	mark(X)	(5)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(fib1(X1,X2))	→	fib1(active(X1),X2)	(10)
active(fib(X))	→	fib(active(X))	(7)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(fib(X))	→	fib(proper(X))	(25)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(30)
active(add(X1,X2))	→	add(active(X1),X2)	(14)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(31)
active(s(X))	→	s(active(X))	(12)
add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
active(fib1(X1,X2))	→	fib1(X1,active(X2))	(11)
active(sel(X1,X2))	→	sel(X1,active(X2))	(9)
active(cons(X1,X2))	→	cons(active(X1),X2)	(13)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(6)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(37)
s(ok(X))	→	ok(s(X))	(35)
proper(0)	→	ok(0)	(29)
active(fib1(X,Y))	→	mark(cons(X,fib1(Y,add(X,Y))))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(54)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

top^#(ok(X))

→

top^#(active(X))

(87)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + 0
[proper(x₁)]	=	3
[fib(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(4)
active(add(X1,X2))	→	add(X1,active(X2))	(15)
active(sel(X1,X2))	→	sel(active(X1),X2)	(8)
active(fib(N))	→	mark(sel(N,fib1(s(0),s(0))))	(1)
active(add(0,X))	→	mark(X)	(3)
fib(mark(X))	→	mark(fib(X))	(16)
s(mark(X))	→	mark(s(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
proper(fib1(X1,X2))	→	fib1(proper(X1),proper(X2))	(27)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
active(sel(0,cons(X,XS)))	→	mark(X)	(5)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(fib1(X1,X2))	→	fib1(active(X1),X2)	(10)
active(fib(X))	→	fib(active(X))	(7)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(fib(X))	→	fib(proper(X))	(25)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(30)
active(add(X1,X2))	→	add(active(X1),X2)	(14)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(31)
active(s(X))	→	s(active(X))	(12)
add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
active(fib1(X1,X2))	→	fib1(X1,active(X2))	(11)
active(sel(X1,X2))	→	sel(X1,active(X2))	(9)
active(cons(X1,X2))	→	cons(active(X1),X2)	(13)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(6)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(37)
s(ok(X))	→	ok(s(X))	(35)
proper(0)	→	ok(0)	(29)
active(fib1(X,Y))	→	mark(cons(X,fib1(Y,add(X,Y))))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(87)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

active^#(s(X))	→	active^#(X)	(101)
active^#(fib1(X1,X2))	→	active^#(X2)	(68)
active^#(fib(X))	→	active^#(X)	(67)
active^#(sel(X1,X2))	→	active^#(X2)	(66)
active^#(add(X1,X2))	→	active^#(X1)	(64)
active^#(add(X1,X2))	→	active^#(X2)	(85)
active^#(sel(X1,X2))	→	active^#(X1)	(51)
active^#(cons(X1,X2))	→	active^#(X1)	(77)
active^#(fib1(X1,X2))	→	active^#(X1)	(43)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 11575
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	x₁ + 0
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	621
[0]	=	4447
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[active(x₁)]	=	32044
[cons(x₁, x₂)]	=	x₁ + x₂ + 32042
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
s(mark(X))	→	mark(s(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
proper(fib1(X1,X2))	→	fib1(proper(X1),proper(X2))	(27)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(fib(X))	→	fib(proper(X))	(25)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(30)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(31)
add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(37)
s(ok(X))	→	ok(s(X))	(35)
proper(0)	→	ok(0)	(29)

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

active^#(s(X))	→	active^#(X)	(101)
active^#(fib1(X1,X2))	→	active^#(X2)	(68)
active^#(fib(X))	→	active^#(X)	(67)
active^#(sel(X1,X2))	→	active^#(X2)	(66)
active^#(add(X1,X2))	→	active^#(X1)	(64)
active^#(add(X1,X2))	→	active^#(X2)	(85)
active^#(sel(X1,X2))	→	active^#(X1)	(51)
active^#(cons(X1,X2))	→	active^#(X1)	(77)
active^#(fib1(X1,X2))	→	active^#(X1)	(43)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(cons(X1,X2))	→	proper^#(X1)	(73)
proper^#(sel(X1,X2))	→	proper^#(X2)	(72)
proper^#(add(X1,X2))	→	proper^#(X2)	(92)
proper^#(cons(X1,X2))	→	proper^#(X2)	(90)
proper^#(s(X))	→	proper^#(X)	(53)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
proper^#(fib(X))	→	proper^#(X)	(81)
proper^#(fib1(X1,X2))	→	proper^#(X1)	(45)
proper^#(fib1(X1,X2))	→	proper^#(X2)	(41)
proper^#(add(X1,X2))	→	proper^#(X1)	(74)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	x₁ + 0
[fib(x₁)]	=	x₁ + 12831
[ok(x₁)]	=	1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 3
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
s(mark(X))	→	mark(s(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
proper(fib1(X1,X2))	→	fib1(proper(X1),proper(X2))	(27)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(fib(X))	→	fib(proper(X))	(25)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(30)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(31)
add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(37)
s(ok(X))	→	ok(s(X))	(35)
proper(0)	→	ok(0)	(29)

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

proper^#(cons(X1,X2))	→	proper^#(X1)	(73)
proper^#(sel(X1,X2))	→	proper^#(X2)	(72)
proper^#(add(X1,X2))	→	proper^#(X2)	(92)
proper^#(cons(X1,X2))	→	proper^#(X2)	(90)
proper^#(s(X))	→	proper^#(X)	(53)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
proper^#(fib(X))	→	proper^#(X)	(81)
proper^#(fib1(X1,X2))	→	proper^#(X1)	(45)
proper^#(fib1(X1,X2))	→	proper^#(X2)	(41)
proper^#(add(X1,X2))	→	proper^#(X1)	(74)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

add^#(X1,mark(X2))	→	add^#(X1,X2)	(98)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(93)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(79)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₂ + 0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

add^#(X1,mark(X2))	→	add^#(X1,X2)	(98)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(79)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

add^#(mark(X1),X2)

→

add^#(X1,X2)

(93)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 36457
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	36459
[cons(x₁, x₂)]	=	x₁ + x₂ + 36457
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

add^#(mark(X1),X2)

→

add^#(X1,X2)

(93)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(100)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(76)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	33309
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	42356
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	36459
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

cons^#(ok(X1),ok(X2))

→

cons^#(X1,X2)

(100)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(76)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	42356
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 2
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(76)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

fib^#(mark(X))	→	fib^#(X)	(71)
fib^#(ok(X))	→	fib^#(X)	(65)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 3020
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 2
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	x₁ + 0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

fib^#(mark(X))	→	fib^#(X)	(71)
fib^#(ok(X))	→	fib^#(X)	(65)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

s^#(ok(X))	→	s^#(X)	(99)
s^#(mark(X))	→	s^#(X)	(58)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

s^#(ok(X))	→	s^#(X)	(99)
s^#(mark(X))	→	s^#(X)	(58)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

fib1^#(ok(X1),ok(X2))	→	fib1^#(X1,X2)	(57)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(44)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(42)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	x₂ + 0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

fib1^#(ok(X1),ok(X2))	→	fib1^#(X1,X2)	(57)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(42)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

fib1^#(mark(X1),X2)

→

fib1^#(X1,X2)

(44)

1.1.8.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	x₁ + 0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 2
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

fib1^#(mark(X1),X2)

→

fib1^#(X1,X2)

(44)

could be deleted.

1.1.8.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(91)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(89)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(80)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 34409
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 19098
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 85326
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	85327
[cons(x₁, x₂)]	=	x₁ + x₂ + 50917
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(91)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(80)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(89)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	2
[fib(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	x₂ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 24055
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 20948
[proper^#(x₁)]	=	0
[active(x₁)]	=	45003
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[fib^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
fib(mark(X))	→	mark(fib(X))	(16)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
fib1(mark(X1),X2)	→	mark(fib1(X1,X2))	(19)
fib(ok(X))	→	ok(fib(X))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
fib1(ok(X1),ok(X2))	→	ok(fib1(X1,X2))	(34)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(22)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
fib1(X1,mark(X2))	→	mark(fib1(X1,X2))	(20)
proper(0)	→	ok(0)	(29)

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

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(89)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.