Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci01)

The rewrite relation of the following TRS is considered.

active(eq(0,0))	→	mark(true)	(1)
active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)
active(eq(X,Y))	→	mark(false)	(3)
active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
active(take(0,X))	→	mark(nil)	(5)
active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
active(length(nil))	→	mark(0)	(7)
active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
active(inf(X))	→	inf(active(X))	(9)
active(take(X1,X2))	→	take(active(X1),X2)	(10)
active(take(X1,X2))	→	take(X1,active(X2))	(11)
active(length(X))	→	length(active(X))	(12)
inf(mark(X))	→	mark(inf(X))	(13)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
length(mark(X))	→	mark(length(X))	(16)
proper(eq(X1,X2))	→	eq(proper(X1),proper(X2))	(17)
proper(0)	→	ok(0)	(18)
proper(true)	→	ok(true)	(19)
proper(s(X))	→	s(proper(X))	(20)
proper(false)	→	ok(false)	(21)
proper(inf(X))	→	inf(proper(X))	(22)
proper(cons(any(X1),X2))	→	cons(any(any(proper(X1))),any(proper(X2)))	(23)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(24)
proper(nil)	→	ok(nil)	(25)
proper(length(X))	→	length(proper(X))	(26)
eq(ok(X1),ok(X2))	→	ok(eq(X1,X2))	(27)
s(ok(X))	→	ok(s(X))	(28)
inf(ok(X))	→	ok(inf(X))	(29)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
length(ok(X))	→	ok(length(X))	(32)
top(mark(X))	→	top(proper(X))	(33)
top(ok(X))	→	top(active(X))	(34)
any(X)	→	s(X)	(35)
any(proper(X))	→	any(any(any(X)))	(36)

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.

inf^#(ok(X))	→	inf^#(X)	(37)
any^#(proper(X))	→	any^#(any(any(X)))	(38)
top^#(mark(X))	→	top^#(proper(X))	(39)
top^#(ok(X))	→	active^#(X)	(40)
length^#(mark(X))	→	length^#(X)	(41)
proper^#(length(X))	→	proper^#(X)	(42)
proper^#(length(X))	→	length^#(proper(X))	(43)
proper^#(eq(X1,X2))	→	eq^#(proper(X1),proper(X2))	(44)
active^#(length(cons(X,L)))	→	s^#(length(L))	(45)
active^#(length(cons(X,L)))	→	length^#(L)	(46)
proper^#(eq(X1,X2))	→	proper^#(X1)	(47)
inf^#(mark(X))	→	inf^#(X)	(48)
length^#(ok(X))	→	length^#(X)	(49)
active^#(inf(X))	→	inf^#(s(X))	(50)
proper^#(take(X1,X2))	→	proper^#(X2)	(51)
active^#(take(X1,X2))	→	take^#(X1,active(X2))	(52)
proper^#(take(X1,X2))	→	take^#(proper(X1),proper(X2))	(53)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(54)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(55)
any^#(proper(X))	→	any^#(X)	(56)
proper^#(take(X1,X2))	→	proper^#(X1)	(57)
s^#(ok(X))	→	s^#(X)	(58)
proper^#(cons(any(X1),X2))	→	cons^#(any(any(proper(X1))),any(proper(X2)))	(59)
top^#(mark(X))	→	proper^#(X)	(60)
active^#(inf(X))	→	s^#(X)	(61)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(62)
proper^#(s(X))	→	s^#(proper(X))	(63)
active^#(length(X))	→	length^#(active(X))	(64)
active^#(inf(X))	→	inf^#(active(X))	(65)
proper^#(eq(X1,X2))	→	proper^#(X2)	(66)
active^#(take(X1,X2))	→	active^#(X2)	(67)
proper^#(inf(X))	→	proper^#(X)	(68)
active^#(take(s(X),cons(Y,L)))	→	take^#(X,L)	(69)
any^#(proper(X))	→	any^#(any(X))	(70)
active^#(take(X1,X2))	→	active^#(X1)	(71)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(72)
top^#(ok(X))	→	top^#(active(X))	(73)
active^#(take(X1,X2))	→	take^#(active(X1),X2)	(74)
proper^#(cons(any(X1),X2))	→	proper^#(X1)	(75)
proper^#(inf(X))	→	inf^#(proper(X))	(76)
proper^#(cons(any(X1),X2))	→	proper^#(X2)	(77)
proper^#(s(X))	→	proper^#(X)	(78)
eq^#(ok(X1),ok(X2))	→	eq^#(X1,X2)	(79)
active^#(length(X))	→	active^#(X)	(80)
proper^#(cons(any(X1),X2))	→	any^#(proper(X1))	(81)
any^#(X)	→	s^#(X)	(82)
active^#(eq(s(X),s(Y)))	→	eq^#(X,Y)	(83)
active^#(inf(X))	→	active^#(X)	(84)
proper^#(cons(any(X1),X2))	→	any^#(any(proper(X1)))	(85)
active^#(take(s(X),cons(Y,L)))	→	cons^#(Y,take(X,L))	(86)
active^#(inf(X))	→	cons^#(X,inf(s(X)))	(87)
proper^#(cons(any(X1),X2))	→	any^#(proper(X2))	(88)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(73)
top^#(mark(X))	→	top^#(proper(X))	(39)

1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[cons^#(x₁, x₂)]

[s(x₁)]

1	0
0	0

· x₁ +

32714

50571

[take^#(x₁, x₂)]

[take(x₁, x₂)]

0	0
0	1

· x₁ +

0	0
0	1

· x₂ +

[top(x₁)]

[eq(x₁, x₂)]

0	0
1	0

· x₁ +

0	0
1	0

· x₂ +

23127

[any(x₁)]

0	1
0	0

· x₁ +

32713

20485

[false]

[top^#(x₁)]

0	1
0	0

· x₁ +

[any^#(x₁)]

[true]

3106

[eq^#(x₁, x₂)]

[proper(x₁)]

x₁ +

[ok(x₁)]

x₁ +

[0]

[s^#(x₁)]

[nil]

[mark(x₁)]

0	0
1	1

· x₁ +

[proper^#(x₁)]

[inf^#(x₁)]

[active(x₁)]

0	0
0	1

· x₁ +

[cons(x₁, x₂)]

17962

83285

[active^#(x₁)]

[length(x₁)]

0	0
0	1

· x₁ +

[length^#(x₁)]

[inf(x₁)]

0	0
0	1

· x₁ +

101249

together with the usable rules

proper(0)	→	ok(0)	(18)
active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
active(eq(0,0))	→	mark(true)	(1)
active(eq(X,Y))	→	mark(false)	(3)
length(mark(X))	→	mark(length(X))	(16)
proper(false)	→	ok(false)	(21)
proper(length(X))	→	length(proper(X))	(26)
proper(true)	→	ok(true)	(19)
length(ok(X))	→	ok(length(X))	(32)
proper(eq(X1,X2))	→	eq(proper(X1),proper(X2))	(17)
eq(ok(X1),ok(X2))	→	ok(eq(X1,X2))	(27)
proper(inf(X))	→	inf(proper(X))	(22)
s(ok(X))	→	ok(s(X))	(28)
active(take(0,X))	→	mark(nil)	(5)
active(take(X1,X2))	→	take(active(X1),X2)	(10)
active(length(nil))	→	mark(0)	(7)
proper(s(X))	→	s(proper(X))	(20)
proper(nil)	→	ok(nil)	(25)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
active(length(X))	→	length(active(X))	(12)
proper(cons(any(X1),X2))	→	cons(any(any(proper(X1))),any(proper(X2)))	(23)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(24)
active(take(X1,X2))	→	take(X1,active(X2))	(11)
active(inf(X))	→	inf(active(X))	(9)
inf(mark(X))	→	mark(inf(X))	(13)
active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
inf(ok(X))	→	ok(inf(X))	(29)
active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(39)

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

(73)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₂ + 20912
[any(x₁)]	=	x₁ + 0
[false]	=	29161
[top^#(x₁)]	=	x₁ + 0
[any^#(x₁)]	=	0
[true]	=	47909
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 2
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	23467
[mark(x₁)]	=	1
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 977
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 34296
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 3824

together with the usable rules

proper(0)	→	ok(0)	(18)
active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
active(eq(0,0))	→	mark(true)	(1)
active(eq(X,Y))	→	mark(false)	(3)
length(mark(X))	→	mark(length(X))	(16)
proper(false)	→	ok(false)	(21)
any(proper(X))	→	any(any(any(X)))	(36)
proper(length(X))	→	length(proper(X))	(26)
proper(true)	→	ok(true)	(19)
length(ok(X))	→	ok(length(X))	(32)
proper(eq(X1,X2))	→	eq(proper(X1),proper(X2))	(17)
eq(ok(X1),ok(X2))	→	ok(eq(X1,X2))	(27)
proper(inf(X))	→	inf(proper(X))	(22)
s(ok(X))	→	ok(s(X))	(28)
active(take(0,X))	→	mark(nil)	(5)
active(take(X1,X2))	→	take(active(X1),X2)	(10)
active(length(nil))	→	mark(0)	(7)
proper(s(X))	→	s(proper(X))	(20)
proper(nil)	→	ok(nil)	(25)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
active(length(X))	→	length(active(X))	(12)
proper(cons(any(X1),X2))	→	cons(any(any(proper(X1))),any(proper(X2)))	(23)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(24)
active(take(X1,X2))	→	take(X1,active(X2))	(11)
active(inf(X))	→	inf(active(X))	(9)
inf(mark(X))	→	mark(inf(X))	(13)
active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
any(X)	→	s(X)	(35)
inf(ok(X))	→	ok(inf(X))	(29)
active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(73)

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^#(take(X1,X2))	→	proper^#(X1)	(57)
proper^#(s(X))	→	proper^#(X)	(78)
proper^#(take(X1,X2))	→	proper^#(X2)	(51)
proper^#(cons(any(X1),X2))	→	proper^#(X2)	(77)
proper^#(cons(any(X1),X2))	→	proper^#(X1)	(75)
proper^#(eq(X1,X2))	→	proper^#(X1)	(47)
proper^#(inf(X))	→	proper^#(X)	(68)
proper^#(length(X))	→	proper^#(X)	(42)
proper^#(eq(X1,X2))	→	proper^#(X2)	(66)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[any(x₁)]	=	x₁ + 0
[false]	=	8573
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	28652
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	8822
[ok(x₁)]	=	x₁ + 39707
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	4934
[proper^#(x₁)]	=	x₁ + 0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 4930
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 2

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

proper^#(take(X1,X2))	→	proper^#(X1)	(57)
proper^#(s(X))	→	proper^#(X)	(78)
proper^#(take(X1,X2))	→	proper^#(X2)	(51)
proper^#(cons(any(X1),X2))	→	proper^#(X2)	(77)
proper^#(cons(any(X1),X2))	→	proper^#(X1)	(75)
proper^#(eq(X1,X2))	→	proper^#(X1)	(47)
proper^#(inf(X))	→	proper^#(X)	(68)
proper^#(length(X))	→	proper^#(X)	(42)
proper^#(eq(X1,X2))	→	proper^#(X2)	(66)

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^#(inf(X))	→	active^#(X)	(84)
active^#(length(X))	→	active^#(X)	(80)
active^#(take(X1,X2))	→	active^#(X1)	(71)
active^#(take(X1,X2))	→	active^#(X2)	(67)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[any(x₁)]	=	x₁ + 0
[false]	=	8822
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	8822
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	8822
[ok(x₁)]	=	x₁ + 1
[0]	=	8822
[s^#(x₁)]	=	0
[nil]	=	8822
[mark(x₁)]	=	17647
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 8562
[active^#(x₁)]	=	x₁ + 0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 1

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

active^#(inf(X))	→	active^#(X)	(84)
active^#(length(X))	→	active^#(X)	(80)
active^#(take(X1,X2))	→	active^#(X1)	(71)
active^#(take(X1,X2))	→	active^#(X2)	(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

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

→

eq^#(X1,X2)

(79)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[any(x₁)]	=	x₁ + 0
[false]	=	1800
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	1
[eq^#(x₁, x₂)]	=	x₁ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	8623
[mark(x₁)]	=	17647
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 1

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

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

→

eq^#(X1,X2)

(79)

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(62)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(55)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(72)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[any(x₁)]	=	x₁ + 0
[false]	=	1
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	1
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 17647
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 35261

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(62)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(55)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(72)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

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

→

cons^#(X1,X2)

(54)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[any(x₁)]	=	x₁ + 0
[false]	=	26784
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	1
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 4
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 1

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

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

→

cons^#(X1,X2)

(54)

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

any^#(proper(X))	→	any^#(X)	(56)
any^#(proper(X))	→	any^#(any(X))	(70)
any^#(proper(X))	→	any^#(any(any(X)))	(38)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₁ + 0
[any(x₁)]	=	1
[false]	=	1
[top^#(x₁)]	=	0
[any^#(x₁)]	=	x₁ + 0
[true]	=	43313
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 2
[ok(x₁)]	=	x₁ + 0
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 3
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 1
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 1

together with the usable rules

any(proper(X))	→	any(any(any(X)))	(36)
s(ok(X))	→	ok(s(X))	(28)
any(X)	→	s(X)	(35)

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

any^#(proper(X))	→	any^#(X)	(56)
any^#(proper(X))	→	any^#(any(X))	(70)
any^#(proper(X))	→	any^#(any(any(X)))	(38)

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)

(58)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	50181
[any(x₁)]	=	x₁ + 0
[false]	=	50181
[top^#(x₁)]	=	0
[any^#(x₁)]	=	x₁ + 0
[true]	=	50181
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	50181
[s^#(x₁)]	=	x₁ + 0
[nil]	=	50181
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	50180
[cons(x₁, x₂)]	=	x₁ + 50181
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 0
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 0

together with the usable rules

proper(0)	→	ok(0)	(18)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
length(mark(X))	→	mark(length(X))	(16)
proper(false)	→	ok(false)	(21)
any(proper(X))	→	any(any(any(X)))	(36)
proper(true)	→	ok(true)	(19)
length(ok(X))	→	ok(length(X))	(32)
s(ok(X))	→	ok(s(X))	(28)
proper(nil)	→	ok(nil)	(25)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
inf(mark(X))	→	mark(inf(X))	(13)
any(X)	→	s(X)	(35)
inf(ok(X))	→	ok(inf(X))	(29)

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

s^#(ok(X))

→

s^#(X)

(58)

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

inf^#(mark(X))	→	inf^#(X)	(48)
inf^#(ok(X))	→	inf^#(X)	(37)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 1
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	2
[any(x₁)]	=	x₁ + 0
[false]	=	17574
[top^#(x₁)]	=	0
[any^#(x₁)]	=	x₁ + 0
[true]	=	30754
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	2
[s^#(x₁)]	=	0
[nil]	=	2
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₁ + 2
[active^#(x₁)]	=	0
[length(x₁)]	=	x₁ + 0
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 0

together with the usable rules

proper(0)	→	ok(0)	(18)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
length(mark(X))	→	mark(length(X))	(16)
proper(false)	→	ok(false)	(21)
any(proper(X))	→	any(any(any(X)))	(36)
proper(true)	→	ok(true)	(19)
length(ok(X))	→	ok(length(X))	(32)
s(ok(X))	→	ok(s(X))	(28)
proper(nil)	→	ok(nil)	(25)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
inf(mark(X))	→	mark(inf(X))	(13)
any(X)	→	s(X)	(35)
inf(ok(X))	→	ok(inf(X))	(29)

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

inf^#(ok(X))

→

inf^#(X)

(37)

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

inf^#(mark(X))

→

inf^#(X)

(48)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	1
[any(x₁)]	=	x₁ + 0
[false]	=	1427
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	26064
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	0
[ok(x₁)]	=	0
[0]	=	25337
[s^#(x₁)]	=	0
[nil]	=	22611
[mark(x₁)]	=	x₁ + 7803
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	7802
[cons(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[length(x₁)]	=	0
[length^#(x₁)]	=	0
[inf(x₁)]	=	0

together with the usable rules

proper(0)	→	ok(0)	(18)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
proper(false)	→	ok(false)	(21)
proper(true)	→	ok(true)	(19)
proper(nil)	→	ok(nil)	(25)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)

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

inf^#(mark(X))

→

inf^#(X)

(48)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

length^#(ok(X))	→	length^#(X)	(49)
length^#(mark(X))	→	length^#(X)	(41)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	0
[any(x₁)]	=	x₁ + 0
[false]	=	1
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	0
[ok(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 34734
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	34733
[cons(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[length(x₁)]	=	0
[length^#(x₁)]	=	x₁ + 0
[inf(x₁)]	=	0

together with the usable rules

proper(0)	→	ok(0)	(18)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
proper(true)	→	ok(true)	(19)
proper(nil)	→	ok(nil)	(25)
take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)

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

length^#(mark(X))

→

length^#(X)

(41)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

length^#(ok(X))

→

length^#(X)

(49)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 0
[top(x₁)]	=	0
[eq(x₁, x₂)]	=	x₂ + 0
[any(x₁)]	=	0
[false]	=	1
[top^#(x₁)]	=	0
[any^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	1
[proper^#(x₁)]	=	0
[inf^#(x₁)]	=	0
[active(x₁)]	=	0
[cons(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[length(x₁)]	=	0
[length^#(x₁)]	=	x₁ + 0
[inf(x₁)]	=	x₁ + 0

together with the usable rules

proper(0)	→	ok(0)	(18)
take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
proper(true)	→	ok(true)	(19)
proper(nil)	→	ok(nil)	(25)

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

length^#(ok(X))

→

length^#(X)

(49)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.