Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex8_BLR02_iGM)

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)
mark(fib(X))	→	active(fib(mark(X)))	(7)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(8)
mark(fib1(X1,X2))	→	active(fib1(mark(X1),mark(X2)))	(9)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(0)	→	active(0)	(11)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
mark(add(X1,X2))	→	active(add(mark(X1),mark(X2)))	(13)
fib(mark(X))	→	fib(X)	(14)
fib(active(X))	→	fib(X)	(15)
sel(mark(X1),X2)	→	sel(X1,X2)	(16)
sel(X1,mark(X2))	→	sel(X1,X2)	(17)
sel(active(X1),X2)	→	sel(X1,X2)	(18)
sel(X1,active(X2))	→	sel(X1,X2)	(19)
fib1(mark(X1),X2)	→	fib1(X1,X2)	(20)
fib1(X1,mark(X2))	→	fib1(X1,X2)	(21)
fib1(active(X1),X2)	→	fib1(X1,X2)	(22)
fib1(X1,active(X2))	→	fib1(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
s(active(X))	→	s(X)	(25)
cons(mark(X1),X2)	→	cons(X1,X2)	(26)
cons(X1,mark(X2))	→	cons(X1,X2)	(27)
cons(active(X1),X2)	→	cons(X1,X2)	(28)
cons(X1,active(X2))	→	cons(X1,X2)	(29)
add(mark(X1),X2)	→	add(X1,X2)	(30)
add(X1,mark(X2))	→	add(X1,X2)	(31)
add(active(X1),X2)	→	add(X1,X2)	(32)
add(X1,active(X2))	→	add(X1,X2)	(33)

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))	→	cons^#(X,fib1(Y,add(X,Y)))	(34)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(35)
mark^#(fib(X))	→	mark^#(X)	(36)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(37)
active^#(fib(N))	→	sel^#(N,fib1(s(0),s(0)))	(38)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(39)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(40)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(41)
active^#(fib(N))	→	fib1^#(s(0),s(0))	(42)
mark^#(sel(X1,X2))	→	mark^#(X2)	(43)
active^#(fib(N))	→	s^#(0)	(44)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(45)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(49)
mark^#(sel(X1,X2))	→	sel^#(mark(X1),mark(X2))	(50)
mark^#(fib1(X1,X2))	→	fib1^#(mark(X1),mark(X2))	(51)
mark^#(add(X1,X2))	→	add^#(mark(X1),mark(X2))	(52)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
active^#(add(s(X),Y))	→	add^#(X,Y)	(54)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(55)
fib^#(mark(X))	→	fib^#(X)	(56)
active^#(fib(N))	→	mark^#(sel(N,fib1(s(0),s(0))))	(57)
mark^#(fib1(X1,X2))	→	active^#(fib1(mark(X1),mark(X2)))	(58)
mark^#(s(X))	→	s^#(mark(X))	(59)
active^#(add(s(X),Y))	→	s^#(add(X,Y))	(60)
mark^#(fib1(X1,X2))	→	mark^#(X1)	(61)
mark^#(s(X))	→	active^#(s(mark(X)))	(62)
mark^#(sel(X1,X2))	→	mark^#(X1)	(63)
active^#(fib(N))	→	s^#(0)	(44)
s^#(active(X))	→	s^#(X)	(64)
mark^#(cons(X1,X2))	→	cons^#(mark(X1),X2)	(65)
active^#(sel(s(N),cons(X,XS)))	→	sel^#(N,XS)	(66)
add^#(active(X1),X2)	→	add^#(X1,X2)	(67)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
add^#(X1,active(X2))	→	add^#(X1,X2)	(69)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(70)
active^#(add(0,X))	→	mark^#(X)	(71)
mark^#(fib(X))	→	fib^#(mark(X))	(72)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(73)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(74)
mark^#(fib(X))	→	active^#(fib(mark(X)))	(75)
s^#(mark(X))	→	s^#(X)	(76)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(78)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(79)
fib1^#(active(X1),X2)	→	fib1^#(X1,X2)	(80)
mark^#(cons(X1,X2))	→	mark^#(X1)	(81)
mark^#(0)	→	active^#(0)	(82)
active^#(fib1(X,Y))	→	fib1^#(Y,add(X,Y))	(83)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)
fib^#(active(X))	→	fib^#(X)	(85)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(86)
mark^#(fib1(X1,X2))	→	mark^#(X2)	(87)
active^#(fib1(X,Y))	→	add^#(X,Y)	(88)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(89)
fib1^#(X1,active(X2))	→	fib1^#(X1,X2)	(90)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(89)
mark^#(sel(X1,X2))	→	mark^#(X1)	(63)
mark^#(s(X))	→	active^#(s(mark(X)))	(62)
mark^#(fib1(X1,X2))	→	mark^#(X1)	(61)
mark^#(fib1(X1,X2))	→	mark^#(X2)	(87)
mark^#(fib1(X1,X2))	→	active^#(fib1(mark(X1),mark(X2)))	(58)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(86)
active^#(fib(N))	→	mark^#(sel(N,fib1(s(0),s(0))))	(57)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)
mark^#(cons(X1,X2))	→	mark^#(X1)	(81)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(78)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
mark^#(fib(X))	→	active^#(fib(mark(X)))	(75)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(74)
mark^#(sel(X1,X2))	→	mark^#(X2)	(43)
active^#(add(0,X))	→	mark^#(X)	(71)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
mark^#(fib(X))	→	mark^#(X)	(36)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	46917
[fib(x₁)]	=	46917
[mark^#(x₁)]	=	46917
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	46917
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[active(x₁)]	=	2
[cons(x₁, x₂)]	=	36466
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	46917
[fib^#(x₁)]	=	0

together with the usable rules

sel(active(X1),X2)	→	sel(X1,X2)	(18)
fib(active(X))	→	fib(X)	(15)
sel(mark(X1),X2)	→	sel(X1,X2)	(16)
fib1(X1,mark(X2))	→	fib1(X1,X2)	(21)
cons(mark(X1),X2)	→	cons(X1,X2)	(26)
sel(X1,active(X2))	→	sel(X1,X2)	(19)
add(active(X1),X2)	→	add(X1,X2)	(32)
sel(X1,mark(X2))	→	sel(X1,X2)	(17)
cons(X1,mark(X2))	→	cons(X1,X2)	(27)
fib1(active(X1),X2)	→	fib1(X1,X2)	(22)
cons(active(X1),X2)	→	cons(X1,X2)	(28)
add(X1,active(X2))	→	add(X1,X2)	(33)
fib1(mark(X1),X2)	→	fib1(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
add(mark(X1),X2)	→	add(X1,X2)	(30)
fib(mark(X))	→	fib(X)	(14)
add(X1,mark(X2))	→	add(X1,X2)	(31)
fib1(X1,active(X2))	→	fib1(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
cons(X1,active(X2))	→	cons(X1,X2)	(29)

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

mark^#(s(X))	→	active^#(s(mark(X)))	(62)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(78)

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

active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
mark^#(sel(X1,X2))	→	mark^#(X2)	(43)
mark^#(sel(X1,X2))	→	mark^#(X1)	(63)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(89)
active^#(fib(N))	→	mark^#(sel(N,fib1(s(0),s(0))))	(57)
active^#(add(0,X))	→	mark^#(X)	(71)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(74)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(fib(X))	→	mark^#(X)	(36)
mark^#(fib(X))	→	active^#(fib(mark(X)))	(75)
mark^#(cons(X1,X2))	→	mark^#(X1)	(81)
mark^#(fib1(X1,X2))	→	mark^#(X2)	(87)
mark^#(fib1(X1,X2))	→	mark^#(X1)	(61)
mark^#(fib1(X1,X2))	→	active^#(fib1(mark(X1),mark(X2)))	(58)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(86)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[fib1^#(x₁, x₂)]	=	max(0)
[fib1(x₁, x₂)]	=	max(x₁ + 8946, x₂ + 8946, 0)
[fib(x₁)]	=	x₁ + 38231
[mark^#(x₁)]	=	x₁ + 0
[0]	=	26286
[sel^#(x₁, x₂)]	=	max(0)
[sel(x₁, x₂)]	=	max(x₁ + 11945, x₂ + 2998, 0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 8946, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	max(0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[fib^#(x₁)]	=	0

together with the usable rules

sel(active(X1),X2)	→	sel(X1,X2)	(18)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(4)
fib(active(X))	→	fib(X)	(15)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(8)
active(fib(N))	→	mark(sel(N,fib1(s(0),s(0))))	(1)
active(add(0,X))	→	mark(X)	(3)
sel(mark(X1),X2)	→	sel(X1,X2)	(16)
fib1(X1,mark(X2))	→	fib1(X1,X2)	(21)
cons(mark(X1),X2)	→	cons(X1,X2)	(26)
sel(X1,active(X2))	→	sel(X1,X2)	(19)
add(active(X1),X2)	→	add(X1,X2)	(32)
sel(X1,mark(X2))	→	sel(X1,X2)	(17)
cons(X1,mark(X2))	→	cons(X1,X2)	(27)
fib1(active(X1),X2)	→	fib1(X1,X2)	(22)
cons(active(X1),X2)	→	cons(X1,X2)	(28)
active(sel(0,cons(X,XS)))	→	mark(X)	(5)
add(X1,active(X2))	→	add(X1,X2)	(33)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(fib(X))	→	active(fib(mark(X)))	(7)
fib1(mark(X1),X2)	→	fib1(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
add(mark(X1),X2)	→	add(X1,X2)	(30)
fib(mark(X))	→	fib(X)	(14)
add(X1,mark(X2))	→	add(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
fib1(X1,active(X2))	→	fib1(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
mark(0)	→	active(0)	(11)
mark(fib1(X1,X2))	→	active(fib1(mark(X1),mark(X2)))	(9)
mark(add(X1,X2))	→	active(add(mark(X1),mark(X2)))	(13)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(6)
cons(X1,active(X2))	→	cons(X1,X2)	(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 pairs

mark^#(sel(X1,X2))	→	mark^#(X2)	(43)
mark^#(sel(X1,X2))	→	mark^#(X1)	(63)
active^#(fib(N))	→	mark^#(sel(N,fib1(s(0),s(0))))	(57)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(74)
mark^#(fib(X))	→	mark^#(X)	(36)
mark^#(cons(X1,X2))	→	mark^#(X1)	(81)
mark^#(fib1(X1,X2))	→	mark^#(X2)	(87)
mark^#(fib1(X1,X2))	→	mark^#(X1)	(61)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(89)
active^#(add(0,X))	→	mark^#(X)	(71)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(fib(X))	→	active^#(fib(mark(X)))	(75)
mark^#(fib1(X1,X2))	→	active^#(fib1(mark(X1),mark(X2)))	(58)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(86)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	31114
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	3
[fib(x₁)]	=	1
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	3
[s^#(x₁)]	=	0
[mark(x₁)]	=	2
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	36466
[active^#(x₁)]	=	x₁ + 46914
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	3
[fib^#(x₁)]	=	0

together with the usable rules

sel(active(X1),X2)	→	sel(X1,X2)	(18)
fib(active(X))	→	fib(X)	(15)
sel(mark(X1),X2)	→	sel(X1,X2)	(16)
fib1(X1,mark(X2))	→	fib1(X1,X2)	(21)
cons(mark(X1),X2)	→	cons(X1,X2)	(26)
sel(X1,active(X2))	→	sel(X1,X2)	(19)
add(active(X1),X2)	→	add(X1,X2)	(32)
sel(X1,mark(X2))	→	sel(X1,X2)	(17)
cons(X1,mark(X2))	→	cons(X1,X2)	(27)
fib1(active(X1),X2)	→	fib1(X1,X2)	(22)
cons(active(X1),X2)	→	cons(X1,X2)	(28)
add(X1,active(X2))	→	add(X1,X2)	(33)
fib1(mark(X1),X2)	→	fib1(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
add(mark(X1),X2)	→	add(X1,X2)	(30)
fib(mark(X))	→	fib(X)	(14)
add(X1,mark(X2))	→	add(X1,X2)	(31)
fib1(X1,active(X2))	→	fib1(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
cons(X1,active(X2))	→	cons(X1,X2)	(29)

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

mark^#(fib(X))

→

active^#(fib(mark(X)))

(75)

could be deleted.

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

active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(89)
active^#(add(0,X))	→	mark^#(X)	(71)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(fib1(X1,X2))	→	active^#(fib1(mark(X1),mark(X2)))	(58)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(86)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(s^#)	=	1
π(mark)	=	1
π(active)	=	1

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

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

and the following Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[s(x₁)]	=	x₁ + 0
[fib1^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[fib1(x₁, x₂)]	=	max(x₁ + 19791, x₂ + 19791, 0)
[fib(x₁)]	=	x₁ + 87762
[mark^#(x₁)]	=	x₁ + 0
[0]	=	48178
[sel^#(x₁, x₂)]	=	x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 19792
[cons(x₁, x₂)]	=	max(x₁ + 19791, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 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(active(X1),X2)	→	sel(X1,X2)	(18)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(4)
fib(active(X))	→	fib(X)	(15)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(8)
active(fib(N))	→	mark(sel(N,fib1(s(0),s(0))))	(1)
active(add(0,X))	→	mark(X)	(3)
sel(mark(X1),X2)	→	sel(X1,X2)	(16)
fib1(X1,mark(X2))	→	fib1(X1,X2)	(21)
cons(mark(X1),X2)	→	cons(X1,X2)	(26)
sel(X1,active(X2))	→	sel(X1,X2)	(19)
add(active(X1),X2)	→	add(X1,X2)	(32)
sel(X1,mark(X2))	→	sel(X1,X2)	(17)
cons(X1,mark(X2))	→	cons(X1,X2)	(27)
fib1(active(X1),X2)	→	fib1(X1,X2)	(22)
cons(active(X1),X2)	→	cons(X1,X2)	(28)
active(sel(0,cons(X,XS)))	→	mark(X)	(5)
add(X1,active(X2))	→	add(X1,X2)	(33)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(fib(X))	→	active(fib(mark(X)))	(7)
fib1(mark(X1),X2)	→	fib1(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
add(mark(X1),X2)	→	add(X1,X2)	(30)
fib(mark(X))	→	fib(X)	(14)
add(X1,mark(X2))	→	add(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
fib1(X1,active(X2))	→	fib1(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
mark(0)	→	active(0)	(11)
mark(fib1(X1,X2))	→	active(fib1(mark(X1),mark(X2)))	(9)
mark(add(X1,X2))	→	active(add(mark(X1),mark(X2)))	(13)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(6)
cons(X1,active(X2))	→	cons(X1,X2)	(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 pairs

active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(48)
active^#(add(0,X))	→	mark^#(X)	(71)
mark^#(s(X))	→	mark^#(X)	(77)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(add(X1,X2))	→	mark^#(X1)	(68)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(47)
active^#(fib1(X,Y))	→	mark^#(cons(X,fib1(Y,add(X,Y))))	(84)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

fib1^#(X1,active(X2))	→	fib1^#(X1,X2)	(90)
fib1^#(active(X1),X2)	→	fib1^#(X1,X2)	(80)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(79)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(39)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

fib1^#(X1,active(X2))	→	fib1^#(X1,X2)	(90)
fib1^#(X1,mark(X2))	→	fib1^#(X1,X2)	(39)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

fib1^#(active(X1),X2)	→	fib1^#(X1,X2)	(80)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(79)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	6993
[fib1^#(x₁, x₂)]	=	x₁ + 0
[fib1(x₁, x₂)]	=	3024
[fib(x₁)]	=	x₁ + 52442
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	52444
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	3265
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	6991
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

fib1^#(active(X1),X2)	→	fib1^#(X1,X2)	(80)
fib1^#(mark(X1),X2)	→	fib1^#(X1,X2)	(79)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

fib^#(active(X))	→	fib^#(X)	(85)
fib^#(mark(X))	→	fib^#(X)	(56)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	12201
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	13962
[fib(x₁)]	=	x₁ + 46517
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	46519
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 21394
[active(x₁)]	=	x₁ + 21395
[cons(x₁, x₂)]	=	29984
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	12199
[fib^#(x₁)]	=	x₁ + 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

fib^#(active(X))	→	fib^#(X)	(85)
fib^#(mark(X))	→	fib^#(X)	(56)

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

s^#(active(X))	→	s^#(X)	(64)
s^#(mark(X))	→	s^#(X)	(76)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	43488
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	15620
[fib(x₁)]	=	x₁ + 36467
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	36469
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 21394
[active(x₁)]	=	x₁ + 21395
[cons(x₁, x₂)]	=	39789
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	43486
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

s^#(active(X))	→	s^#(X)	(64)
s^#(mark(X))	→	s^#(X)	(76)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

add^#(mark(X1),X2)	→	add^#(X1,X2)	(55)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(73)
add^#(X1,active(X2))	→	add^#(X1,X2)	(69)
add^#(active(X1),X2)	→	add^#(X1,X2)	(67)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	26053
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	35955
[fib(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	122
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 21394
[active(x₁)]	=	x₁ + 21395
[cons(x₁, x₂)]	=	54704
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	x₂ + 0
[add(x₁, x₂)]	=	1
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

add^#(X1,mark(X2))	→	add^#(X1,X2)	(73)
add^#(X1,active(X2))	→	add^#(X1,X2)	(69)

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

add^#(active(X1),X2)	→	add^#(X1,X2)	(67)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(55)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	59833
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	29161
[fib(x₁)]	=	x₁ + 43802
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	76385
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 21394
[active(x₁)]	=	x₁ + 53976
[cons(x₁, x₂)]	=	61744
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	27250
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

add^#(active(X1),X2)	→	add^#(X1,X2)	(67)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(55)

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

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(49)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(45)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(35)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	29299
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	1
[fib(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 0
[sel(x₁, x₂)]	=	32583
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	30810
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	29297
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(49)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(45)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(35)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(70)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(41)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(40)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(37)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	9050
[fib1^#(x₁, x₂)]	=	0
[fib1(x₁, x₂)]	=	1
[fib(x₁)]	=	x₁ + 29344
[mark^#(x₁)]	=	46917
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	29346
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 23641
[active(x₁)]	=	x₁ + 23642
[cons(x₁, x₂)]	=	1065
[active^#(x₁)]	=	46917
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	1
[fib^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(70)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(41)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(40)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(37)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.