Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_Luc03b_C)

The rewrite relation of the following TRS is considered.

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

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

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

The 1^st component contains the pair

top^#(mark(X))	→	top^#(proper(X))	(59)
top^#(ok(X))	→	top^#(active(X))	(50)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	11650
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₁ + x₂ + 43209
[top^#(x₁)]	=	x₁ + 0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 0
[0]	=	5876
[from(x₁)]	=	x₁ + 41055
[s^#(x₁)]	=	0
[nil]	=	32018
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 41054
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 12280
[len(x₁)]	=	x₁ + 1

together with the usable rules

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

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

top^#(mark(X))

→

top^#(proper(X))

(59)

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))

(50)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₁ + 1
[top^#(x₁)]	=	x₁ + 0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 27377
[ok(x₁)]	=	x₁ + 27377
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	32018
[mark(x₁)]	=	1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

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

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

top^#(ok(X))

→

top^#(active(X))

(50)

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

proper^#(len(X))	→	proper^#(X)	(90)
proper^#(s(X))	→	proper^#(X)	(89)
proper^#(cons(X1,X2))	→	proper^#(X1)	(58)
proper^#(cons(X1,X2))	→	proper^#(X2)	(57)
proper^#(from(X))	→	proper^#(X)	(49)
proper^#(add(X1,X2))	→	proper^#(X1)	(76)
proper^#(fst(X1,X2))	→	proper^#(X2)	(73)
proper^#(add(X1,X2))	→	proper^#(X2)	(41)
proper^#(fst(X1,X2))	→	proper^#(X1)	(39)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	x₁ + 0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	1
[0]	=	1
[from(x₁)]	=	x₁ + 11575
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	625
[proper^#(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 21027
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[len(x₁)]	=	x₁ + 1

together with the usable rules

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

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

proper^#(len(X))	→	proper^#(X)	(90)
proper^#(s(X))	→	proper^#(X)	(89)
proper^#(cons(X1,X2))	→	proper^#(X1)	(58)
proper^#(cons(X1,X2))	→	proper^#(X2)	(57)
proper^#(from(X))	→	proper^#(X)	(49)
proper^#(add(X1,X2))	→	proper^#(X1)	(76)
proper^#(fst(X1,X2))	→	proper^#(X2)	(73)
proper^#(add(X1,X2))	→	proper^#(X2)	(41)
proper^#(fst(X1,X2))	→	proper^#(X1)	(39)

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

active^#(fst(X1,X2))	→	active^#(X1)	(56)
active^#(add(X1,X2))	→	active^#(X2)	(55)
active^#(from(X))	→	active^#(X)	(54)
active^#(add(X1,X2))	→	active^#(X1)	(78)
active^#(cons(X1,X2))	→	active^#(X1)	(47)
active^#(fst(X1,X2))	→	active^#(X2)	(40)
active^#(len(X))	→	active^#(X)	(67)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	x₁ + 0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	1
[0]	=	1
[from(x₁)]	=	x₁ + 11575
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[len(x₁)]	=	x₁ + 12063

together with the usable rules

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

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

active^#(fst(X1,X2))	→	active^#(X1)	(56)
active^#(add(X1,X2))	→	active^#(X2)	(55)
active^#(from(X))	→	active^#(X)	(54)
active^#(add(X1,X2))	→	active^#(X1)	(78)
active^#(cons(X1,X2))	→	active^#(X1)	(47)
active^#(fst(X1,X2))	→	active^#(X2)	(40)
active^#(len(X))	→	active^#(X)	(67)

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

len^#(mark(X))	→	len^#(X)	(46)
len^#(ok(X))	→	len^#(X)	(72)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₁ + 1
[top^#(x₁)]	=	x₁ + 0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 32570
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 44249
[len(x₁)]	=	x₁ + 0

together with the usable rules

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

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

len^#(ok(X))

→

len^#(X)

(72)

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

len^#(mark(X))

→

len^#(X)

(46)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

len^#(mark(X))

→

len^#(X)

(46)

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

fst^#(ok(X1),ok(X2))	→	fst^#(X1,X2)	(52)
fst^#(mark(X1),X2)	→	fst^#(X1,X2)	(48)
fst^#(X1,mark(X2))	→	fst^#(X1,X2)	(69)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	x₁ + 0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	3
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

fst^#(ok(X1),ok(X2))	→	fst^#(X1,X2)	(52)
fst^#(mark(X1),X2)	→	fst^#(X1,X2)	(48)

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

fst^#(X1,mark(X2))

→

fst^#(X1,X2)

(69)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	x₂ + 0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 14756
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 14758
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

fst^#(X1,mark(X2))

→

fst^#(X1,X2)

(69)

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

add^#(X1,mark(X2))	→	add^#(X1,X2)	(66)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(82)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(44)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 31675
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 63039
[cons(x₁, x₂)]	=	x₂ + 31363
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₁ + x₂ + 0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

add^#(X1,mark(X2))	→	add^#(X1,X2)	(66)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(82)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(44)

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

from^#(ok(X))	→	from^#(X)	(63)
from^#(mark(X))	→	from^#(X)	(51)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

from^#(ok(X))	→	from^#(X)	(63)
from^#(mark(X))	→	from^#(X)	(51)

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

s^#(ok(X))

→

s^#(X)

(83)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 16898
[s^#(x₁)]	=	x₁ + 0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

s^#(ok(X))

→

s^#(X)

(83)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(92)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(87)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	0
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[fst(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	0
[fst^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 1
[len(x₁)]	=	x₁ + 0

together with the usable rules

from(mark(X))	→	mark(from(X))	(18)
active(add(0,X))	→	mark(X)	(4)
active(fst(0,Z))	→	mark(nil)	(1)
len(mark(X))	→	mark(len(X))	(21)
proper(0)	→	ok(0)	(22)
from(ok(X))	→	ok(from(X))	(33)
active(len(cons(X,Z)))	→	mark(s(len(Z)))	(7)
s(ok(X))	→	ok(s(X))	(30)
proper(nil)	→	ok(nil)	(24)
active(len(nil))	→	mark(0)	(6)
len(ok(X))	→	ok(len(X))	(35)

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

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(92)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(87)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.