Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nosorts_noand_iGM)

The rewrite relation of the following TRS is considered.

active(U11(tt,M,N))	→	mark(U12(tt,M,N))	(1)
active(U12(tt,M,N))	→	mark(s(plus(N,M)))	(2)
active(U21(tt,M,N))	→	mark(U22(tt,M,N))	(3)
active(U22(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
active(plus(N,0))	→	mark(N)	(5)
active(plus(N,s(M)))	→	mark(U11(tt,M,N))	(6)
active(x(N,0))	→	mark(0)	(7)
active(x(N,s(M)))	→	mark(U21(tt,M,N))	(8)
mark(U11(X1,X2,X3))	→	active(U11(mark(X1),X2,X3))	(9)
mark(tt)	→	active(tt)	(10)
mark(U12(X1,X2,X3))	→	active(U12(mark(X1),X2,X3))	(11)
mark(s(X))	→	active(s(mark(X)))	(12)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(14)
mark(U22(X1,X2,X3))	→	active(U22(mark(X1),X2,X3))	(15)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(16)
mark(0)	→	active(0)	(17)
U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
x(mark(X1),X2)	→	x(X1,X2)	(48)
x(X1,mark(X2))	→	x(X1,X2)	(49)
x(active(X1),X2)	→	x(X1,X2)	(50)
x(X1,active(X2))	→	x(X1,X2)	(51)

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^#(U12(tt,M,N))	→	s^#(plus(N,M))	(52)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(53)
U11^#(X1,X2,active(X3))	→	U11^#(X1,X2,X3)	(54)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
active^#(x(N,s(M)))	→	mark^#(U21(tt,M,N))	(56)
active^#(plus(N,0))	→	mark^#(N)	(57)
active^#(x(N,0))	→	mark^#(0)	(58)
U11^#(X1,X2,mark(X3))	→	U11^#(X1,X2,X3)	(59)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(60)
active^#(U22(tt,M,N))	→	x^#(N,M)	(61)
U22^#(X1,X2,mark(X3))	→	U22^#(X1,X2,X3)	(62)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(63)
active^#(U22(tt,M,N))	→	mark^#(plus(x(N,M),N))	(64)
U12^#(X1,active(X2),X3)	→	U12^#(X1,X2,X3)	(65)
U11^#(mark(X1),X2,X3)	→	U11^#(X1,X2,X3)	(66)
x^#(active(X1),X2)	→	x^#(X1,X2)	(67)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
mark^#(x(X1,X2))	→	mark^#(X2)	(69)
s^#(mark(X))	→	s^#(X)	(70)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(71)
mark^#(x(X1,X2))	→	x^#(mark(X1),mark(X2))	(72)
U12^#(X1,X2,mark(X3))	→	U12^#(X1,X2,X3)	(73)
active^#(x(N,s(M)))	→	U21^#(tt,M,N)	(74)
U12^#(X1,mark(X2),X3)	→	U12^#(X1,X2,X3)	(75)
U12^#(active(X1),X2,X3)	→	U12^#(X1,X2,X3)	(76)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(77)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(78)
U22^#(X1,X2,active(X3))	→	U22^#(X1,X2,X3)	(79)
U11^#(active(X1),X2,X3)	→	U11^#(X1,X2,X3)	(80)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(U22(X1,X2,X3))	→	mark^#(X1)	(82)
mark^#(U11(X1,X2,X3))	→	U11^#(mark(X1),X2,X3)	(83)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(84)
mark^#(U22(X1,X2,X3))	→	U22^#(mark(X1),X2,X3)	(85)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(86)
mark^#(s(X))	→	active^#(s(mark(X)))	(87)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(88)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
U22^#(active(X1),X2,X3)	→	U22^#(X1,X2,X3)	(91)
mark^#(0)	→	active^#(0)	(92)
U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(93)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(plus(X1,X2))	→	mark^#(X1)	(95)
U22^#(X1,active(X2),X3)	→	U22^#(X1,X2,X3)	(96)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(97)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(98)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
mark^#(s(X))	→	mark^#(X)	(100)
active^#(U22(tt,M,N))	→	plus^#(x(N,M),N)	(101)
U12^#(X1,X2,active(X3))	→	U12^#(X1,X2,X3)	(102)
mark^#(tt)	→	active^#(tt)	(103)
active^#(U11(tt,M,N))	→	U12^#(tt,M,N)	(104)
U12^#(mark(X1),X2,X3)	→	U12^#(X1,X2,X3)	(105)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
s^#(active(X))	→	s^#(X)	(107)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(108)
mark^#(x(X1,X2))	→	mark^#(X1)	(109)
x^#(X1,active(X2))	→	x^#(X1,X2)	(110)
mark^#(s(X))	→	s^#(mark(X))	(111)
mark^#(plus(X1,X2))	→	plus^#(mark(X1),mark(X2))	(112)
active^#(U21(tt,M,N))	→	U22^#(tt,M,N)	(113)
mark^#(U12(X1,X2,X3))	→	U12^#(mark(X1),X2,X3)	(114)
mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
mark^#(U21(X1,X2,X3))	→	U21^#(mark(X1),X2,X3)	(116)
mark^#(plus(X1,X2))	→	mark^#(X2)	(117)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(118)
active^#(U12(tt,M,N))	→	plus^#(N,M)	(119)
active^#(U12(tt,M,N))	→	mark^#(s(plus(N,M)))	(120)
U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(121)
U22^#(mark(X1),X2,X3)	→	U22^#(X1,X2,X3)	(122)
active^#(plus(N,s(M)))	→	U11^#(tt,M,N)	(123)
U22^#(X1,mark(X2),X3)	→	U22^#(X1,X2,X3)	(124)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(125)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)
mark^#(s(X))	→	active^#(s(mark(X)))	(87)
active^#(U12(tt,M,N))	→	mark^#(s(plus(N,M)))	(120)
mark^#(U22(X1,X2,X3))	→	mark^#(X1)	(82)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(plus(X1,X2))	→	mark^#(X2)	(117)
mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
mark^#(x(X1,X2))	→	mark^#(X1)	(109)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(108)
mark^#(x(X1,X2))	→	mark^#(X2)	(69)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
active^#(U22(tt,M,N))	→	mark^#(plus(x(N,M),N))	(64)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(60)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
mark^#(s(X))	→	mark^#(X)	(100)
active^#(plus(N,0))	→	mark^#(N)	(57)
active^#(x(N,s(M)))	→	mark^#(U21(tt,M,N))	(56)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
mark^#(plus(X1,X2))	→	mark^#(X1)	(95)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	9727
[U11(x₁, x₂, x₃)]	=	9727
[s(x₁)]	=	1
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	9727
[x(x₁, x₂)]	=	9727
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	9727
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[plus(x₁, x₂)]	=	9727
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	2
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U22(x₁, x₂, x₃)]	=	9727

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

mark^#(s(X))

→

active^#(s(mark(X)))

(87)

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^#(U22(tt,M,N))	→	mark^#(plus(x(N,M),N))	(64)
mark^#(U22(X1,X2,X3))	→	mark^#(X1)	(82)
mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(x(N,s(M)))	→	mark^#(U21(tt,M,N))	(56)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(x(X1,X2))	→	mark^#(X2)	(69)
mark^#(x(X1,X2))	→	mark^#(X1)	(109)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
active^#(plus(N,0))	→	mark^#(N)	(57)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(60)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
mark^#(s(X))	→	mark^#(X)	(100)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(108)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
mark^#(plus(X1,X2))	→	mark^#(X2)	(117)
mark^#(plus(X1,X2))	→	mark^#(X1)	(95)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)
active^#(U12(tt,M,N))	→	mark^#(s(plus(N,M)))	(120)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₁ + 36470, x₂ + 42324, x₃ + 36469, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 30614, x₂ + 36469, x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(0)
[U12(x₁, x₂, x₃)]	=	max(x₁ + 30613, x₂ + 36469, x₃ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 36469, x₂ + 42324, 0)
[U12^#(x₁, x₂, x₃)]	=	max(0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	36470
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 36469, 0)
[U11^#(x₁, x₂, x₃)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	max(0)
[U22^#(x₁, x₂, x₃)]	=	max(0)
[tt]	=	5854
[U22(x₁, x₂, x₃)]	=	max(x₁ + 28101, x₂ + 42324, x₃ + 36469, 0)

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
active(U22(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
mark(U22(X1,X2,X3))	→	active(U22(mark(X1),X2,X3))	(15)
active(x(N,s(M)))	→	mark(U21(tt,M,N))	(8)
active(U11(tt,M,N))	→	mark(U12(tt,M,N))	(1)
active(U21(tt,M,N))	→	mark(U22(tt,M,N))	(3)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(16)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
mark(0)	→	active(0)	(17)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
active(plus(N,0))	→	mark(N)	(5)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
active(x(N,0))	→	mark(0)	(7)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(14)
s(active(X))	→	s(X)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
mark(U12(X1,X2,X3))	→	active(U12(mark(X1),X2,X3))	(11)
mark(U11(X1,X2,X3))	→	active(U11(mark(X1),X2,X3))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
active(plus(N,s(M)))	→	mark(U11(tt,M,N))	(6)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)
active(U12(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

mark^#(U22(X1,X2,X3))	→	mark^#(X1)	(82)
mark^#(x(X1,X2))	→	mark^#(X2)	(69)
mark^#(x(X1,X2))	→	mark^#(X1)	(109)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(60)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(108)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(plus(X1,X2))	→	mark^#(X2)	(117)

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^#(U22(tt,M,N))	→	mark^#(plus(x(N,M),N))	(64)
mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(x(N,s(M)))	→	mark^#(U21(tt,M,N))	(56)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
active^#(plus(N,0))	→	mark^#(N)	(57)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
mark^#(s(X))	→	mark^#(X)	(100)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
mark^#(plus(X1,X2))	→	mark^#(X1)	(95)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)
active^#(U12(tt,M,N))	→	mark^#(s(plus(N,M)))	(120)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(U21)	=	2	status(U21)	=	[3, 2, 1]	list-extension(U21)	=	Lex
prec(U11)	=	1	status(U11)	=	[3, 2, 1]	list-extension(U11)	=	Lex
prec(s)	=	0	status(s)	=	[1]	list-extension(s)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[2, 1]	list-extension(plus^#)	=	Lex
prec(U12)	=	1	status(U12)	=	[3, 2, 1]	list-extension(U12)	=	Lex
prec(x)	=	2	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[1, 2, 3]	list-extension(U12^#)	=	Lex
prec(mark^#)	=	3	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(plus)	=	1	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[2, 1, 3]	list-extension(U11^#)	=	Lex
prec(active^#)	=	3	status(active^#)	=	[1]	list-extension(active^#)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[3, 2, 1]	list-extension(U21^#)	=	Lex
prec(U22^#)	=	0	status(U22^#)	=	[2, 3, 1]	list-extension(U22^#)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U22)	=	2	status(U22)	=	[3, 2, 1]	list-extension(U22)	=	Lex

and the following Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U12(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U12^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U22^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[tt]	=	0
[U22(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
active(U22(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
mark(U22(X1,X2,X3))	→	active(U22(mark(X1),X2,X3))	(15)
active(x(N,s(M)))	→	mark(U21(tt,M,N))	(8)
active(U11(tt,M,N))	→	mark(U12(tt,M,N))	(1)
active(U21(tt,M,N))	→	mark(U22(tt,M,N))	(3)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(16)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
mark(0)	→	active(0)	(17)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
active(plus(N,0))	→	mark(N)	(5)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
active(x(N,0))	→	mark(0)	(7)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(14)
s(active(X))	→	s(X)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
mark(U12(X1,X2,X3))	→	active(U12(mark(X1),X2,X3))	(11)
mark(U11(X1,X2,X3))	→	active(U11(mark(X1),X2,X3))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
active(plus(N,s(M)))	→	mark(U11(tt,M,N))	(6)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)
active(U12(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

active^#(U22(tt,M,N))	→	mark^#(plus(x(N,M),N))	(64)
active^#(x(N,s(M)))	→	mark^#(U21(tt,M,N))	(56)
active^#(plus(N,0))	→	mark^#(N)	(57)
mark^#(s(X))	→	mark^#(X)	(100)
mark^#(plus(X1,X2))	→	mark^#(X1)	(95)
active^#(U12(tt,M,N))	→	mark^#(s(plus(N,M)))	(120)

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^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	4296
[U11(x₁, x₂, x₃)]	=	4295
[s(x₁)]	=	15593
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	4295
[x(x₁, x₂)]	=	x₂ + 4296
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 5432
[0]	=	19891
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	19890
[plus(x₁, x₂)]	=	4296
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	9727
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	19891
[U22(x₁, x₂, x₃)]	=	4295

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(68)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(55)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(126)

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

mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)
active^#(plus(N,s(M)))	→	mark^#(U11(tt,M,N))	(89)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	0
[U11(x₁, x₂, x₃)]	=	0
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	9727
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	x₁ + 9727
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U22(x₁, x₂, x₃)]	=	0

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
active(U22(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
mark(U22(X1,X2,X3))	→	active(U22(mark(X1),X2,X3))	(15)
active(x(N,s(M)))	→	mark(U21(tt,M,N))	(8)
active(U11(tt,M,N))	→	mark(U12(tt,M,N))	(1)
active(U21(tt,M,N))	→	mark(U22(tt,M,N))	(3)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(16)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
mark(0)	→	active(0)	(17)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
active(plus(N,0))	→	mark(N)	(5)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
active(x(N,0))	→	mark(0)	(7)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(14)
s(active(X))	→	s(X)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
mark(U12(X1,X2,X3))	→	active(U12(mark(X1),X2,X3))	(11)
mark(U11(X1,X2,X3))	→	active(U11(mark(X1),X2,X3))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
active(plus(N,s(M)))	→	mark(U11(tt,M,N))	(6)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)
active(U12(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

active^#(plus(N,s(M)))

→

mark^#(U11(tt,M,N))

(89)

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

mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 9216
[U11(x₁, x₂, x₃)]	=	9215
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	4608
[x(x₁, x₂)]	=	13824
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	9727
[0]	=	9217
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4608
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 512
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	24234
[U22(x₁, x₂, x₃)]	=	4609

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

mark^#(U22(X1,X2,X3))	→	active^#(U22(mark(X1),X2,X3))	(115)
active^#(U21(tt,M,N))	→	mark^#(U22(tt,M,N))	(90)
mark^#(U12(X1,X2,X3))	→	active^#(U12(mark(X1),X2,X3))	(94)

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^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)

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

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 3621
[U11(x₁, x₂, x₃)]	=	x₃ + 22631
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	11316
[x(x₁, x₂)]	=	14937
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	9217
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 11316
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	24234
[U22(x₁, x₂, x₃)]	=	15908

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

active^#(U11(tt,M,N))	→	mark^#(U12(tt,M,N))	(99)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(106)

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 0 components.

The 2^nd component contains the pair

U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(93)
U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(121)
U11^#(active(X1),X2,X3)	→	U11^#(X1,X2,X3)	(80)
U11^#(mark(X1),X2,X3)	→	U11^#(X1,X2,X3)	(66)
U11^#(X1,X2,mark(X3))	→	U11^#(X1,X2,X3)	(59)
U11^#(X1,X2,active(X3))	→	U11^#(X1,X2,X3)	(54)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 2103
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	26785
[x(x₁, x₂)]	=	5857
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	9217
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U22(x₁, x₂, x₃)]	=	15908

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U11^#(active(X1),X2,X3)	→	U11^#(X1,X2,X3)	(80)
U11^#(mark(X1),X2,X3)	→	U11^#(X1,X2,X3)	(66)
U11^#(X1,X2,mark(X3))	→	U11^#(X1,X2,X3)	(59)
U11^#(X1,X2,active(X3))	→	U11^#(X1,X2,X3)	(54)

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

U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(121)
U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(93)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 2246
[U11(x₁, x₂, x₃)]	=	x₃ + 1441
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	2632
[x(x₁, x₂)]	=	21903
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	19272
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2633
[plus(x₁, x₂)]	=	2631
[U11^#(x₁, x₂, x₃)]	=	x₂ + 0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	21314
[U22(x₁, x₂, x₃)]	=	5263

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(121)
U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(93)

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

s^#(mark(X))	→	s^#(X)	(70)
s^#(active(X))	→	s^#(X)	(107)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 20694
[U11(x₁, x₂, x₃)]	=	x₃ + 1898
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	34052
[x(x₁, x₂)]	=	85605
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	51554
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 34053
[plus(x₁, x₂)]	=	34051
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	39502
[U22(x₁, x₂, x₃)]	=	68103

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

s^#(mark(X))	→	s^#(X)	(70)
s^#(active(X))	→	s^#(X)	(107)

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

U12^#(active(X1),X2,X3)	→	U12^#(X1,X2,X3)	(76)
U12^#(X1,mark(X2),X3)	→	U12^#(X1,X2,X3)	(75)
U12^#(X1,X2,mark(X3))	→	U12^#(X1,X2,X3)	(73)
U12^#(X1,active(X2),X3)	→	U12^#(X1,X2,X3)	(65)
U12^#(mark(X1),X2,X3)	→	U12^#(X1,X2,X3)	(105)
U12^#(X1,X2,active(X3))	→	U12^#(X1,X2,X3)	(102)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 1
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	9994
[x(x₁, x₂)]	=	3
[U12^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	57076
[U22(x₁, x₂, x₃)]	=	32092

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U12^#(active(X1),X2,X3)	→	U12^#(X1,X2,X3)	(76)
U12^#(X1,mark(X2),X3)	→	U12^#(X1,X2,X3)	(75)
U12^#(X1,X2,mark(X3))	→	U12^#(X1,X2,X3)	(73)
U12^#(X1,active(X2),X3)	→	U12^#(X1,X2,X3)	(65)
U12^#(mark(X1),X2,X3)	→	U12^#(X1,X2,X3)	(105)
U12^#(X1,X2,active(X3))	→	U12^#(X1,X2,X3)	(102)

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

U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(88)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(118)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(78)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(77)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(98)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(53)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 1
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	16960
[x(x₁, x₂)]	=	3
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U22(x₁, x₂, x₃)]	=	26357

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(88)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(118)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(78)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(77)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(98)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(53)

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

plus^#(active(X1),X2)	→	plus^#(X1,X2)	(125)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(84)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(71)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(63)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 17724
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[U12(x₁, x₂, x₃)]	=	25645
[x(x₁, x₂)]	=	3
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U22(x₁, x₂, x₃)]	=	26964

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

plus^#(active(X1),X2)	→	plus^#(X1,X2)	(125)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(84)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(71)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(63)

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

x^#(mark(X1),X2)	→	x^#(X1,X2)	(86)
x^#(X1,active(X2))	→	x^#(X1,X2)	(110)
x^#(active(X1),X2)	→	x^#(X1,X2)	(67)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(97)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 1
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	29192
[x(x₁, x₂)]	=	13521
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	39004
[x^#(x₁, x₂)]	=	x₁ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U22(x₁, x₂, x₃)]	=	3

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

x^#(mark(X1),X2)	→	x^#(X1,X2)	(86)
x^#(active(X1),X2)	→	x^#(X1,X2)	(67)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

x^#(X1,mark(X2))	→	x^#(X1,X2)	(97)
x^#(X1,active(X2))	→	x^#(X1,X2)	(110)

1.1.7.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 10867
[U11(x₁, x₂, x₃)]	=	x₃ + 1
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	7037
[x(x₁, x₂)]	=	17904
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	39119
[x^#(x₁, x₂)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 7038
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	0
[tt]	=	40807
[U22(x₁, x₂, x₃)]	=	28922

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

x^#(X1,mark(X2))	→	x^#(X1,X2)	(97)
x^#(X1,active(X2))	→	x^#(X1,X2)	(110)

could be deleted.

1.1.7.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

U22^#(X1,mark(X2),X3)	→	U22^#(X1,X2,X3)	(124)
U22^#(active(X1),X2,X3)	→	U22^#(X1,X2,X3)	(91)
U22^#(mark(X1),X2,X3)	→	U22^#(X1,X2,X3)	(122)
U22^#(X1,X2,active(X3))	→	U22^#(X1,X2,X3)	(79)
U22^#(X1,X2,mark(X3))	→	U22^#(X1,X2,X3)	(62)
U22^#(X1,active(X2),X3)	→	U22^#(X1,X2,X3)	(96)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 1
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	2
[x(x₁, x₂)]	=	3
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[tt]	=	8128
[U22(x₁, x₂, x₃)]	=	28118

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U22^#(active(X1),X2,X3)	→	U22^#(X1,X2,X3)	(91)
U22^#(mark(X1),X2,X3)	→	U22^#(X1,X2,X3)	(122)
U22^#(X1,X2,active(X3))	→	U22^#(X1,X2,X3)	(79)
U22^#(X1,X2,mark(X3))	→	U22^#(X1,X2,X3)	(62)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U22^#(X1,active(X2),X3)	→	U22^#(X1,X2,X3)	(96)
U22^#(X1,mark(X2),X3)	→	U22^#(X1,X2,X3)	(124)

1.1.8.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[U11(x₁, x₂, x₃)]	=	x₃ + 2089
[s(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[U12(x₁, x₂, x₃)]	=	39724
[x(x₁, x₂)]	=	3
[U12^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	9590
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[plus(x₁, x₂)]	=	1
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[U22^#(x₁, x₂, x₃)]	=	x₂ + 0
[tt]	=	57205
[U22(x₁, x₂, x₃)]	=	19456

together with the usable rules

U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(18)
x(active(X1),X2)	→	x(X1,X2)	(50)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(21)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(36)
U12(X1,X2,mark(X3))	→	U12(X1,X2,X3)	(26)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(19)
plus(mark(X1),X2)	→	plus(X1,X2)	(32)
U12(active(X1),X2,X3)	→	U12(X1,X2,X3)	(27)
plus(active(X1),X2)	→	plus(X1,X2)	(34)
U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(22)
U12(X1,active(X2),X3)	→	U12(X1,X2,X3)	(28)
U22(X1,X2,mark(X3))	→	U22(X1,X2,X3)	(44)
plus(X1,mark(X2))	→	plus(X1,X2)	(33)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(39)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(20)
U12(X1,mark(X2),X3)	→	U12(X1,X2,X3)	(25)
x(X1,mark(X2))	→	x(X1,X2)	(49)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
U22(active(X1),X2,X3)	→	U22(X1,X2,X3)	(45)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(23)
U12(mark(X1),X2,X3)	→	U12(X1,X2,X3)	(24)
x(X1,active(X2))	→	x(X1,X2)	(51)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(40)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(38)
x(mark(X1),X2)	→	x(X1,X2)	(48)
U22(X1,X2,active(X3))	→	U22(X1,X2,X3)	(47)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(37)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(41)
U22(mark(X1),X2,X3)	→	U22(X1,X2,X3)	(42)
U22(X1,active(X2),X3)	→	U22(X1,X2,X3)	(46)
plus(X1,active(X2))	→	plus(X1,X2)	(35)
U12(X1,X2,active(X3))	→	U12(X1,X2,X3)	(29)
U22(X1,mark(X2),X3)	→	U22(X1,X2,X3)	(43)

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

U22^#(X1,active(X2),X3)	→	U22^#(X1,X2,X3)	(96)
U22^#(X1,mark(X2),X3)	→	U22^#(X1,X2,X3)	(124)

could be deleted.

1.1.8.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.