Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_7_37_Bor03_iGM)

The rewrite relation of the following TRS is considered.

active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
active(minus(X,0))	→	mark(0)	(4)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
active(quot(0,s(Y)))	→	mark(0)	(6)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(zWquot(nil,XS))	→	mark(nil)	(9)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
mark(from(X))	→	active(from(mark(X)))	(11)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
mark(s(X))	→	active(s(mark(X)))	(13)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
mark(0)	→	active(0)	(15)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
mark(nil)	→	active(nil)	(19)
from(mark(X))	→	from(X)	(20)
from(active(X))	→	from(X)	(21)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(26)
s(active(X))	→	s(X)	(27)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)

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.

zWquot^#(X1,active(X2))	→	zWquot^#(X1,X2)	(44)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(45)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(46)
quot^#(X1,active(X2))	→	quot^#(X1,X2)	(47)
active^#(zWquot(XS,nil))	→	mark^#(nil)	(48)
s^#(active(X))	→	s^#(X)	(49)
active^#(minus(s(X),s(Y)))	→	minus^#(X,Y)	(50)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	cons^#(quot(X,Y),zWquot(XS,YS))	(52)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
s^#(mark(X))	→	s^#(X)	(54)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(55)
mark^#(quot(X1,X2))	→	quot^#(mark(X1),mark(X2))	(56)
mark^#(minus(X1,X2))	→	mark^#(X1)	(57)
active^#(sel(s(N),cons(X,XS)))	→	sel^#(N,XS)	(58)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	quot^#(X,Y)	(59)
zWquot^#(X1,mark(X2))	→	zWquot^#(X1,X2)	(60)
mark^#(minus(X1,X2))	→	mark^#(X2)	(61)
from^#(active(X))	→	from^#(X)	(62)
mark^#(0)	→	active^#(0)	(63)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(64)
minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(65)
mark^#(s(X))	→	mark^#(X)	(66)
active^#(quot(0,s(Y)))	→	mark^#(0)	(67)
mark^#(s(X))	→	active^#(s(mark(X)))	(68)
mark^#(minus(X1,X2))	→	minus^#(mark(X1),mark(X2))	(69)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
mark^#(zWquot(X1,X2))	→	zWquot^#(mark(X1),mark(X2))	(71)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(72)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(73)
mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
mark^#(s(X))	→	s^#(mark(X))	(75)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
active^#(zWquot(nil,XS))	→	mark^#(nil)	(78)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
from^#(mark(X))	→	from^#(X)	(80)
mark^#(nil)	→	active^#(nil)	(81)
mark^#(quot(X1,X2))	→	mark^#(X1)	(82)
mark^#(sel(X1,X2))	→	sel^#(mark(X1),mark(X2))	(83)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(84)
quot^#(X1,mark(X2))	→	quot^#(X1,X2)	(85)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	zWquot^#(XS,YS)	(86)
zWquot^#(mark(X1),X2)	→	zWquot^#(X1,X2)	(87)
active^#(from(X))	→	from^#(s(X))	(88)
active^#(quot(s(X),s(Y)))	→	quot^#(minus(X,Y),s(Y))	(89)
mark^#(zWquot(X1,X2))	→	mark^#(X2)	(90)
zWquot^#(active(X1),X2)	→	zWquot^#(X1,X2)	(91)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(92)
active^#(from(X))	→	s^#(X)	(93)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(94)
mark^#(cons(X1,X2))	→	mark^#(X1)	(95)
active^#(quot(s(X),s(Y)))	→	minus^#(X,Y)	(96)
mark^#(sel(X1,X2))	→	mark^#(X2)	(97)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(from(X))	→	mark^#(X)	(99)
active^#(quot(s(X),s(Y)))	→	s^#(quot(minus(X,Y),s(Y)))	(100)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(101)
active^#(from(X))	→	cons^#(X,from(s(X)))	(102)
mark^#(sel(X1,X2))	→	mark^#(X1)	(103)
active^#(minus(X,0))	→	mark^#(0)	(104)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
mark^#(cons(X1,X2))	→	cons^#(mark(X1),X2)	(106)
mark^#(from(X))	→	from^#(mark(X))	(107)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(108)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(109)
quot^#(mark(X1),X2)	→	quot^#(X1,X2)	(110)
quot^#(active(X1),X2)	→	quot^#(X1,X2)	(111)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)
minus^#(X1,active(X2))	→	minus^#(X1,X2)	(113)
mark^#(quot(X1,X2))	→	mark^#(X2)	(114)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(115)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

mark^#(quot(X1,X2))	→	mark^#(X2)	(114)
mark^#(quot(X1,X2))	→	mark^#(X1)	(82)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(109)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
mark^#(sel(X1,X2))	→	mark^#(X1)	(103)
mark^#(s(X))	→	active^#(s(mark(X)))	(68)
mark^#(s(X))	→	mark^#(X)	(66)
mark^#(from(X))	→	mark^#(X)	(99)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	mark^#(X2)	(61)
mark^#(sel(X1,X2))	→	mark^#(X2)	(97)
mark^#(minus(X1,X2))	→	mark^#(X1)	(57)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(55)
mark^#(cons(X1,X2))	→	mark^#(X1)	(95)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
mark^#(zWquot(X1,X2))	→	mark^#(X2)	(90)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(84)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	24867
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	24868
[zWquot(x₁, x₂)]	=	24868
[mark^#(x₁)]	=	24868
[0]	=	1
[quot(x₁, x₂)]	=	24868
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	24868
[sel(x₁, x₂)]	=	24868
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 0
[quot^#(x₁, x₂)]	=	0

together with the usable rules

from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)

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

mark^#(s(X))	→	active^#(s(mark(X)))	(68)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(84)

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

mark^#(zWquot(X1,X2))	→	mark^#(X2)	(90)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(55)
mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	mark^#(X2)	(61)
mark^#(minus(X1,X2))	→	mark^#(X1)	(57)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
mark^#(quot(X1,X2))	→	mark^#(X2)	(114)
mark^#(quot(X1,X2))	→	mark^#(X1)	(82)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(sel(X1,X2))	→	mark^#(X2)	(97)
mark^#(sel(X1,X2))	→	mark^#(X1)	(103)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
mark^#(cons(X1,X2))	→	mark^#(X1)	(95)
mark^#(from(X))	→	mark^#(X)	(99)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)
mark^#(s(X))	→	mark^#(X)	(66)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(109)

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
[zWquot^#(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[zWquot(x₁, x₂)]	=	max(x₁ + 25438, x₂ + 16580, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	7723
[quot(x₁, x₂)]	=	max(x₁ + 7720, x₂ + 7722, 0)
[sel^#(x₁, x₂)]	=	max(0)
[from(x₁)]	=	x₁ + 30096
[sel(x₁, x₂)]	=	max(x₁ + 2439, x₂ + 2438, 0)
[s^#(x₁)]	=	0
[nil]	=	25439
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	max(0)
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 8857, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[quot^#(x₁, x₂)]	=	max(0)

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

mark^#(zWquot(X1,X2))	→	mark^#(X2)	(90)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(55)
mark^#(minus(X1,X2))	→	mark^#(X2)	(61)
mark^#(quot(X1,X2))	→	mark^#(X2)	(114)
mark^#(quot(X1,X2))	→	mark^#(X1)	(82)
mark^#(sel(X1,X2))	→	mark^#(X2)	(97)
mark^#(sel(X1,X2))	→	mark^#(X1)	(103)
mark^#(cons(X1,X2))	→	mark^#(X1)	(95)
mark^#(from(X))	→	mark^#(X)	(99)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(109)

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

mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	mark^#(X1)	(57)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)
mark^#(s(X))	→	mark^#(X)	(66)

1.1.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
[zWquot^#(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 2, x₂ + 1, 0)
[zWquot(x₁, x₂)]	=	max(0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[quot(x₁, x₂)]	=	max(0)
[sel^#(x₁, x₂)]	=	max(0)
[from(x₁)]	=	x₁ + 1
[sel(x₁, x₂)]	=	max(x₁ + 1, x₂ + 23022, 0)
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	max(0)
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[quot^#(x₁, x₂)]	=	max(0)

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

mark^#(minus(X1,X2))

→

mark^#(X1)

(57)

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

mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)
mark^#(s(X))	→	mark^#(X)	(66)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	5970
[zWquot(x₁, x₂)]	=	x₁ + 5971
[mark^#(x₁)]	=	x₁ + 0
[0]	=	5972
[quot(x₁, x₂)]	=	5970
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	5971
[sel(x₁, x₂)]	=	5970
[s^#(x₁)]	=	0
[nil]	=	5973
[mark(x₁)]	=	x₁ + 17525
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 17526
[cons(x₁, x₂)]	=	5969
[active^#(x₁)]	=	5970
[quot^#(x₁, x₂)]	=	0

together with the usable rules

quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)

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

mark^#(zWquot(X1,X2))	→	active^#(zWquot(mark(X1),mark(X2)))	(74)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(79)
active^#(zWquot(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(quot(X,Y),zWquot(XS,YS)))	(105)
mark^#(from(X))	→	active^#(from(mark(X)))	(112)

could be deleted.

1.1.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^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)
mark^#(s(X))	→	mark^#(X)	(66)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(zWquot^#)	=	0	status(zWquot^#)	=	[]	list-extension(zWquot^#)	=	Lex
prec(minus)	=	2	status(minus)	=	[]	list-extension(minus)	=	Lex
prec(zWquot)	=	4	status(zWquot)	=	[1]	list-extension(zWquot)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	4	status(quot)	=	[1]	list-extension(quot)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(from)	=	5	status(from)	=	[]	list-extension(from)	=	Lex
prec(sel)	=	3	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(nil)	=	1	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(minus^#)	=	0	status(minus^#)	=	[2, 1]	list-extension(minus^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(cons)	=	4	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[]	list-extension(quot^#)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[zWquot^#(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	max(0)
[zWquot(x₁, x₂)]	=	x₁ + x₂ + 1
[0]	=	0
[quot(x₁, x₂)]	=	max(x₁ + 7580, 0)
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 38693
[sel(x₁, x₂)]	=	x₂ + 19794
[nil]	=	0
[minus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 7581, x₂ + 0, 0)
[quot^#(x₁, x₂)]	=	max(x₁ + 1, 0)

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

active^#(quot(s(X),s(Y)))	→	mark^#(s(quot(minus(X,Y),s(Y))))	(76)
mark^#(s(X))	→	mark^#(X)	(66)

could be deleted.

1.1.1.1.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^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
mark^#(quot(X1,X2))	→	active^#(quot(mark(X1),mark(X2)))	(53)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	24703
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[quot(x₁, x₂)]	=	x₂ + 24704
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	24703
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	24703
[quot^#(x₁, x₂)]	=	0

together with the usable rules

s(mark(X))	→	s(X)	(26)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)

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

mark^#(quot(X1,X2))

→

active^#(quot(mark(X1),mark(X2)))

(53)

could be deleted.

1.1.1.1.1.1.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^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(98)
mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	1
π(s^#)	=	1
π(mark)	=	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(zWquot^#)	=	0	status(zWquot^#)	=	[]	list-extension(zWquot^#)	=	Lex
prec(minus)	=	2	status(minus)	=	[]	list-extension(minus)	=	Lex
prec(zWquot)	=	5	status(zWquot)	=	[]	list-extension(zWquot)	=	Lex
prec(mark^#)	=	2	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	6	status(quot)	=	[1]	list-extension(quot)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(from)	=	5	status(from)	=	[1]	list-extension(from)	=	Lex
prec(sel)	=	3	status(sel)	=	[1]	list-extension(sel)	=	Lex
prec(nil)	=	0	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(minus^#)	=	0	status(minus^#)	=	[2, 1]	list-extension(minus^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(cons)	=	5	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(active^#)	=	2	status(active^#)	=	[1]	list-extension(active^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[]	list-extension(quot^#)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[zWquot^#(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	max(0)
[zWquot(x₁, x₂)]	=	x₁ + 27849
[mark^#(x₁)]	=	x₁ + 2
[0]	=	0
[quot(x₁, x₂)]	=	max(x₁ + 14023, 0)
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 1770
[sel(x₁, x₂)]	=	x₁ + x₂ + 9246
[nil]	=	27848
[minus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 2
[quot^#(x₁, x₂)]	=	max(x₁ + 1, 0)

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

active^#(sel(s(N),cons(X,XS)))

→

mark^#(sel(N,XS))

(98)

could be deleted.

1.1.1.1.1.1.1.1.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

mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(70)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	2
[zWquot(x₁, x₂)]	=	1
[mark^#(x₁)]	=	2
[0]	=	1
[quot(x₁, x₂)]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 0
[quot^#(x₁, x₂)]	=	0

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

mark^#(sel(X1,X2))

→

active^#(sel(mark(X1),mark(X2)))

(70)

could be deleted.

1.1.1.1.1.1.1.1.1.1.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

mark^#(minus(X1,X2))	→	active^#(minus(mark(X1),mark(X2)))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(51)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(zWquot^#)	=	0	status(zWquot^#)	=	[]	list-extension(zWquot^#)	=	Lex
prec(minus)	=	2	status(minus)	=	[1]	list-extension(minus)	=	Lex
prec(zWquot)	=	5	status(zWquot)	=	[]	list-extension(zWquot)	=	Lex
prec(mark^#)	=	3	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	6	status(quot)	=	[1]	list-extension(quot)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(from)	=	4	status(from)	=	[1]	list-extension(from)	=	Lex
prec(sel)	=	4	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(nil)	=	0	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(minus^#)	=	0	status(minus^#)	=	[2, 1]	list-extension(minus^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(cons)	=	4	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(active^#)	=	3	status(active^#)	=	[1]	list-extension(active^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[]	list-extension(quot^#)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[zWquot^#(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	max(x₁ + 0, 0)
[zWquot(x₁, x₂)]	=	x₁ + 82834
[mark^#(x₁)]	=	x₁ + 1
[0]	=	0
[quot(x₁, x₂)]	=	max(x₁ + 56460, 0)
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 42249
[sel(x₁, x₂)]	=	x₂ + 46734
[nil]	=	0
[minus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 26373, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 1
[quot^#(x₁, x₂)]	=	max(x₁ + 1, 0)

together with the usable rules

mark(zWquot(X1,X2))	→	active(zWquot(mark(X1),mark(X2)))	(18)
active(minus(X,0))	→	mark(0)	(4)
mark(0)	→	active(0)	(15)
active(zWquot(XS,nil))	→	mark(nil)	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(3)
mark(minus(X1,X2))	→	active(minus(mark(X1),mark(X2)))	(16)
from(active(X))	→	from(X)	(21)
quot(mark(X1),X2)	→	quot(X1,X2)	(36)
s(mark(X))	→	s(X)	(26)
mark(nil)	→	active(nil)	(19)
minus(mark(X1),X2)	→	minus(X1,X2)	(32)
mark(quot(X1,X2))	→	active(quot(mark(X1),mark(X2)))	(17)
s(active(X))	→	s(X)	(27)
minus(active(X1),X2)	→	minus(X1,X2)	(34)
cons(mark(X1),X2)	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(28)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(5)
minus(X1,mark(X2))	→	minus(X1,X2)	(33)
active(zWquot(cons(X,XS),cons(Y,YS)))	→	mark(cons(quot(X,Y),zWquot(XS,YS)))	(10)
quot(X1,active(X2))	→	quot(X1,X2)	(39)
active(quot(s(X),s(Y)))	→	mark(s(quot(minus(X,Y),s(Y))))	(7)
from(mark(X))	→	from(X)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(30)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(14)
sel(X1,active(X2))	→	sel(X1,X2)	(31)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(12)
cons(X1,mark(X2))	→	cons(X1,X2)	(23)
cons(active(X1),X2)	→	cons(X1,X2)	(24)
mark(from(X))	→	active(from(mark(X)))	(11)
active(zWquot(nil,XS))	→	mark(nil)	(9)
mark(s(X))	→	active(s(mark(X)))	(13)
zWquot(mark(X1),X2)	→	zWquot(X1,X2)	(40)
active(quot(0,s(Y)))	→	mark(0)	(6)
quot(active(X1),X2)	→	quot(X1,X2)	(38)
quot(X1,mark(X2))	→	quot(X1,X2)	(37)
zWquot(X1,mark(X2))	→	zWquot(X1,X2)	(41)
zWquot(active(X1),X2)	→	zWquot(X1,X2)	(42)
minus(X1,active(X2))	→	minus(X1,X2)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(29)
zWquot(X1,active(X2))	→	zWquot(X1,X2)	(43)
active(sel(0,cons(X,XS)))	→	mark(X)	(2)

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

active^#(minus(s(X),s(Y)))

→

mark^#(minus(X,Y))

(51)

could be deleted.

1.1.1.1.1.1.1.1.1.1.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

quot^#(active(X1),X2)	→	quot^#(X1,X2)	(111)
quot^#(mark(X1),X2)	→	quot^#(X1,X2)	(110)
quot^#(X1,mark(X2))	→	quot^#(X1,X2)	(85)
quot^#(X1,active(X2))	→	quot^#(X1,X2)	(47)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	21069
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	1941
[zWquot(x₁, x₂)]	=	x₁ + 21065
[mark^#(x₁)]	=	1
[0]	=	21069
[quot(x₁, x₂)]	=	21067
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	30860
[sel(x₁, x₂)]	=	x₁ + 56475
[s^#(x₁)]	=	0
[nil]	=	21067
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 30862
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	x₂ + 0

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

quot^#(X1,mark(X2))	→	quot^#(X1,X2)	(85)
quot^#(X1,active(X2))	→	quot^#(X1,X2)	(47)

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

quot^#(mark(X1),X2)	→	quot^#(X1,X2)	(110)
quot^#(active(X1),X2)	→	quot^#(X1,X2)	(111)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	16961
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	765
[zWquot(x₁, x₂)]	=	x₁ + 16957
[mark^#(x₁)]	=	1
[0]	=	16961
[quot(x₁, x₂)]	=	16959
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	3137
[sel(x₁, x₂)]	=	x₁ + 26087
[s^#(x₁)]	=	0
[nil]	=	16959
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 3139
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	x₁ + 0

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

quot^#(mark(X1),X2)	→	quot^#(X1,X2)	(110)
quot^#(active(X1),X2)	→	quot^#(X1,X2)	(111)

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

minus^#(X1,active(X2))	→	minus^#(X1,X2)	(113)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(73)
minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(65)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(64)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1664
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 30753
[zWquot(x₁, x₂)]	=	x₁ + 1660
[mark^#(x₁)]	=	1
[0]	=	26987
[quot(x₁, x₂)]	=	1662
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	x₁ + 33102
[s^#(x₁)]	=	0
[nil]	=	1662
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	x₂ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 3
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

minus^#(X1,active(X2))	→	minus^#(X1,X2)	(113)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(64)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(65)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(73)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	15910
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 1
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	1
[0]	=	18403
[quot(x₁, x₂)]	=	15908
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	10127
[sel(x₁, x₂)]	=	x₁ + 11248
[s^#(x₁)]	=	0
[nil]	=	3
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 10129
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(65)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(73)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(72)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(108)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(94)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(45)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	8677
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 29509
[zWquot(x₁, x₂)]	=	x₁ + 8673
[mark^#(x₁)]	=	1
[0]	=	18403
[quot(x₁, x₂)]	=	8675
[sel^#(x₁, x₂)]	=	x₁ + 0
[from(x₁)]	=	11403
[sel(x₁, x₂)]	=	x₁ + 16837
[s^#(x₁)]	=	0
[nil]	=	8675
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 11405
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

sel^#(active(X1),X2)	→	sel^#(X1,X2)	(94)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(45)

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

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(72)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(108)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1330
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 23235
[zWquot(x₁, x₂)]	=	x₁ + 1326
[mark^#(x₁)]	=	1
[0]	=	1330
[quot(x₁, x₂)]	=	1328
[sel^#(x₁, x₂)]	=	x₂ + 0
[from(x₁)]	=	875
[sel(x₁, x₂)]	=	x₁ + 36320
[s^#(x₁)]	=	0
[nil]	=	8675
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 11405
[active^#(x₁)]	=	0
[quot^#(x₁, 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)	(72)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(108)

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

zWquot^#(X1,mark(X2))	→	zWquot^#(X1,X2)	(60)
zWquot^#(active(X1),X2)	→	zWquot^#(X1,X2)	(91)
zWquot^#(mark(X1),X2)	→	zWquot^#(X1,X2)	(87)
zWquot^#(X1,active(X2))	→	zWquot^#(X1,X2)	(44)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	5
[zWquot^#(x₁, x₂)]	=	x₁ + x₂ + 0
[minus(x₁, x₂)]	=	x₂ + 1
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	1
[0]	=	2492
[quot(x₁, x₂)]	=	3
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	12340
[sel(x₁, x₂)]	=	x₁ + 18887
[s^#(x₁)]	=	0
[nil]	=	15698
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 12342
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

zWquot^#(X1,mark(X2))	→	zWquot^#(X1,X2)	(60)
zWquot^#(active(X1),X2)	→	zWquot^#(X1,X2)	(91)
zWquot^#(mark(X1),X2)	→	zWquot^#(X1,X2)	(87)
zWquot^#(X1,active(X2))	→	zWquot^#(X1,X2)	(44)

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^#(active(X1),X2)	→	cons^#(X1,X2)	(115)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(101)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(92)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(46)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	5613
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 16393
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	1
[0]	=	8097
[quot(x₁, x₂)]	=	3
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	8517
[sel(x₁, x₂)]	=	x₁ + 24853
[s^#(x₁)]	=	0
[nil]	=	21294
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 8519
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(115)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(92)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(46)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(101)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	5
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 1
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	1
[0]	=	5
[quot(x₁, x₂)]	=	3
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	3342
[sel(x₁, x₂)]	=	x₁ + 21443
[s^#(x₁)]	=	0
[nil]	=	21294
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 3344
[active^#(x₁)]	=	0
[quot^#(x₁, 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)	(46)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(101)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

from^#(mark(X))	→	from^#(X)	(80)
from^#(active(X))	→	from^#(X)	(62)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	23105
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 13068
[zWquot(x₁, x₂)]	=	x₁ + 1
[mark^#(x₁)]	=	1
[0]	=	5
[quot(x₁, x₂)]	=	3
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	29655
[sel(x₁, x₂)]	=	x₁ + 38231
[s^#(x₁)]	=	0
[nil]	=	31608
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 29657
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

from^#(mark(X))	→	from^#(X)	(80)
from^#(active(X))	→	from^#(X)	(62)

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^#(mark(X))	→	s^#(X)	(54)
s^#(active(X))	→	s^#(X)	(49)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	17947
[zWquot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 28660
[zWquot(x₁, x₂)]	=	x₁ + 17943
[mark^#(x₁)]	=	1
[0]	=	17947
[quot(x₁, x₂)]	=	17945
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	592
[sel(x₁, x₂)]	=	x₁ + 50844
[s^#(x₁)]	=	x₁ + 0
[nil]	=	17945
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + 594
[active^#(x₁)]	=	0
[quot^#(x₁, x₂)]	=	0

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

s^#(mark(X))	→	s^#(X)	(54)
s^#(active(X))	→	s^#(X)	(49)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.