Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_complete_iGM)

The rewrite relation of the following TRS is considered.

There are 111 ruless (increase limit for explicit display).

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.

There are 200 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 19 components.

The 1^st component contains the pair

active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(310)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
active^#(and(tt,X))	→	mark^#(X)	(211)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
mark^#(U33(X))	→	mark^#(X)	(196)
mark^#(x(X1,X2))	→	mark^#(X2)	(294)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(187)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(s(X))	→	active^#(s(mark(X)))	(282)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(U32(X1,X2))	→	active^#(U32(mark(X1),X2))	(267)
mark^#(U41(X1,X2))	→	mark^#(X1)	(263)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
active^#(x(N,0))	→	mark^#(U61(and(isNat(N),isNatKind(N))))	(260)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
mark^#(U22(X))	→	active^#(U22(mark(X)))	(157)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
active^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(s(X))	→	mark^#(X)	(153)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
active^#(U32(tt,V2))	→	mark^#(U33(isNat(V2)))	(150)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
mark^#(U61(X))	→	mark^#(X)	(141)
active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
active^#(U41(tt,N))	→	mark^#(N)	(136)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(plus(X1,X2))	→	mark^#(X2)	(230)
mark^#(U13(X))	→	active^#(U13(mark(X)))	(125)
mark^#(U33(X))	→	active^#(U33(mark(X)))	(227)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
mark^#(U61(X))	→	active^#(U61(mark(X)))	(120)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(x(X1,X2))	→	mark^#(X1)	(223)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	2
[U21(x₁, x₂)]	=	2
[U11(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	2
[and(x₁, x₂)]	=	2
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	2
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	2
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	2
[0]	=	4
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	3
[U32(x₁, x₂)]	=	2
[U33(x₁)]	=	1
[isNat(x₁)]	=	2
[plus(x₁, x₂)]	=	2
[U61(x₁)]	=	1
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 0
[U31(x₁, x₂, x₃)]	=	2
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	2335
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	1
[U22(x₁)]	=	1
[U51(x₁, x₂, x₃)]	=	2
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	2
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(50)
U41(active(X1),X2)	→	U41(X1,X2)	(80)
x(active(X1),X2)	→	x(X1,X2)	(104)
x(X1,mark(X2))	→	x(X1,X2)	(103)
x(mark(X1),X2)	→	x(X1,X2)	(102)
U12(active(X1),X2)	→	U12(X1,X2)	(54)
U33(active(X))	→	U33(X)	(77)
U31(X1,X2,mark(X3))	→	U31(X1,X2,X3)	(68)
U51(active(X1),X2,X3)	→	U51(X1,X2,X3)	(85)
U71(X1,active(X2),X3)	→	U71(X1,X2,X3)	(100)
x(X1,active(X2))	→	x(X1,X2)	(105)
U21(X1,active(X2))	→	U21(X1,X2)	(63)
U21(mark(X1),X2)	→	U21(X1,X2)	(60)
U51(X1,X2,active(X3))	→	U51(X1,X2,X3)	(87)
U51(X1,X2,mark(X3))	→	U51(X1,X2,X3)	(84)
U22(active(X))	→	U22(X)	(65)
U32(mark(X1),X2)	→	U32(X1,X2)	(72)
U22(mark(X))	→	U22(X)	(64)
plus(X1,active(X2))	→	plus(X1,X2)	(93)
plus(active(X1),X2)	→	plus(X1,X2)	(92)
s(mark(X))	→	s(X)	(88)
and(active(X1),X2)	→	and(X1,X2)	(108)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(49)
U12(mark(X1),X2)	→	U12(X1,X2)	(52)
U21(active(X1),X2)	→	U21(X1,X2)	(62)
and(mark(X1),X2)	→	and(X1,X2)	(106)
isNatKind(active(X))	→	isNatKind(X)	(111)
U51(mark(X1),X2,X3)	→	U51(X1,X2,X3)	(82)
s(active(X))	→	s(X)	(89)
isNat(mark(X))	→	isNat(X)	(56)
U41(X1,mark(X2))	→	U41(X1,X2)	(79)
U71(X1,X2,active(X3))	→	U71(X1,X2,X3)	(101)
U31(active(X1),X2,X3)	→	U31(X1,X2,X3)	(69)
U71(mark(X1),X2,X3)	→	U71(X1,X2,X3)	(96)
U41(mark(X1),X2)	→	U41(X1,X2)	(78)
U41(X1,active(X2))	→	U41(X1,X2)	(81)
U31(X1,active(X2),X3)	→	U31(X1,X2,X3)	(70)
U61(mark(X))	→	U61(X)	(94)
and(X1,active(X2))	→	and(X1,X2)	(109)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
U71(X1,X2,mark(X3))	→	U71(X1,X2,X3)	(98)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(51)
and(X1,mark(X2))	→	and(X1,X2)	(107)
plus(mark(X1),X2)	→	plus(X1,X2)	(90)
U31(X1,mark(X2),X3)	→	U31(X1,X2,X3)	(67)
U12(X1,active(X2))	→	U12(X1,X2)	(55)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U21(X1,mark(X2))	→	U21(X1,X2)	(61)
U13(mark(X))	→	U13(X)	(58)
U32(active(X1),X2)	→	U32(X1,X2)	(74)
U32(X1,active(X2))	→	U32(X1,X2)	(75)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(48)
U31(X1,X2,active(X3))	→	U31(X1,X2,X3)	(71)
U12(X1,mark(X2))	→	U12(X1,X2)	(53)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(47)
U32(X1,mark(X2))	→	U32(X1,X2)	(73)
plus(X1,mark(X2))	→	plus(X1,X2)	(91)
U71(X1,mark(X2),X3)	→	U71(X1,X2,X3)	(97)
U71(active(X1),X2,X3)	→	U71(X1,X2,X3)	(99)
U61(active(X))	→	U61(X)	(95)
U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(46)
U31(mark(X1),X2,X3)	→	U31(X1,X2,X3)	(66)
U51(X1,mark(X2),X3)	→	U51(X1,X2,X3)	(83)
U51(X1,active(X2),X3)	→	U51(X1,X2,X3)	(86)

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

mark^#(s(X))	→	active^#(s(mark(X)))	(282)
mark^#(U22(X))	→	active^#(U22(mark(X)))	(157)
mark^#(U13(X))	→	active^#(U13(mark(X)))	(125)
mark^#(U33(X))	→	active^#(U33(mark(X)))	(227)
mark^#(U61(X))	→	active^#(U61(mark(X)))	(120)

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^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
mark^#(U41(X1,X2))	→	mark^#(X1)	(263)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
mark^#(U32(X1,X2))	→	active^#(U32(mark(X1),X2))	(267)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X2)	(230)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(U32(tt,V2))	→	mark^#(U33(isNat(V2)))	(150)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(x(N,0))	→	mark^#(U61(and(isNat(N),isNatKind(N))))	(260)
active^#(U41(tt,N))	→	mark^#(N)	(136)
active^#(and(tt,X))	→	mark^#(X)	(211)
mark^#(U61(X))	→	mark^#(X)	(141)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(187)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(310)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(U33(X))	→	mark^#(X)	(196)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	mark^#(X2)	(294)
mark^#(x(X1,X2))	→	mark^#(X1)	(223)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	max(0)
[isNatKind(x₁)]	=	0
[U21(x₁, x₂)]	=	max(x₁ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 591, x₂ + 32872, x₃ + 32871, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 32871, x₂ + 32872, 0)
[U12^#(x₁, x₂)]	=	max(0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	841
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[U32(x₁, x₂)]	=	max(x₁ + 0, 0)
[U33(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 592, 0)
[U61(x₁)]	=	x₁ + 2447
[U51^#(x₁, x₂, x₃)]	=	max(0)
[U11^#(x₁, x₂, x₃)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, 0)
[U41^#(x₁, x₂)]	=	max(0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	max(0)
[U22^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(0)
[U13(x₁)]	=	x₁ + 0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 591, x₂ + 592, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	max(x₁ + 1432, x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[U61^#(x₁)]	=	0

together with the usable rules

There are 111 ruless (increase limit for explicit display).

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

mark^#(U41(X1,X2))	→	mark^#(X1)	(263)
mark^#(plus(X1,X2))	→	mark^#(X2)	(230)
active^#(x(N,0))	→	mark^#(U61(and(isNat(N),isNatKind(N))))	(260)
mark^#(U61(X))	→	mark^#(X)	(141)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(187)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(310)
mark^#(x(X1,X2))	→	mark^#(X2)	(294)
mark^#(x(X1,X2))	→	mark^#(X1)	(223)

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^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
mark^#(U32(X1,X2))	→	active^#(U32(mark(X1),X2))	(267)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(U32(tt,V2))	→	mark^#(U33(isNat(V2)))	(150)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
active^#(and(tt,X))	→	mark^#(X)	(211)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(U33(X))	→	mark^#(X)	(196)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	max(0)
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 1, x₃ + 1, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 1, x₃ + 0, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U12^#(x₁, x₂)]	=	max(0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[U32(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U33(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	1
[U51^#(x₁, x₂, x₃)]	=	max(0)
[U11^#(x₁, x₂, x₃)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 1, x₃ + 2, 0)
[U41^#(x₁, x₂)]	=	max(0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	max(0)
[U22^#(x₁)]	=	0
[tt]	=	2
[U71^#(x₁, x₂, x₃)]	=	max(0)
[U13(x₁)]	=	x₁ + 0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[U61^#(x₁)]	=	0

together with the usable rules

There are 111 ruless (increase limit for explicit display).

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

active^#(U32(tt,V2))

→

mark^#(U33(isNat(V2)))

(150)

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

active^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
mark^#(U32(X1,X2))	→	active^#(U32(mark(X1),X2))	(267)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
active^#(and(tt,X))	→	mark^#(X)	(211)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(U33(X))	→	mark^#(X)	(196)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	20695
[U21(x₁, x₂)]	=	20695
[U11(x₁, x₂, x₃)]	=	20695
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	20695
[and(x₁, x₂)]	=	20695
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	20695
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	20695
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	20695
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[U32(x₁, x₂)]	=	1
[U33(x₁)]	=	2
[isNat(x₁)]	=	20695
[plus(x₁, x₂)]	=	20695
[U61(x₁)]	=	6
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	2
[U31(x₁, x₂, x₃)]	=	20695
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	1
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	1
[U22(x₁)]	=	1
[U51(x₁, x₂, x₃)]	=	20695
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	20695
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(50)
U41(active(X1),X2)	→	U41(X1,X2)	(80)
x(active(X1),X2)	→	x(X1,X2)	(104)
x(X1,mark(X2))	→	x(X1,X2)	(103)
x(mark(X1),X2)	→	x(X1,X2)	(102)
U12(active(X1),X2)	→	U12(X1,X2)	(54)
U33(active(X))	→	U33(X)	(77)
U31(X1,X2,mark(X3))	→	U31(X1,X2,X3)	(68)
U51(active(X1),X2,X3)	→	U51(X1,X2,X3)	(85)
U71(X1,active(X2),X3)	→	U71(X1,X2,X3)	(100)
x(X1,active(X2))	→	x(X1,X2)	(105)
U21(X1,active(X2))	→	U21(X1,X2)	(63)
U21(mark(X1),X2)	→	U21(X1,X2)	(60)
U51(X1,X2,active(X3))	→	U51(X1,X2,X3)	(87)
U51(X1,X2,mark(X3))	→	U51(X1,X2,X3)	(84)
U22(active(X))	→	U22(X)	(65)
U32(mark(X1),X2)	→	U32(X1,X2)	(72)
U22(mark(X))	→	U22(X)	(64)
plus(X1,active(X2))	→	plus(X1,X2)	(93)
plus(active(X1),X2)	→	plus(X1,X2)	(92)
s(mark(X))	→	s(X)	(88)
and(active(X1),X2)	→	and(X1,X2)	(108)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(49)
U12(mark(X1),X2)	→	U12(X1,X2)	(52)
U21(active(X1),X2)	→	U21(X1,X2)	(62)
and(mark(X1),X2)	→	and(X1,X2)	(106)
isNatKind(active(X))	→	isNatKind(X)	(111)
U51(mark(X1),X2,X3)	→	U51(X1,X2,X3)	(82)
s(active(X))	→	s(X)	(89)
isNat(mark(X))	→	isNat(X)	(56)
U41(X1,mark(X2))	→	U41(X1,X2)	(79)
U71(X1,X2,active(X3))	→	U71(X1,X2,X3)	(101)
U31(active(X1),X2,X3)	→	U31(X1,X2,X3)	(69)
U71(mark(X1),X2,X3)	→	U71(X1,X2,X3)	(96)
U41(mark(X1),X2)	→	U41(X1,X2)	(78)
U41(X1,active(X2))	→	U41(X1,X2)	(81)
U31(X1,active(X2),X3)	→	U31(X1,X2,X3)	(70)
U61(mark(X))	→	U61(X)	(94)
and(X1,active(X2))	→	and(X1,X2)	(109)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
U71(X1,X2,mark(X3))	→	U71(X1,X2,X3)	(98)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(51)
and(X1,mark(X2))	→	and(X1,X2)	(107)
plus(mark(X1),X2)	→	plus(X1,X2)	(90)
U31(X1,mark(X2),X3)	→	U31(X1,X2,X3)	(67)
U12(X1,active(X2))	→	U12(X1,X2)	(55)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U21(X1,mark(X2))	→	U21(X1,X2)	(61)
U13(mark(X))	→	U13(X)	(58)
U32(active(X1),X2)	→	U32(X1,X2)	(74)
U32(X1,active(X2))	→	U32(X1,X2)	(75)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(48)
U31(X1,X2,active(X3))	→	U31(X1,X2,X3)	(71)
U12(X1,mark(X2))	→	U12(X1,X2)	(53)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(47)
U32(X1,mark(X2))	→	U32(X1,X2)	(73)
plus(X1,mark(X2))	→	plus(X1,X2)	(91)
U71(X1,mark(X2),X3)	→	U71(X1,X2,X3)	(97)
U71(active(X1),X2,X3)	→	U71(X1,X2,X3)	(99)
U61(active(X))	→	U61(X)	(95)
U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(46)
U31(mark(X1),X2,X3)	→	U31(X1,X2,X3)	(66)
U51(X1,mark(X2),X3)	→	U51(X1,X2,X3)	(83)
U51(X1,active(X2),X3)	→	U51(X1,X2,X3)	(86)

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

mark^#(U32(X1,X2))

→

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

(267)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
active^#(and(tt,X))	→	mark^#(X)	(211)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(U33(X))	→	mark^#(X)	(196)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	max(0)
[isNatKind(x₁)]	=	x₁ + 10066
[U21(x₁, x₂)]	=	max(x₁ + 3, x₂ + 10072, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 10072, x₃ + 19964, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 39698, x₂ + 49773, x₃ + 49775, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 4, 0)
[plus^#(x₁, x₂)]	=	max(0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 10074, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 49775, x₂ + 49773, 0)
[U12^#(x₁, x₂)]	=	max(0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	8
[x^#(x₁, x₂)]	=	max(0)
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[U32(x₁, x₂)]	=	max(x₁ + 9134, x₂ + 19206, 0)
[U33(x₁)]	=	x₁ + 2
[isNat(x₁)]	=	x₁ + 10072
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 9893, 0)
[U61(x₁)]	=	49776
[U51^#(x₁, x₂, x₃)]	=	max(0)
[U11^#(x₁, x₂, x₃)]	=	max(0)
[active(x₁)]	=	x₁ + 0
[U31(x₁, x₂, x₃)]	=	max(x₁ + 9133, x₂ + 19207, x₃ + 19208, 0)
[U41^#(x₁, x₂)]	=	max(0)
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	max(0)
[U22^#(x₁)]	=	0
[tt]	=	10074
[U71^#(x₁, x₂, x₃)]	=	max(0)
[U13(x₁)]	=	x₁ + 1
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₂ + 9893, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[U61^#(x₁)]	=	0

together with the usable rules

There are 111 ruless (increase limit for explicit display).

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

active^#(isNatKind(x(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(137)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(215)
active^#(isNat(x(V1,V2)))	→	mark^#(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(259)
mark^#(U32(X1,X2))	→	mark^#(X1)	(301)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(188)
mark^#(U13(X))	→	mark^#(X)	(131)
mark^#(U21(X1,X2))	→	mark^#(X1)	(113)
active^#(and(tt,X))	→	mark^#(X)	(211)
active^#(U31(tt,V1,V2))	→	mark^#(U32(isNat(V1),V2))	(224)
mark^#(U33(X))	→	mark^#(X)	(196)
active^#(U12(tt,V2))	→	mark^#(U13(isNat(V2)))	(288)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	51803
[U21(x₁, x₂)]	=	51803
[U11(x₁, x₂, x₃)]	=	51803
[s(x₁)]	=	1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	51803
[and(x₁, x₂)]	=	5662
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	51802
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	51803
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	51803
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	1
[U32(x₁, x₂)]	=	4
[U33(x₁)]	=	1
[isNat(x₁)]	=	51803
[plus(x₁, x₂)]	=	51803
[U61(x₁)]	=	6
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	2
[U31(x₁, x₂, x₃)]	=	33105
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	1
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	1
[U22(x₁)]	=	1
[U51(x₁, x₂, x₃)]	=	51803
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	51803
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U11(X1,active(X2),X3)	→	U11(X1,X2,X3)	(50)
U41(active(X1),X2)	→	U41(X1,X2)	(80)
x(active(X1),X2)	→	x(X1,X2)	(104)
x(X1,mark(X2))	→	x(X1,X2)	(103)
x(mark(X1),X2)	→	x(X1,X2)	(102)
U12(active(X1),X2)	→	U12(X1,X2)	(54)
U33(active(X))	→	U33(X)	(77)
U31(X1,X2,mark(X3))	→	U31(X1,X2,X3)	(68)
U51(active(X1),X2,X3)	→	U51(X1,X2,X3)	(85)
U71(X1,active(X2),X3)	→	U71(X1,X2,X3)	(100)
x(X1,active(X2))	→	x(X1,X2)	(105)
U21(X1,active(X2))	→	U21(X1,X2)	(63)
U21(mark(X1),X2)	→	U21(X1,X2)	(60)
U51(X1,X2,active(X3))	→	U51(X1,X2,X3)	(87)
U51(X1,X2,mark(X3))	→	U51(X1,X2,X3)	(84)
U22(active(X))	→	U22(X)	(65)
U32(mark(X1),X2)	→	U32(X1,X2)	(72)
U22(mark(X))	→	U22(X)	(64)
plus(X1,active(X2))	→	plus(X1,X2)	(93)
plus(active(X1),X2)	→	plus(X1,X2)	(92)
s(mark(X))	→	s(X)	(88)
and(active(X1),X2)	→	and(X1,X2)	(108)
U11(active(X1),X2,X3)	→	U11(X1,X2,X3)	(49)
U12(mark(X1),X2)	→	U12(X1,X2)	(52)
U21(active(X1),X2)	→	U21(X1,X2)	(62)
and(mark(X1),X2)	→	and(X1,X2)	(106)
isNatKind(active(X))	→	isNatKind(X)	(111)
U51(mark(X1),X2,X3)	→	U51(X1,X2,X3)	(82)
s(active(X))	→	s(X)	(89)
isNat(mark(X))	→	isNat(X)	(56)
U41(X1,mark(X2))	→	U41(X1,X2)	(79)
U71(X1,X2,active(X3))	→	U71(X1,X2,X3)	(101)
U31(active(X1),X2,X3)	→	U31(X1,X2,X3)	(69)
U71(mark(X1),X2,X3)	→	U71(X1,X2,X3)	(96)
U41(mark(X1),X2)	→	U41(X1,X2)	(78)
U41(X1,active(X2))	→	U41(X1,X2)	(81)
U31(X1,active(X2),X3)	→	U31(X1,X2,X3)	(70)
U61(mark(X))	→	U61(X)	(94)
and(X1,active(X2))	→	and(X1,X2)	(109)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
U71(X1,X2,mark(X3))	→	U71(X1,X2,X3)	(98)
U11(X1,X2,active(X3))	→	U11(X1,X2,X3)	(51)
and(X1,mark(X2))	→	and(X1,X2)	(107)
plus(mark(X1),X2)	→	plus(X1,X2)	(90)
U31(X1,mark(X2),X3)	→	U31(X1,X2,X3)	(67)
U12(X1,active(X2))	→	U12(X1,X2)	(55)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U21(X1,mark(X2))	→	U21(X1,X2)	(61)
U13(mark(X))	→	U13(X)	(58)
U32(active(X1),X2)	→	U32(X1,X2)	(74)
U32(X1,active(X2))	→	U32(X1,X2)	(75)
U11(X1,X2,mark(X3))	→	U11(X1,X2,X3)	(48)
U31(X1,X2,active(X3))	→	U31(X1,X2,X3)	(71)
U12(X1,mark(X2))	→	U12(X1,X2)	(53)
U11(X1,mark(X2),X3)	→	U11(X1,X2,X3)	(47)
U32(X1,mark(X2))	→	U32(X1,X2)	(73)
plus(X1,mark(X2))	→	plus(X1,X2)	(91)
U71(X1,mark(X2),X3)	→	U71(X1,X2,X3)	(97)
U71(active(X1),X2,X3)	→	U71(X1,X2,X3)	(99)
U61(active(X))	→	U61(X)	(95)
U11(mark(X1),X2,X3)	→	U11(X1,X2,X3)	(46)
U31(mark(X1),X2,X3)	→	U31(X1,X2,X3)	(66)
U51(X1,mark(X2),X3)	→	U51(X1,X2,X3)	(83)
U51(X1,active(X2),X3)	→	U51(X1,X2,X3)	(86)

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

mark^#(U12(X1,X2))	→	active^#(U12(mark(X1),X2))	(273)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(281)
mark^#(U31(X1,X2,X3))	→	active^#(U31(mark(X1),X2,X3))	(220)

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^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(U32^#)	=	1
π(U33^#)	=	1
π(U12^#)	=	1
π(mark)	=	1
π(isNat)	=	1
π(U61)	=	1
π(active)	=	1
π(U31)	=	1
π(U41^#)	=	2
π(active^#)	=	1
π(and^#)	=	2

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

prec(isNatKind)	=	3	status(isNatKind)	=	[1]	list-extension(isNatKind)	=	Lex
prec(U21)	=	4	status(U21)	=	[2]	list-extension(U21)	=	Lex
prec(U11)	=	6	status(U11)	=	[2]	list-extension(U11)	=	Lex
prec(s)	=	5	status(s)	=	[1]	list-extension(s)	=	Lex
prec(isNat^#)	=	0	status(isNat^#)	=	[]	list-extension(isNat^#)	=	Lex
prec(U71)	=	9	status(U71)	=	[2, 3, 1]	list-extension(U71)	=	Lex
prec(and)	=	3	status(and)	=	[1, 2]	list-extension(and)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[1, 2]	list-extension(plus^#)	=	Lex
prec(U13^#)	=	0	status(U13^#)	=	[]	list-extension(U13^#)	=	Lex
prec(U12)	=	5	status(U12)	=	[1]	list-extension(U12)	=	Lex
prec(x)	=	9	status(x)	=	[2, 1]	list-extension(x)	=	Lex
prec(mark^#)	=	1	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(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(U32)	=	0	status(U32)	=	[]	list-extension(U32)	=	Lex
prec(U33)	=	0	status(U33)	=	[]	list-extension(U33)	=	Lex
prec(plus)	=	7	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U51^#)	=	0	status(U51^#)	=	[3, 1, 2]	list-extension(U51^#)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[3, 1, 2]	list-extension(U11^#)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[1, 2]	list-extension(U21^#)	=	Lex
prec(U22^#)	=	0	status(U22^#)	=	[]	list-extension(U22^#)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U71^#)	=	0	status(U71^#)	=	[2, 1]	list-extension(U71^#)	=	Lex
prec(U13)	=	5	status(U13)	=	[]	list-extension(U13)	=	Lex
prec(U22)	=	3	status(U22)	=	[1]	list-extension(U22)	=	Lex
prec(U51)	=	7	status(U51)	=	[3, 2, 1]	list-extension(U51)	=	Lex
prec(isNatKind^#)	=	0	status(isNatKind^#)	=	[]	list-extension(isNatKind^#)	=	Lex
prec(U41)	=	7	status(U41)	=	[2]	list-extension(U41)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[2, 1, 3]	list-extension(U31^#)	=	Lex
prec(U61^#)	=	0	status(U61^#)	=	[]	list-extension(U61^#)	=	Lex

and the following Max-polynomial interpretation

[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₂ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, 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)
[s^#(x₁)]	=	0
[U32(x₁, x₂)]	=	max(0)
[U33(x₁)]	=	0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U51^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U22^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, 0)
[U13(x₁)]	=	0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

There are 111 ruless (increase limit for explicit display).

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

active^#(U21(tt,V1))	→	mark^#(U22(isNat(V1)))	(251)
active^#(isNat(plus(V1,V2)))	→	mark^#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))	(258)
active^#(U11(tt,V1,V2))	→	mark^#(U12(isNat(V1),V2))	(311)
active^#(isNat(s(V1)))	→	mark^#(U21(isNatKind(V1),V1))	(119)
mark^#(U41(X1,X2))	→	active^#(U41(mark(X1),X2))	(147)
mark^#(U11(X1,X2,X3))	→	active^#(U11(mark(X1),X2,X3))	(198)
active^#(isNatKind(plus(V1,V2)))	→	mark^#(and(isNatKind(V1),isNatKind(V2)))	(151)
mark^#(U22(X))	→	mark^#(X)	(252)
active^#(plus(N,0))	→	mark^#(U41(and(isNat(N),isNatKind(N)),N))	(149)
mark^#(U12(X1,X2))	→	mark^#(X1)	(254)
mark^#(and(X1,X2))	→	mark^#(X1)	(202)
active^#(U51(tt,M,N))	→	mark^#(s(plus(N,M)))	(237)
mark^#(plus(X1,X2))	→	mark^#(X1)	(190)
mark^#(plus(X1,X2))	→	active^#(plus(mark(X1),mark(X2)))	(156)
active^#(isNatKind(s(V1)))	→	mark^#(isNatKind(V1))	(163)
active^#(x(N,s(M)))	→	mark^#(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(276)
mark^#(U21(X1,X2))	→	active^#(U21(mark(X1),X2))	(249)
active^#(U71(tt,M,N))	→	mark^#(plus(x(N,M),N))	(189)
mark^#(isNatKind(X))	→	active^#(isNatKind(X))	(287)
active^#(plus(N,s(M)))	→	mark^#(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))	(118)
active^#(U41(tt,N))	→	mark^#(N)	(136)
mark^#(s(X))	→	mark^#(X)	(153)
mark^#(U51(X1,X2,X3))	→	active^#(U51(mark(X1),X2,X3))	(283)
mark^#(U71(X1,X2,X3))	→	active^#(U71(mark(X1),X2,X3))	(284)
mark^#(isNat(X))	→	active^#(isNat(X))	(173)
mark^#(x(X1,X2))	→	active^#(x(mark(X1),mark(X2)))	(238)

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

U51^#(X1,active(X2),X3)	→	U51^#(X1,X2,X3)	(305)
U51^#(active(X1),X2,X3)	→	U51^#(X1,X2,X3)	(296)
U51^#(X1,mark(X2),X3)	→	U51^#(X1,X2,X3)	(172)
U51^#(X1,X2,mark(X3))	→	U51^#(X1,X2,X3)	(169)
U51^#(mark(X1),X2,X3)	→	U51^#(X1,X2,X3)	(168)
U51^#(X1,X2,active(X3))	→	U51^#(X1,X2,X3)	(139)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	48285
[U21(x₁, x₂)]	=	x₁ + x₂ + 53013
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	63326
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 34650
[and(x₁, x₂)]	=	120921
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	80311
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 10309
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	48283
[U33(x₁)]	=	48285
[isNat(x₁)]	=	x₁ + 37970
[plus(x₁, x₂)]	=	x₁ + x₂ + 72630
[U61(x₁)]	=	x₁ + 39997
[U51^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	48281
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	48287
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	80313
[U22(x₁)]	=	101302
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 15037
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	72633
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U51^#(X1,active(X2),X3)	→	U51^#(X1,X2,X3)	(305)
U51^#(active(X1),X2,X3)	→	U51^#(X1,X2,X3)	(296)
U51^#(X1,mark(X2),X3)	→	U51^#(X1,X2,X3)	(172)
U51^#(X1,X2,mark(X3))	→	U51^#(X1,X2,X3)	(169)
U51^#(mark(X1),X2,X3)	→	U51^#(X1,X2,X3)	(168)
U51^#(X1,X2,active(X3))	→	U51^#(X1,X2,X3)	(139)

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

x^#(active(X1),X2)	→	x^#(X1,X2)	(178)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(269)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(162)
x^#(X1,active(X2))	→	x^#(X1,X2)	(130)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	4
[U21(x₁, x₂)]	=	x₁ + x₂ + 18
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	19
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[and(x₁, x₂)]	=	26
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	13
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 12
[U61(x₁)]	=	x₁ + 1
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	15
[U22(x₁)]	=	30
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 7
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	17785
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

x^#(active(X1),X2)	→	x^#(X1,X2)	(178)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(269)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(162)
x^#(X1,active(X2))	→	x^#(X1,X2)	(130)

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

U71^#(X1,X2,active(X3))	→	U71^#(X1,X2,X3)	(308)
U71^#(X1,mark(X2),X3)	→	U71^#(X1,X2,X3)	(213)
U71^#(mark(X1),X2,X3)	→	U71^#(X1,X2,X3)	(191)
U71^#(active(X1),X2,X3)	→	U71^#(X1,X2,X3)	(184)
U71^#(X1,active(X2),X3)	→	U71^#(X1,X2,X3)	(180)
U71^#(X1,X2,mark(X3))	→	U71^#(X1,X2,X3)	(165)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	2285
[U21(x₁, x₂)]	=	x₁ + x₂ + 23
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	2305
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 27340
[and(x₁, x₂)]	=	29642
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	2709
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 2278
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	2283
[U33(x₁)]	=	2285
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 27351
[U61(x₁)]	=	x₁ + 37885
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	2281
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	2287
[U71^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U13(x₁)]	=	2711
[U22(x₁)]	=	2312
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 16
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	27354
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U71^#(X1,X2,active(X3))	→	U71^#(X1,X2,X3)	(308)
U71^#(X1,mark(X2),X3)	→	U71^#(X1,X2,X3)	(213)
U71^#(mark(X1),X2,X3)	→	U71^#(X1,X2,X3)	(191)
U71^#(active(X1),X2,X3)	→	U71^#(X1,X2,X3)	(184)
U71^#(X1,active(X2),X3)	→	U71^#(X1,X2,X3)	(180)
U71^#(X1,X2,mark(X3))	→	U71^#(X1,X2,X3)	(165)

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

U61^#(active(X))	→	U61^#(X)	(266)
U61^#(mark(X))	→	U61^#(X)	(161)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	35945
[U21(x₁, x₂)]	=	x₁ + x₂ + 13653
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	36282
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 41897
[and(x₁, x₂)]	=	91172
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	62055
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 22625
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	35943
[U33(x₁)]	=	35945
[isNat(x₁)]	=	x₁ + 13314
[plus(x₁, x₂)]	=	x₁ + x₂ + 55221
[U61(x₁)]	=	x₁ + 18211
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	35941
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	35947
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	62057
[U22(x₁)]	=	49602
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 333
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	55224
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	x₁ + 0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U61^#(active(X))	→	U61^#(X)	(266)
U61^#(mark(X))	→	U61^#(X)	(161)

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

U33^#(mark(X))	→	U33^#(X)	(177)
U33^#(active(X))	→	U33^#(X)	(278)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	7
[U21(x₁, x₂)]	=	x₁ + x₂ + 20
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 21559
[s(x₁)]	=	24
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[and(x₁, x₂)]	=	26
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	21571
[U33^#(x₁)]	=	x₁ + 0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 12
[U61(x₁)]	=	x₁ + 14529
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	21573
[U22(x₁)]	=	32
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 12
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	16196
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U33^#(mark(X))	→	U33^#(X)	(177)
U33^#(active(X))	→	U33^#(X)	(278)

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

s^#(active(X))	→	s^#(X)	(201)
s^#(mark(X))	→	s^#(X)	(145)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	4
[U21(x₁, x₂)]	=	x₁ + x₂ + 7019
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	7020
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 28848
[and(x₁, x₂)]	=	28873
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	27810
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 28859
[U61(x₁)]	=	x₁ + 33320
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	27812
[U22(x₁)]	=	7031
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 7008
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	28862
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

s^#(active(X))	→	s^#(X)	(201)
s^#(mark(X))	→	s^#(X)	(145)

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

plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(212)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(290)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(275)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(142)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	6
[U21(x₁, x₂)]	=	x₁ + x₂ + 15192
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	15195
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 21859
[and(x₁, x₂)]	=	21884
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	2259
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 21870
[U61(x₁)]	=	x₁ + 29329
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	27812
[U22(x₁)]	=	15204
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 15183
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	21873
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(212)
plus^#(X1,active(X2))	→	plus^#(X1,X2)	(290)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(275)
plus^#(active(X1),X2)	→	plus^#(X1,X2)	(142)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

U31^#(X1,X2,active(X3))	→	U31^#(X1,X2,X3)	(209)
U31^#(mark(X1),X2,X3)	→	U31^#(X1,X2,X3)	(205)
U31^#(active(X1),X2,X3)	→	U31^#(X1,X2,X3)	(199)
U31^#(X1,mark(X2),X3)	→	U31^#(X1,X2,X3)	(192)
U31^#(X1,X2,mark(X3))	→	U31^#(X1,X2,X3)	(245)
U31^#(X1,active(X2),X3)	→	U31^#(X1,X2,X3)	(240)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	5
[U21(x₁, x₂)]	=	x₁ + x₂ + 14
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	16
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[and(x₁, x₂)]	=	26
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	13
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 12
[U61(x₁)]	=	468
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	15
[U22(x₁)]	=	26
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 4
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	15
[U31^#(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
s(mark(X))	→	s(X)	(88)
isNatKind(active(X))	→	isNatKind(X)	(111)
s(active(X))	→	s(X)	(89)
U33(mark(X))	→	U33(X)	(76)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U31^#(mark(X1),X2,X3)	→	U31^#(X1,X2,X3)	(205)
U31^#(active(X1),X2,X3)	→	U31^#(X1,X2,X3)	(199)
U31^#(X1,mark(X2),X3)	→	U31^#(X1,X2,X3)	(192)
U31^#(X1,active(X2),X3)	→	U31^#(X1,X2,X3)	(240)

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

U31^#(X1,X2,mark(X3))	→	U31^#(X1,X2,X3)	(245)
U31^#(X1,X2,active(X3))	→	U31^#(X1,X2,X3)	(209)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 40586
[U21(x₁, x₂)]	=	x₂ + 24354
[U11(x₁, x₂, x₃)]	=	x₂ + 73089
[s(x₁)]	=	x₁ + 12146
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 48665
[and(x₁, x₂)]	=	x₁ + x₂ + 20297
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 60885
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	21815
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	53746
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 34025
[U33(x₁)]	=	34027
[isNat(x₁)]	=	x₁ + 12206
[plus(x₁, x₂)]	=	x₁ + 60881
[U61(x₁)]	=	x₁ + 19715
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	34023
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	34029
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	15819
[U22(x₁)]	=	x₁ + 41602
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8809
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 60883
[U31^#(x₁, x₂, x₃)]	=	x₃ + 0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

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

U31^#(X1,X2,mark(X3))	→	U31^#(X1,X2,X3)	(245)
U31^#(X1,X2,active(X3))	→	U31^#(X1,X2,X3)	(209)

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

U21^#(active(X1),X2)	→	U21^#(X1,X2)	(183)
U21^#(X1,active(X2))	→	U21^#(X1,X2)	(235)
U21^#(mark(X1),X2)	→	U21^#(X1,X2)	(124)
U21^#(X1,mark(X2))	→	U21^#(X1,X2)	(116)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 783
[U21(x₁, x₂)]	=	x₂ + 1139
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 27404
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 50360
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 77408
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	49994
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	49998
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 51134
[U33(x₁)]	=	51136
[isNat(x₁)]	=	x₁ + 1136
[plus(x₁, x₂)]	=	x₂ + 51141
[U61(x₁)]	=	49996
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	51132
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	x₁ + 0
[U22^#(x₁)]	=	0
[tt]	=	51138
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	28914
[U22(x₁)]	=	1141
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 101141
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U21^#(active(X1),X2)	→	U21^#(X1,X2)	(183)
U21^#(mark(X1),X2)	→	U21^#(X1,X2)	(124)

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

U21^#(X1,active(X2))	→	U21^#(X1,X2)	(235)
U21^#(X1,mark(X2))	→	U21^#(X1,X2)	(116)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₂ + 4
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 12232
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 14
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 12233
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	6
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 13
[U61(x₁)]	=	4
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	x₂ + 0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	7
[U22(x₁)]	=	8
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 2
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 21
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U21^#(X1,active(X2))	→	U21^#(X1,X2)	(235)
U21^#(X1,mark(X2))	→	U21^#(X1,X2)	(116)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

U32^#(mark(X1),X2)	→	U32^#(X1,X2)	(217)
U32^#(X1,active(X2))	→	U32^#(X1,X2)	(265)
U32^#(X1,mark(X2))	→	U32^#(X1,X2)	(253)
U32^#(active(X1),X2)	→	U32^#(X1,X2)	(233)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	x₂ + 0
[isNatKind(x₁)]	=	x₁ + 28642
[U21(x₁, x₂)]	=	x₂ + 45974
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 151200
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 59245
[and(x₁, x₂)]	=	x₁ + x₂ + 76587
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 105231
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	7
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 45976
[U33(x₁)]	=	45978
[isNat(x₁)]	=	x₁ + 45971
[plus(x₁, x₂)]	=	x₂ + 105227
[U61(x₁)]	=	5
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	45974
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	45980
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	30324
[U22(x₁)]	=	45976
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 30067
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 105236
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U32^#(X1,active(X2))	→	U32^#(X1,X2)	(265)
U32^#(X1,mark(X2))	→	U32^#(X1,X2)	(253)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U32^#(mark(X1),X2)	→	U32^#(X1,X2)	(217)
U32^#(active(X1),X2)	→	U32^#(X1,X2)	(233)

1.1.11.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	x₁ + 0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₂ + 17453
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 71068
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 53617
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 53620
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	36155
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	36159
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 53609
[U33(x₁)]	=	53611
[isNat(x₁)]	=	x₁ + 17450
[plus(x₁, x₂)]	=	x₂ + 53616
[U61(x₁)]	=	36157
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	53607
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	53613
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	21079
[U22(x₁)]	=	17455
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 89777
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U32^#(mark(X1),X2)	→	U32^#(X1,X2)	(217)
U32^#(active(X1),X2)	→	U32^#(X1,X2)	(233)

could be deleted.

1.1.11.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

U12^#(active(X1),X2)	→	U12^#(X1,X2)	(207)
U12^#(mark(X1),X2)	→	U12^#(X1,X2)	(175)
U12^#(X1,active(X2))	→	U12^#(X1,X2)	(239)
U12^#(X1,mark(X2))	→	U12^#(X1,X2)	(115)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₂ + 9317
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 49038
[s(x₁)]	=	x₁ + 9314
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 27655
[and(x₁, x₂)]	=	x₁ + x₂ + 49036
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 49039
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	21369
[U12^#(x₁, x₂)]	=	x₁ + 0
[mark^#(x₁)]	=	0
[0]	=	21373
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 21374
[U33(x₁)]	=	21376
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 49035
[U61(x₁)]	=	21371
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	21372
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	21378
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	8656
[U22(x₁)]	=	9319
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 6975
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 70410
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U12^#(active(X1),X2)	→	U12^#(X1,X2)	(207)
U12^#(mark(X1),X2)	→	U12^#(X1,X2)	(175)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U12^#(X1,active(X2))	→	U12^#(X1,X2)	(239)
U12^#(X1,mark(X2))	→	U12^#(X1,X2)	(115)

1.1.12.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 17985
[U21(x₁, x₂)]	=	x₂ + 1346
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 60912
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 35878
[and(x₁, x₂)]	=	x₁ + x₂ + 42926
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 60913
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	x₂ + 0
[mark^#(x₁)]	=	0
[0]	=	5
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 25025
[U33(x₁)]	=	25027
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 60909
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	25023
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	25029
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	2191
[U22(x₁)]	=	1348
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 2691
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 60916
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U12^#(X1,active(X2))	→	U12^#(X1,X2)	(239)
U12^#(X1,mark(X2))	→	U12^#(X1,X2)	(115)

could be deleted.

1.1.12.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 13^th component contains the pair

and^#(X1,mark(X2))	→	and^#(X1,X2)	(309)
and^#(active(X1),X2)	→	and^#(X1,X2)	(182)
and^#(X1,active(X2))	→	and^#(X1,X2)	(148)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(231)

1.1.13 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 2
[U21(x₁, x₂)]	=	x₂ + 4
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 16
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 5343
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 17
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	5
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 13
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	1
[U22(x₁)]	=	6
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 2
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 20
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	x₁ + x₂ + 0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

and^#(X1,mark(X2))	→	and^#(X1,X2)	(309)
and^#(active(X1),X2)	→	and^#(X1,X2)	(182)
and^#(X1,active(X2))	→	and^#(X1,X2)	(148)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(231)

could be deleted.

1.1.13.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 14^th component contains the pair

U11^#(mark(X1),X2,X3)	→	U11^#(X1,X2,X3)	(300)
U11^#(X1,X2,mark(X3))	→	U11^#(X1,X2,X3)	(197)
U11^#(X1,X2,active(X3))	→	U11^#(X1,X2,X3)	(171)
U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(262)
U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(242)
U11^#(active(X1),X2,X3)	→	U11^#(X1,X2,X3)	(129)

1.1.14 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₂ + 6
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 16199
[s(x₁)]	=	x₁ + 2
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 25908
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 16200
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	5
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	x₂ + 6
[U33(x₁)]	=	8
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₂ + 13
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	4
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	10
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	2
[U22(x₁)]	=	8
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 3
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₂ + 20
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U22(active(X))	→	U22(X)	(65)
U22(mark(X))	→	U22(X)	(64)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U13(active(X))	→	U13(X)	(59)
U13(mark(X))	→	U13(X)	(58)
U61(active(X))	→	U61(X)	(95)

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

U11^#(mark(X1),X2,X3)	→	U11^#(X1,X2,X3)	(300)
U11^#(X1,X2,mark(X3))	→	U11^#(X1,X2,X3)	(197)
U11^#(X1,X2,active(X3))	→	U11^#(X1,X2,X3)	(171)
U11^#(X1,active(X2),X3)	→	U11^#(X1,X2,X3)	(262)
U11^#(X1,mark(X2),X3)	→	U11^#(X1,X2,X3)	(242)
U11^#(active(X1),X2,X3)	→	U11^#(X1,X2,X3)	(129)

could be deleted.

1.1.14.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 15^th component contains the pair

U22^#(active(X))	→	U22^#(X)	(185)
U22^#(mark(X))	→	U22^#(X)	(268)

1.1.15 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 6099
[U21(x₁, x₂)]	=	x₁ + x₂ + 11099
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + 1132
[s(x₁)]	=	x₁ + 12011
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₂ + x₃ + 590
[and(x₁, x₂)]	=	x₁ + x₂ + 90
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 2579
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1765
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	2
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 52127
[U32(x₁, x₂)]	=	x₁ + x₂ + 15531
[U33(x₁)]	=	99995
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + 30352
[U61(x₁)]	=	x₁ + 2369
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁, x₂, x₃)]	=	x₁ + 3341
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	x₁ + 0
[tt]	=	47870
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	x₁ + 10546
[U22(x₁)]	=	x₁ + 26210
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 1385
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₁ + x₂ + 4255
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)

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

U22^#(active(X))	→	U22^#(X)	(185)
U22^#(mark(X))	→	U22^#(X)	(268)

could be deleted.

1.1.15.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 16^th component contains the pair

isNat^#(active(X))	→	isNat^#(X)	(200)
isNat^#(mark(X))	→	isNat^#(X)	(222)

1.1.16 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₁ + x₂ + 10730
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 59000
[s(x₁)]	=	x₁ + 8474
[isNat^#(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 35210
[and(x₁, x₂)]	=	x₁ + x₂ + 35221
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 59010
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	5
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	5
[U33(x₁)]	=	7
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + 35220
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	3
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	9
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	x₁ + 59020
[U22(x₁)]	=	x₁ + 10740
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 5084
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₁ + x₂ + 42468
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U61(active(X))	→	U61(X)	(95)

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

isNat^#(active(X))	→	isNat^#(X)	(200)
isNat^#(mark(X))	→	isNat^#(X)	(222)

could be deleted.

1.1.16.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 17^th component contains the pair

U41^#(mark(X1),X2)	→	U41^#(X1,X2)	(179)
U41^#(X1,mark(X2))	→	U41^#(X1,X2)	(250)
U41^#(X1,active(X2))	→	U41^#(X1,X2)	(143)
U41^#(active(X1),X2)	→	U41^#(X1,X2)	(123)

1.1.17 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₁ + x₂ + 26709
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[s(x₁)]	=	x₁ + 33470
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 6019
[and(x₁, x₂)]	=	x₁ + x₂ + 6029
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 11
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	2
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	6
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	5
[U33(x₁)]	=	7
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + 6028
[U61(x₁)]	=	4
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	3
[U41^#(x₁, x₂)]	=	x₁ + x₂ + 0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	9
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	x₁ + 21
[U22(x₁)]	=	x₁ + 56558
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 39487
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₁ + x₂ + 22493
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U61(active(X))	→	U61(X)	(95)

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

U41^#(mark(X1),X2)	→	U41^#(X1,X2)	(179)
U41^#(X1,mark(X2))	→	U41^#(X1,X2)	(250)
U41^#(X1,active(X2))	→	U41^#(X1,X2)	(143)
U41^#(active(X1),X2)	→	U41^#(X1,X2)	(123)

could be deleted.

1.1.17.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 18^th component contains the pair

isNatKind^#(active(X))	→	isNatKind^#(X)	(132)
isNatKind^#(mark(X))	→	isNatKind^#(X)	(114)

1.1.18 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 2
[U21(x₁, x₂)]	=	x₁ + x₂ + 18781
[U11(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 55679
[s(x₁)]	=	x₁ + 18728
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 20981
[and(x₁, x₂)]	=	x₁ + x₂ + 20991
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 55689
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	1
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	5
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	5
[U33(x₁)]	=	7
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + 20991
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 2
[U31(x₁, x₂, x₃)]	=	3
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	9
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	x₁ + 55699
[U22(x₁)]	=	x₁ + 18791
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 39708
[isNatKind^#(x₁)]	=	x₁ + 0
[U41(x₁, x₂)]	=	x₁ + x₂ + 5739
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U61(active(X))	→	U61(X)	(95)

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

isNatKind^#(active(X))	→	isNatKind^#(X)	(132)
isNatKind^#(mark(X))	→	isNatKind^#(X)	(114)

could be deleted.

1.1.18.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 19^th component contains the pair

U13^#(mark(X))	→	U13^#(X)	(246)
U13^#(active(X))	→	U13^#(X)	(121)

1.1.19 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U32^#(x₁, x₂)]	=	0
[isNatKind(x₁)]	=	x₁ + 1
[U21(x₁, x₂)]	=	x₁ + x₂ + 7319
[U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 7320
[s(x₁)]	=	x₁ + 40283
[isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + 2508
[and(x₁, x₂)]	=	x₁ + x₂ + 44029
[plus^#(x₁, x₂)]	=	0
[U13^#(x₁)]	=	x₁ + 0
[U12(x₁, x₂)]	=	x₁ + 14638
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	2393
[U12^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	21957
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[U32(x₁, x₂)]	=	14639
[U33(x₁)]	=	21958
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + 36711
[U61(x₁)]	=	9712
[U51^#(x₁, x₂, x₃)]	=	0
[U11^#(x₁, x₂, x₃)]	=	0
[active(x₁)]	=	x₁ + 7319
[U31(x₁, x₂, x₃)]	=	7320
[U41^#(x₁, x₂)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	0
[U22^#(x₁)]	=	0
[tt]	=	29277
[U71^#(x₁, x₂, x₃)]	=	0
[U13(x₁)]	=	x₁ + 51233
[U22(x₁)]	=	x₁ + 43914
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 40398
[isNatKind^#(x₁)]	=	0
[U41(x₁, x₂)]	=	x₁ + x₂ + 46035
[U31^#(x₁, x₂, x₃)]	=	0
[and^#(x₁, x₂)]	=	0
[U61^#(x₁)]	=	0

together with the usable rules

U33(active(X))	→	U33(X)	(77)
isNatKind(active(X))	→	isNatKind(X)	(111)
isNat(mark(X))	→	isNat(X)	(56)
U61(mark(X))	→	U61(X)	(94)
U33(mark(X))	→	U33(X)	(76)
isNat(active(X))	→	isNat(X)	(57)
isNatKind(mark(X))	→	isNatKind(X)	(110)
U61(active(X))	→	U61(X)	(95)

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

U13^#(mark(X))	→	U13^#(X)	(246)
U13^#(active(X))	→	U13^#(X)	(121)

could be deleted.

1.1.19.1 Dependency Graph Processor

The dependency pairs are split into 0 components.