Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_iGM)

The rewrite relation of the following TRS is considered.

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

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^#(U21(tt,M,N))	→	s^#(plus(N,M))	(59)
active^#(U31(tt))	→	mark^#(0)	(60)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(61)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(x(X1,X2))	→	x^#(mark(X1),mark(X2))	(65)
mark^#(U11(X1,X2))	→	U11^#(mark(X1),X2)	(66)
active^#(x(N,0))	→	isNat^#(N)	(67)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(68)
active^#(x(N,0))	→	U31^#(isNat(N))	(69)
mark^#(and(X1,X2))	→	and^#(mark(X1),X2)	(70)
mark^#(plus(X1,X2))	→	mark^#(X2)	(71)
mark^#(plus(X1,X2))	→	plus^#(mark(X1),mark(X2))	(72)
mark^#(tt)	→	active^#(tt)	(73)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(U11(X1,X2))	→	mark^#(X1)	(75)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(s(X))	→	active^#(s(mark(X)))	(77)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(78)
mark^#(U31(X))	→	active^#(U31(mark(X)))	(79)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(80)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(82)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
s^#(mark(X))	→	s^#(X)	(84)
active^#(plus(N,0))	→	U11^#(isNat(N),N)	(85)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V1)	(86)
mark^#(x(X1,X2))	→	mark^#(X1)	(87)
active^#(x(N,0))	→	mark^#(U31(isNat(N)))	(88)
active^#(isNat(s(V1)))	→	isNat^#(V1)	(89)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(90)
U41^#(X1,X2,active(X3))	→	U41^#(X1,X2,X3)	(91)
U31^#(mark(X))	→	U31^#(X)	(92)
U41^#(X1,active(X2),X3)	→	U41^#(X1,X2,X3)	(93)
mark^#(plus(X1,X2))	→	mark^#(X1)	(94)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(95)
mark^#(U31(X))	→	U31^#(mark(X))	(96)
active^#(U41(tt,M,N))	→	x^#(N,M)	(97)
active^#(x(N,s(M)))	→	isNat^#(N)	(98)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(99)
active^#(x(N,s(M)))	→	isNat^#(M)	(100)
mark^#(U41(X1,X2,X3))	→	U41^#(mark(X1),X2,X3)	(101)
U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(102)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(105)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(106)
active^#(plus(N,s(M)))	→	and^#(isNat(M),isNat(N))	(107)
s^#(active(X))	→	s^#(X)	(108)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V2)	(109)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(111)
isNat^#(active(X))	→	isNat^#(X)	(112)
active^#(and(tt,X))	→	mark^#(X)	(113)
active^#(plus(N,s(M)))	→	U21^#(and(isNat(M),isNat(N)),M,N)	(114)
mark^#(0)	→	active^#(0)	(115)
x^#(X1,active(X2))	→	x^#(X1,X2)	(116)
active^#(isNat(x(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(117)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(119)
U41^#(active(X1),X2,X3)	→	U41^#(X1,X2,X3)	(120)
U41^#(X1,X2,mark(X3))	→	U41^#(X1,X2,X3)	(121)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(122)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(U41(tt,M,N))	→	plus^#(x(N,M),N)	(124)
U11^#(X1,active(X2))	→	U11^#(X1,X2)	(125)
active^#(plus(N,s(M)))	→	isNat^#(N)	(126)
mark^#(s(X))	→	s^#(mark(X))	(127)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(128)
and^#(X1,active(X2))	→	and^#(X1,X2)	(129)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(isNat(x(V1,V2)))	→	isNat^#(V2)	(131)
active^#(x(N,s(M)))	→	and^#(isNat(M),isNat(N))	(132)
isNat^#(mark(X))	→	isNat^#(X)	(133)
mark^#(U21(X1,X2,X3))	→	U21^#(mark(X1),X2,X3)	(134)
active^#(U11(tt,N))	→	mark^#(N)	(135)
active^#(isNat(x(V1,V2)))	→	isNat^#(V1)	(136)
active^#(plus(N,0))	→	isNat^#(N)	(137)
and^#(active(X1),X2)	→	and^#(X1,X2)	(138)
active^#(plus(N,s(M)))	→	isNat^#(M)	(139)
x^#(active(X1),X2)	→	x^#(X1,X2)	(140)
U41^#(X1,mark(X2),X3)	→	U41^#(X1,X2,X3)	(141)
active^#(isNat(x(V1,V2)))	→	and^#(isNat(V1),isNat(V2))	(142)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(143)
mark^#(x(X1,X2))	→	mark^#(X2)	(144)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(145)
active^#(x(N,s(M)))	→	U41^#(and(isNat(M),isNat(N)),M,N)	(146)
active^#(isNat(0))	→	mark^#(tt)	(147)
active^#(U21(tt,M,N))	→	plus^#(N,M)	(148)
mark^#(U31(X))	→	mark^#(X)	(149)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)
active^#(isNat(plus(V1,V2)))	→	and^#(isNat(V1),isNat(V2))	(151)
U31^#(active(X))	→	U31^#(X)	(152)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(153)
U41^#(mark(X1),X2,X3)	→	U41^#(X1,X2,X3)	(154)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(156)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(157)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
active^#(isNat(x(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(117)
active^#(and(tt,X))	→	mark^#(X)	(113)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(111)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)
mark^#(U31(X))	→	mark^#(X)	(149)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(145)
mark^#(x(X1,X2))	→	mark^#(X2)	(144)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(143)
mark^#(plus(X1,X2))	→	mark^#(X1)	(94)
active^#(x(N,0))	→	mark^#(U31(isNat(N)))	(88)
mark^#(x(X1,X2))	→	mark^#(X1)	(87)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
active^#(U11(tt,N))	→	mark^#(N)	(135)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
mark^#(U31(X))	→	active^#(U31(mark(X)))	(79)
mark^#(s(X))	→	active^#(s(mark(X)))	(77)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(U11(X1,X2))	→	mark^#(X1)	(75)
mark^#(plus(X1,X2))	→	mark^#(X2)	(71)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	36336
[U11(x₁, x₂)]	=	36336
[s(x₁)]	=	35495
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	36336
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	36336
[mark^#(x₁)]	=	36336
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[isNat(x₁)]	=	36336
[plus(x₁, x₂)]	=	36336
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	5
[U41(x₁, x₂, x₃)]	=	36336
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

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

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

mark^#(U31(X))	→	active^#(U31(mark(X)))	(79)
mark^#(s(X))	→	active^#(s(mark(X)))	(77)

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^#(plus(X1,X2))	→	mark^#(X2)	(71)
mark^#(plus(X1,X2))	→	mark^#(X1)	(94)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
active^#(U11(tt,N))	→	mark^#(N)	(135)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(143)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(111)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
mark^#(U31(X))	→	mark^#(X)	(149)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(x(X1,X2))	→	mark^#(X2)	(144)
mark^#(x(X1,X2))	→	mark^#(X1)	(87)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(and(tt,X))	→	mark^#(X)	(113)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(U11(X1,X2))	→	mark^#(X1)	(75)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
active^#(x(N,0))	→	mark^#(U31(isNat(N)))	(88)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(145)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(isNat(x(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(117)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 21878, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(0)
[x(x₁, x₂)]	=	max(x₁ + 21880, x₂ + 21881, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	19430
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 21878, 0)
[U11^#(x₁, x₂)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[U31(x₁)]	=	x₁ + 591
[U41^#(x₁, x₂, x₃)]	=	max(0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	max(0)
[tt]	=	19428
[U41(x₁, x₂, x₃)]	=	max(x₁ + 2451, x₂ + 21881, x₃ + 21880, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(0)

together with the usable rules

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

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

mark^#(plus(X1,X2))	→	mark^#(X2)	(71)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(143)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(111)
mark^#(U31(X))	→	mark^#(X)	(149)
mark^#(x(X1,X2))	→	mark^#(X2)	(144)
mark^#(x(X1,X2))	→	mark^#(X1)	(87)
mark^#(U11(X1,X2))	→	mark^#(X1)	(75)
active^#(x(N,0))	→	mark^#(U31(isNat(N)))	(88)

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^#(plus(X1,X2))	→	mark^#(X1)	(94)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
active^#(U11(tt,N))	→	mark^#(N)	(135)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(and(tt,X))	→	mark^#(X)	(113)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(145)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(isNat(x(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(117)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₂ + 38781, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[plus^#(x₁, x₂)]	=	max(0)
[x(x₁, x₂)]	=	max(x₁ + 38781, x₂ + 16336, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	22325
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 5969
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 38781, 0)
[U11^#(x₁, x₂)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[U31(x₁)]	=	x₁ + 32812
[U41^#(x₁, x₂, x₃)]	=	max(0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	max(0)
[tt]	=	17525
[U41(x₁, x₂, x₃)]	=	max(x₂ + 16336, x₃ + 38781, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(0)

together with the usable rules

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

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

active^#(and(tt,X))	→	mark^#(X)	(113)
active^#(isNat(x(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(117)

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^#(plus(X1,X2))	→	mark^#(X1)	(94)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
active^#(U11(tt,N))	→	mark^#(N)	(135)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(145)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	9049
[U11(x₁, x₂)]	=	9049
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	9049
[mark^#(x₁)]	=	9049
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[isNat(x₁)]	=	9049
[plus(x₁, x₂)]	=	9049
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	0
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	9049
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

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

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

mark^#(and(X1,X2))

→

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

(145)

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^#(plus(X1,X2))	→	mark^#(X1)	(94)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
active^#(U11(tt,N))	→	mark^#(N)	(135)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(U21)	=	4	status(U21)	=	[2, 3, 1]	list-extension(U21)	=	Lex
prec(U11)	=	3	status(U11)	=	[2, 1]	list-extension(U11)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(isNat^#)	=	0	status(isNat^#)	=	[]	list-extension(isNat^#)	=	Lex
prec(and)	=	3	status(and)	=	[2, 1]	list-extension(and)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[]	list-extension(plus^#)	=	Lex
prec(x)	=	5	status(x)	=	[2, 1]	list-extension(x)	=	Lex
prec(mark^#)	=	2	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	0	status(x^#)	=	[2, 1]	list-extension(x^#)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[1]	list-extension(isNat)	=	Lex
prec(plus)	=	4	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[1, 2]	list-extension(U11^#)	=	Lex
prec(U31)	=	4	status(U31)	=	[]	list-extension(U31)	=	Lex
prec(U41^#)	=	0	status(U41^#)	=	[1, 2, 3]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[3, 1]	list-extension(U21^#)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U41)	=	5	status(U41)	=	[2, 3, 1]	list-extension(U41)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[]	list-extension(U31^#)	=	Lex
prec(and^#)	=	0	status(and^#)	=	[2, 1]	list-extension(and^#)	=	Lex

and the following Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U31(x₁)]	=	0
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₃ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

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

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

mark^#(plus(X1,X2))	→	mark^#(X1)	(94)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(104)
active^#(U41(tt,M,N))	→	mark^#(plus(x(N,M),N))	(123)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(110)
active^#(U11(tt,N))	→	mark^#(N)	(135)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(64)
mark^#(U41(X1,X2,X3))	→	active^#(U41(mark(X1),X2,X3))	(155)
mark^#(s(X))	→	mark^#(X)	(74)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(130)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(81)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(76)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(103)
mark^#(and(X1,X2))	→	mark^#(X1)	(83)
mark^#(isNat(X))	→	active^#(isNat(X))	(63)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(62)
active^#(x(N,s(M)))	→	mark^#(U41(and(isNat(M),isNat(N)),M,N))	(118)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(150)

could be deleted.

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

and^#(mark(X1),X2)	→	and^#(X1,X2)	(106)
and^#(active(X1),X2)	→	and^#(X1,X2)	(138)
and^#(X1,active(X2))	→	and^#(X1,X2)	(129)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(119)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	1
[U11(x₁, x₂)]	=	1
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	0
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 3
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 2
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	x₂ + 0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

and^#(X1,active(X2))	→	and^#(X1,X2)	(129)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(119)

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

and^#(active(X1),X2)	→	and^#(X1,X2)	(138)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(106)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	2
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 2
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 2
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	x₁ + 0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

and^#(active(X1),X2)	→	and^#(X1,X2)	(138)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(106)

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

U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(102)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(99)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(90)
U11^#(X1,active(X2))	→	U11^#(X1,X2)	(125)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	3
[U11(x₁, x₂)]	=	1
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	x₁ + x₂ + 0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(102)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(99)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(90)
U11^#(X1,active(X2))	→	U11^#(X1,X2)	(125)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

s^#(active(X))	→	s^#(X)	(108)
s^#(mark(X))	→	s^#(X)	(84)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	10949
[U11(x₁, x₂)]	=	6447
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	13856
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 8028
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 21807
[isNat(x₁)]	=	x₁ + 21804
[plus(x₁, x₂)]	=	x₁ + 3
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	6773
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 3103
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

s^#(active(X))	→	s^#(X)	(108)
s^#(mark(X))	→	s^#(X)	(84)

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

U31^#(active(X))	→	U31^#(X)	(152)
U31^#(mark(X))	→	U31^#(X)	(92)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	1
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	3
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 4
[U31^#(x₁)]	=	x₁ + 0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

U31^#(active(X))	→	U31^#(X)	(152)
U31^#(mark(X))	→	U31^#(X)	(92)

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

U41^#(mark(X1),X2,X3)	→	U41^#(X1,X2,X3)	(154)
U41^#(X1,active(X2),X3)	→	U41^#(X1,X2,X3)	(93)
U41^#(X1,X2,active(X3))	→	U41^#(X1,X2,X3)	(91)
U41^#(X1,mark(X2),X3)	→	U41^#(X1,X2,X3)	(141)
U41^#(X1,X2,mark(X3))	→	U41^#(X1,X2,X3)	(121)
U41^#(active(X1),X2,X3)	→	U41^#(X1,X2,X3)	(120)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	1
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

U41^#(mark(X1),X2,X3)	→	U41^#(X1,X2,X3)	(154)
U41^#(X1,active(X2),X3)	→	U41^#(X1,X2,X3)	(93)
U41^#(X1,X2,active(X3))	→	U41^#(X1,X2,X3)	(91)
U41^#(X1,mark(X2),X3)	→	U41^#(X1,X2,X3)	(141)
U41^#(X1,X2,mark(X3))	→	U41^#(X1,X2,X3)	(121)
U41^#(active(X1),X2,X3)	→	U41^#(X1,X2,X3)	(120)

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

isNat^#(active(X))	→	isNat^#(X)	(112)
isNat^#(mark(X))	→	isNat^#(X)	(133)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	2
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	1
[isNat^#(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 3
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

isNat^#(active(X))	→	isNat^#(X)	(112)
isNat^#(mark(X))	→	isNat^#(X)	(133)

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

U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(105)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(82)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(80)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(78)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(128)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(61)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	1
[U11(x₁, x₂)]	=	1
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	2
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 3
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(105)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(82)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(78)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(61)

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

U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(80)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(128)

1.1.8.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	2488
[U11(x₁, x₂)]	=	410
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1142
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 1
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4513
[isNat(x₁)]	=	x₁ + 2101
[plus(x₁, x₂)]	=	x₁ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	x₁ + 0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 28
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(80)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(128)

could be deleted.

1.1.8.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

x^#(mark(X1),X2)	→	x^#(X1,X2)	(156)
x^#(X1,active(X2))	→	x^#(X1,X2)	(116)
x^#(active(X1),X2)	→	x^#(X1,X2)	(140)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(68)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	19314
[U11(x₁, x₂)]	=	23959
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 15155
[mark^#(x₁)]	=	0
[0]	=	37883
[x^#(x₁, x₂)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 54021
[isNat(x₁)]	=	x₁ + 16136
[plus(x₁, x₂)]	=	x₁ + 8752
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	x₂ + 12692
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)

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

x^#(X1,active(X2))	→	x^#(X1,X2)	(116)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(68)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

x^#(mark(X1),X2)	→	x^#(X1,X2)	(156)
x^#(active(X1),X2)	→	x^#(X1,X2)	(140)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₁ + 44033
[s(x₁)]	=	x₁ + 29823
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	13862
[plus^#(x₁, x₂)]	=	0
[x(x₁, x₂)]	=	x₂ + 16019
[mark^#(x₁)]	=	0
[0]	=	10026
[x^#(x₁, x₂)]	=	x₁ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 73356
[isNat(x₁)]	=	x₁ + 3901
[plus(x₁, x₂)]	=	x₂ + 2061
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	x₁ + 14809
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	29321
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + 13780
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

x^#(mark(X1),X2)	→	x^#(X1,X2)	(156)
x^#(active(X1),X2)	→	x^#(X1,X2)	(140)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

plus^#(X1,active(X2))	→	plus^#(X1,X2)	(157)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(153)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(95)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(122)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + 2
[U11(x₁, x₂)]	=	x₁ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[plus^#(x₁, x₂)]	=	x₁ + 0
[x(x₁, x₂)]	=	x₁ + 2
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 2
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₃ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

plus^#(active(X1),X2)	→	plus^#(X1,X2)	(95)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(122)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(X1,active(X2))	→	plus^#(X1,X2)	(157)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(153)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + 22315
[U11(x₁, x₂)]	=	x₁ + x₂ + 47469
[s(x₁)]	=	3162
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 17603
[plus^#(x₁, x₂)]	=	x₂ + 0
[x(x₁, x₂)]	=	x₁ + x₂ + 7135
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 47476
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₂ + 25
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 5
[U31(x₁)]	=	x₁ + 1602
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 11413
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

plus^#(X1,active(X2))	→	plus^#(X1,X2)	(157)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(153)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.