Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_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(and(tt,X))	→	mark(X)	(3)
active(isNat(0))	→	mark(tt)	(4)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
mark(tt)	→	active(tt)	(10)
mark(U21(X1,X2,X3))	→	active(U21(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(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
mark(isNat(X))	→	active(isNat(X))	(15)
mark(0)	→	active(0)	(16)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
s(mark(X))	→	s(X)	(27)
s(active(X))	→	s(X)	(28)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
and(mark(X1),X2)	→	and(X1,X2)	(33)
and(X1,mark(X2))	→	and(X1,X2)	(34)
and(active(X1),X2)	→	and(X1,X2)	(35)
and(X1,active(X2))	→	and(X1,X2)	(36)
isNat(mark(X))	→	isNat(X)	(37)
isNat(active(X))	→	isNat(X)	(38)

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))	(39)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(41)
mark^#(tt)	→	active^#(tt)	(42)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(43)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(44)
s^#(active(X))	→	s^#(X)	(45)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(47)
active^#(U11(tt,N))	→	mark^#(N)	(48)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(49)
active^#(plus(N,s(M)))	→	isNat^#(N)	(50)
U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(51)
active^#(isNat(plus(V1,V2)))	→	and^#(isNat(V1),isNat(V2))	(52)
isNat^#(mark(X))	→	isNat^#(X)	(53)
mark^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(plus(N,s(M)))	→	U21^#(and(isNat(M),isNat(N)),M,N)	(55)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V2)	(56)
mark^#(0)	→	active^#(0)	(57)
mark^#(plus(X1,X2))	→	mark^#(X2)	(58)
active^#(isNat(s(V1)))	→	isNat^#(V1)	(59)
mark^#(plus(X1,X2))	→	plus^#(mark(X1),mark(X2))	(60)
active^#(plus(N,s(M)))	→	isNat^#(M)	(61)
mark^#(s(X))	→	mark^#(X)	(62)
mark^#(s(X))	→	s^#(mark(X))	(63)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(64)
mark^#(plus(X1,X2))	→	mark^#(X1)	(65)
U11^#(X1,active(X2))	→	U11^#(X1,X2)	(66)
active^#(plus(N,s(M)))	→	and^#(isNat(M),isNat(N))	(67)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(69)
active^#(and(tt,X))	→	mark^#(X)	(70)
and^#(X1,active(X2))	→	and^#(X1,X2)	(71)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(72)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(73)
isNat^#(active(X))	→	isNat^#(X)	(74)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V1)	(75)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(plus(N,0))	→	U11^#(isNat(N),N)	(77)
and^#(active(X1),X2)	→	and^#(X1,X2)	(78)
s^#(mark(X))	→	s^#(X)	(79)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(s(X))	→	active^#(s(mark(X)))	(81)
active^#(plus(N,0))	→	isNat^#(N)	(82)
mark^#(and(X1,X2))	→	and^#(mark(X1),X2)	(83)
active^#(isNat(0))	→	mark^#(tt)	(84)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(86)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(87)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(89)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(90)
mark^#(U11(X1,X2))	→	mark^#(X1)	(91)
active^#(U21(tt,M,N))	→	plus^#(N,M)	(92)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(93)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(94)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)
mark^#(U11(X1,X2))	→	U11^#(mark(X1),X2)	(96)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(97)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(98)
mark^#(U21(X1,X2,X3))	→	U21^#(mark(X1),X2,X3)	(99)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

active^#(and(tt,X))	→	mark^#(X)	(70)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	mark^#(X1)	(65)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(94)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(93)
mark^#(s(X))	→	mark^#(X)	(62)
mark^#(U11(X1,X2))	→	mark^#(X1)	(91)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(plus(X1,X2))	→	mark^#(X2)	(58)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(86)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(87)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(isNat(X))	→	active^#(isNat(X))	(54)
mark^#(s(X))	→	active^#(s(mark(X)))	(81)
active^#(U11(tt,N))	→	mark^#(N)	(48)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)

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

mark^#(s(X))

→

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

(81)

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^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(94)
active^#(U11(tt,N))	→	mark^#(N)	(48)
active^#(and(tt,X))	→	mark^#(X)	(70)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(86)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(s(X))	→	mark^#(X)	(62)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(87)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(U11(X1,X2))	→	mark^#(X1)	(91)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	mark^#(X2)	(58)
mark^#(plus(X1,X2))	→	mark^#(X1)	(65)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(93)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 677
[U11(x₁, x₂)]	=	x₁ + x₂ + 841
[s(x₁)]	=	x₁ + 591
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	756
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 86
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
active(isNat(0))	→	mark(tt)	(4)
mark(isNat(X))	→	active(isNat(X))	(15)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(and(tt,X))	→	mark(X)	(3)
mark(0)	→	active(0)	(16)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
and(mark(X1),X2)	→	and(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)
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^#(U11(tt,N))	→	mark^#(N)	(48)
active^#(plus(N,0))	→	mark^#(U11(isNat(N),N))	(86)
mark^#(s(X))	→	mark^#(X)	(62)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(87)
mark^#(U11(X1,X2))	→	mark^#(X1)	(91)
mark^#(plus(X1,X2))	→	mark^#(X2)	(58)
mark^#(plus(X1,X2))	→	mark^#(X1)	(65)

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^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(plus(N,s(M)))	→	mark^#(U21(and(isNat(M),isNat(N)),M,N))	(94)
active^#(and(tt,X))	→	mark^#(X)	(70)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(93)

1.1.1.1.1.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₂ + 1
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
active(isNat(0))	→	mark(tt)	(4)
mark(isNat(X))	→	active(isNat(X))	(15)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(and(tt,X))	→	mark(X)	(3)
mark(0)	→	active(0)	(16)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
and(mark(X1),X2)	→	and(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)
active(U21(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^#(U21(and(isNat(M),isNat(N)),M,N))

(94)

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^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(and(tt,X))	→	mark^#(X)	(70)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)
active^#(U21(tt,M,N))	→	mark^#(s(plus(N,M)))	(93)

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₃ + 2
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
active(isNat(0))	→	mark(tt)	(4)
mark(isNat(X))	→	active(isNat(X))	(15)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(and(tt,X))	→	mark(X)	(3)
mark(0)	→	active(0)	(16)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
and(mark(X1),X2)	→	and(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)
active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

active^#(U21(tt,M,N))

→

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

(93)

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^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(and(tt,X))	→	mark^#(X)	(70)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)

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₃ + 77330
[U11(x₁, x₂)]	=	x₂ + 5599
[s(x₁)]	=	x₁ + 27858
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 14137
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 35333
[plus(x₁, x₂)]	=	x₁ + x₂ + 49472
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	21653
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
active(isNat(0))	→	mark(tt)	(4)
mark(isNat(X))	→	active(isNat(X))	(15)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(and(tt,X))	→	mark(X)	(3)
mark(0)	→	active(0)	(16)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
plus(X1,active(X2))	→	plus(X1,X2)	(32)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
and(mark(X1),X2)	→	and(X1,X2)	(33)
mark(tt)	→	active(tt)	(10)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
plus(X1,mark(X2))	→	plus(X1,X2)	(30)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
plus(active(X1),X2)	→	plus(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(29)
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^#(isNat(X))	→	active^#(isNat(X))	(54)
active^#(and(tt,X))	→	mark^#(X)	(70)
active^#(isNat(plus(V1,V2)))	→	mark^#(and(isNat(V1),isNat(V2)))	(46)
mark^#(and(X1,X2))	→	mark^#(X1)	(80)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(88)
mark^#(U21(X1,X2,X3))	→	active^#(U21(mark(X1),X2,X3))	(85)
mark^#(U11(X1,X2))	→	active^#(U11(mark(X1),X2))	(68)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(76)
active^#(isNat(s(V1)))	→	mark^#(isNat(V1))	(95)

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

U11^#(X1,active(X2))	→	U11^#(X1,X2)	(66)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(64)
U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(51)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(47)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 2987
[U11(x₁, x₂)]	=	x₂ + 1521
[s(x₁)]	=	2987
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 405
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	28872
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	2987
[U11^#(x₁, x₂)]	=	x₁ + x₂ + 0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	11820
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

U11^#(X1,active(X2))	→	U11^#(X1,X2)	(66)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(64)
U11^#(X1,mark(X2))	→	U11^#(X1,X2)	(51)
U11^#(active(X1),X2)	→	U11^#(X1,X2)	(47)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

isNat^#(mark(X))	→	isNat^#(X)	(53)
isNat^#(active(X))	→	isNat^#(X)	(74)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

isNat^#(mark(X))	→	isNat^#(X)	(53)
isNat^#(active(X))	→	isNat^#(X)	(74)

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

plus^#(active(X1),X2)	→	plus^#(X1,X2)	(72)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(97)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(43)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(41)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 15360
[U11(x₁, x₂)]	=	x₂ + 12063
[s(x₁)]	=	6812
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 12701
[plus^#(x₁, x₂)]	=	x₁ + 0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	37154
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	39090
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	5586
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

plus^#(active(X1),X2)	→	plus^#(X1,X2)	(72)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(97)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(X1,active(X2))	→	plus^#(X1,X2)	(43)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(41)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

plus^#(X1,active(X2))	→	plus^#(X1,X2)	(43)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(41)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

and^#(X1,active(X2))	→	and^#(X1,X2)	(71)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(89)
and^#(active(X1),X2)	→	and^#(X1,X2)	(78)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 31985
[U11(x₁, x₂)]	=	x₂ + 30808
[s(x₁)]	=	3801
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 21095
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2204
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 21310
[plus(x₁, x₂)]	=	38405
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	2607
[and^#(x₁, x₂)]	=	x₂ + 0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

and^#(X1,active(X2))	→	and^#(X1,X2)	(71)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

and^#(mark(X1),X2)	→	and^#(X1,X2)	(89)
and^#(active(X1),X2)	→	and^#(X1,X2)	(78)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 16760
[U11(x₁, x₂)]	=	x₂ + 7362
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 11495
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 16264
[plus(x₁, x₂)]	=	27507
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	10114
[and^#(x₁, x₂)]	=	x₁ + 0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

and^#(mark(X1),X2)	→	and^#(X1,X2)	(89)
and^#(active(X1),X2)	→	and^#(X1,X2)	(78)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

s^#(mark(X))	→	s^#(X)	(79)
s^#(active(X))	→	s^#(X)	(45)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 34866
[U11(x₁, x₂)]	=	x₂ + 6133
[s(x₁)]	=	28733
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 7343
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 6134
[isNat(x₁)]	=	x₁ + 13363
[plus(x₁, x₂)]	=	40999
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

s^#(mark(X))	→	s^#(X)	(79)
s^#(active(X))	→	s^#(X)	(45)

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

U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(98)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(69)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(90)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(49)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(44)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(73)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 970
[U11(x₁, x₂)]	=	x₂ + 2421
[s(x₁)]	=	970
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 2720
[plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	15243
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 37749
[plus(x₁, x₂)]	=	3448
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[tt]	=	24817
[and^#(x₁, x₂)]	=	0

together with the usable rules

U11(X1,mark(X2))	→	U11(X1,X2)	(18)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
and(X1,active(X2))	→	and(X1,X2)	(36)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(19)
U11(mark(X1),X2)	→	U11(X1,X2)	(17)
s(mark(X))	→	s(X)	(27)
and(X1,mark(X2))	→	and(X1,X2)	(34)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
s(active(X))	→	s(X)	(28)
and(mark(X1),X2)	→	and(X1,X2)	(33)
U11(X1,active(X2))	→	U11(X1,X2)	(20)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
isNat(active(X))	→	isNat(X)	(38)
isNat(mark(X))	→	isNat(X)	(37)
and(active(X1),X2)	→	and(X1,X2)	(35)

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

U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(98)
U21^#(X1,active(X2),X3)	→	U21^#(X1,X2,X3)	(69)
U21^#(X1,X2,mark(X3))	→	U21^#(X1,X2,X3)	(90)
U21^#(X1,X2,active(X3))	→	U21^#(X1,X2,X3)	(49)
U21^#(X1,mark(X2),X3)	→	U21^#(X1,X2,X3)	(44)
U21^#(active(X1),X2,X3)	→	U21^#(X1,X2,X3)	(73)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.