Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/OvConsOS_complete_noand_GM)

The rewrite relation of the following TRS is considered.

There are 177 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 196 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(372)
mark^#(U131(X1,X2,X3,X4))	→	mark^#(X1)	(279)
mark^#(U122(X))	→	mark^#(X)	(277)
mark^#(U12(X1,X2))	→	mark^#(X1)	(369)
mark^#(U93(X1,X2,X3))	→	mark^#(X1)	(274)
mark^#(U132(X1,X2,X3,X4))	→	a__U132^#(mark(X1),X2,X3,X4)	(272)
mark^#(U22(X1,X2))	→	mark^#(X1)	(273)
mark^#(U134(X1,X2,X3,X4))	→	a__U134^#(mark(X1),X2,X3,X4)	(266)
mark^#(U136(X1,X2,X3,X4))	→	mark^#(X1)	(263)
a__U133^#(tt,IL,M,N)	→	a__U134^#(a__isNatKind(M),IL,M,N)	(262)
mark^#(U133(X1,X2,X3,X4))	→	a__U133^#(mark(X1),X2,X3,X4)	(261)
a__take^#(s(M),cons(N,IL))	→	a__U131^#(a__isNatIList(IL),IL,M,N)	(260)
mark^#(length(X))	→	a__length^#(mark(X))	(357)
a__U131^#(tt,IL,M,N)	→	a__U132^#(a__isNatIListKind(IL),IL,M,N)	(355)
mark^#(U102(X1,X2,X3))	→	mark^#(X1)	(257)
a__U132^#(tt,IL,M,N)	→	a__U133^#(a__isNat(M),IL,M,N)	(354)
mark^#(U136(X1,X2,X3,X4))	→	a__U136^#(mark(X1),X2,X3,X4)	(255)
mark^#(U52(X))	→	mark^#(X)	(349)
a__U113^#(tt,L,N)	→	a__U114^#(a__isNatKind(N),L)	(250)
mark^#(U94(X1,X2,X3))	→	mark^#(X1)	(348)
mark^#(U134(X1,X2,X3,X4))	→	mark^#(X1)	(249)
mark^#(U43(X1,X2,X3))	→	mark^#(X1)	(245)
mark^#(U113(X1,X2,X3))	→	a__U113^#(mark(X1),X2,X3)	(246)
mark^#(U21(X1,X2))	→	mark^#(X1)	(247)
mark^#(U44(X1,X2,X3))	→	mark^#(X1)	(244)
mark^#(U103(X1,X2,X3))	→	mark^#(X1)	(344)
a__U112^#(tt,L,N)	→	a__U113^#(a__isNat(N),L,N)	(343)
a__U111^#(tt,L,N)	→	a__U112^#(a__isNatIListKind(L),L,N)	(342)
mark^#(U112(X1,X2,X3))	→	a__U112^#(mark(X1),X2,X3)	(339)
a__U114^#(tt,L)	→	mark^#(L)	(338)
mark^#(U33(X))	→	mark^#(X)	(240)
mark^#(U91(X1,X2,X3))	→	mark^#(X1)	(337)
mark^#(U114(X1,X2))	→	mark^#(X1)	(239)
mark^#(U132(X1,X2,X3,X4))	→	mark^#(X1)	(334)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(332)
a__U135^#(tt,IL,M,N)	→	a__U136^#(a__isNatKind(N),IL,M,N)	(333)
mark^#(U131(X1,X2,X3,X4))	→	a__U131^#(mark(X1),X2,X3,X4)	(235)
mark^#(U111(X1,X2,X3))	→	mark^#(X1)	(331)
mark^#(U133(X1,X2,X3,X4))	→	mark^#(X1)	(327)
mark^#(take(X1,X2))	→	mark^#(X1)	(328)
mark^#(U11(X1,X2))	→	mark^#(X1)	(233)
mark^#(U92(X1,X2,X3))	→	mark^#(X1)	(326)
mark^#(U113(X1,X2,X3))	→	mark^#(X1)	(228)
mark^#(U121(X1,X2))	→	mark^#(X1)	(222)
mark^#(cons(X1,X2))	→	mark^#(X1)	(318)
mark^#(U45(X1,X2))	→	mark^#(X1)	(221)
mark^#(U135(X1,X2,X3,X4))	→	a__U135^#(mark(X1),X2,X3,X4)	(317)
a__U136^#(tt,IL,M,N)	→	mark^#(N)	(219)
mark^#(U135(X1,X2,X3,X4))	→	mark^#(X1)	(214)
mark^#(U61(X1,X2))	→	mark^#(X1)	(213)
mark^#(U32(X1,X2))	→	mark^#(X1)	(310)
mark^#(U62(X))	→	mark^#(X)	(210)
mark^#(U104(X1,X2,X3))	→	mark^#(X1)	(309)
mark^#(U106(X))	→	mark^#(X)	(208)
mark^#(U81(X))	→	mark^#(X)	(206)
a__length^#(cons(N,L))	→	a__U111^#(a__isNatList(L),L,N)	(205)
a__U134^#(tt,IL,M,N)	→	a__U135^#(a__isNat(N),IL,M,N)	(307)
mark^#(U13(X))	→	mark^#(X)	(202)
mark^#(U31(X1,X2))	→	mark^#(X1)	(305)
mark^#(U111(X1,X2,X3))	→	a__U111^#(mark(X1),X2,X3)	(200)
mark^#(U46(X))	→	mark^#(X)	(303)
mark^#(U23(X))	→	mark^#(X)	(198)
mark^#(U105(X1,X2))	→	mark^#(X1)	(302)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(299)
a__U114^#(tt,L)	→	a__length^#(mark(L))	(194)
mark^#(U101(X1,X2,X3))	→	mark^#(X1)	(292)
mark^#(U71(X))	→	mark^#(X)	(187)
mark^#(U114(X1,X2))	→	a__U114^#(mark(X1),X2)	(290)
mark^#(U96(X))	→	mark^#(X)	(289)
mark^#(length(X))	→	mark^#(X)	(288)
mark^#(s(X))	→	mark^#(X)	(287)
mark^#(U95(X1,X2))	→	mark^#(X1)	(285)
mark^#(U51(X1,X2))	→	mark^#(X1)	(283)
mark^#(U112(X1,X2,X3))	→	mark^#(X1)	(179)
mark^#(take(X1,X2))	→	mark^#(X2)	(281)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	0
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	24635
[a__U131^#(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 56408
[U21(x₁, x₂)]	=	x₁ + 0
[a__U102(x₁, x₂, x₃)]	=	x₁ + 0
[a__U45(x₁, x₂)]	=	x₁ + 0
[isNatList(x₁)]	=	24635
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₁ + 0
[a__U92^#(x₁, x₂, x₃)]	=	0
[a__U104(x₁, x₂, x₃)]	=	x₁ + 0
[U136(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U112^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[s(x₁)]	=	x₁ + 0
[a__U133^#(x₁,...,x₄)]	=	x₄ + 56408
[U105(x₁, x₂)]	=	x₁ + 0
[a__U31^#(x₁, x₂)]	=	0
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	0
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 8922
[a__isNatIList(x₁)]	=	24635
[a__U33(x₁)]	=	x₁ + 0
[U106(x₁)]	=	x₁ + 0
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₁ + 0
[U42(x₁, x₂, x₃)]	=	x₁ + 0
[U91(x₁, x₂, x₃)]	=	x₁ + 0
[a__isNat^#(x₁)]	=	0
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	x₄ + 24635
[take(x₁, x₂)]	=	x₁ + x₂ + 56410
[U71(x₁)]	=	x₁ + 0
[a__U62(x₁)]	=	x₁ + 0
[a__U44(x₁, x₂, x₃)]	=	x₁ + 0
[U131(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[isNatIList(x₁)]	=	24635
[U135(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[U101(x₁, x₂, x₃)]	=	x₁ + 0
[a__U43^#(x₁, x₂, x₃)]	=	0
[U95(x₁, x₂)]	=	x₁ + 0
[U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[U43(x₁, x₂, x₃)]	=	x₁ + 0
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₁ + 12267
[a__U135^#(x₁,...,x₄)]	=	x₄ + 24636
[a__U44^#(x₁, x₂, x₃)]	=	0
[U103(x₁, x₂, x₃)]	=	x₁ + 0
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[a__U103^#(x₁, x₂, x₃)]	=	0
[U44(x₁, x₂, x₃)]	=	x₁ + 0
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	x₂ + 24635
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 0
[a__U22(x₁, x₂)]	=	x₁ + 0
[U93(x₁, x₂, x₃)]	=	x₁ + 0
[a__U94(x₁, x₂, x₃)]	=	x₁ + 0
[a__U106(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂)]	=	0
[U94(x₁, x₂, x₃)]	=	x₁ + 0
[zeros]	=	1
[a__U31(x₁, x₂)]	=	x₁ + 0
[a__U51(x₁, x₂)]	=	x₁ + 0
[a__U81(x₁)]	=	x₁ + 0
[a__take^#(x₁, x₂)]	=	x₂ + 81043
[U12(x₁, x₂)]	=	x₁ + 0
[a__isNatList(x₁)]	=	24635
[a__U43(x₁, x₂, x₃)]	=	x₁ + 0
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U42^#(x₁, x₂, x₃)]	=	0
[a__U41(x₁, x₂, x₃)]	=	x₁ + 0
[a__U134(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	0
[U104(x₁, x₂, x₃)]	=	x₁ + 0
[a__U122(x₁)]	=	x₁ + 5037
[a__U21^#(x₁, x₂)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[mark^#(x₁)]	=	x₁ + 24634
[0]	=	0
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 24635
[U134(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U21(x₁, x₂)]	=	x₁ + 0
[a__U32(x₁, x₂)]	=	x₁ + 0
[a__U91(x₁, x₂, x₃)]	=	x₁ + 0
[a__U111^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 24635
[nil]	=	1
[isNatIListKind(x₁)]	=	24635
[U114(x₁, x₂)]	=	x₁ + x₂ + 8922
[U62(x₁)]	=	x₁ + 0
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	0
[U45(x₁, x₂)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 0
[U133(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U101^#(x₁, x₂, x₃)]	=	0
[a__U11(x₁, x₂)]	=	x₁ + 0
[U32(x₁, x₂)]	=	x₁ + 0
[a__U42(x₁, x₂, x₃)]	=	x₁ + 0
[a__U93(x₁, x₂, x₃)]	=	x₁ + 0
[U33(x₁)]	=	x₁ + 0
[a__U45^#(x₁, x₂)]	=	0
[a__U52(x₁)]	=	x₁ + 0
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__length^#(x₁)]	=	x₁ + 24635
[a__U105^#(x₁, x₂)]	=	0
[a__U12(x₁, x₂)]	=	x₁ + 0
[a__isNatIListKind(x₁)]	=	24635
[a__U104^#(x₁, x₂, x₃)]	=	0
[isNat(x₁)]	=	24635
[U46(x₁)]	=	x₁ + 0
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	x₁ + 0
[U61(x₁, x₂)]	=	x₁ + 0
[a__U46(x₁)]	=	x₁ + 0
[a__U22^#(x₁, x₂)]	=	0
[a__U113(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[U96(x₁)]	=	x₁ + 0
[a__U13(x₁)]	=	x₁ + 0
[U31(x₁, x₂)]	=	x₁ + 0
[a__isNatList^#(x₁)]	=	0
[a__U71(x₁)]	=	x₁ + 0
[U92(x₁, x₂, x₃)]	=	x₁ + 0
[U112(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U92(x₁, x₂, x₃)]	=	x₁ + 0
[a__U61(x₁, x₂)]	=	x₁ + 0
[U102(x₁, x₂, x₃)]	=	x₁ + 0
[a__U105(x₁, x₂)]	=	x₁ + 0
[a__take(x₁, x₂)]	=	x₁ + x₂ + 56410
[U81(x₁)]	=	x₁ + 0
[a__U95^#(x₁, x₂)]	=	0
[a__U41^#(x₁, x₂, x₃)]	=	0
[tt]	=	24635
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__isNat(x₁)]	=	24635
[U13(x₁)]	=	x₁ + 0
[a__U133(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 31775
[a__U23(x₁)]	=	x₁ + 0
[a__U96(x₁)]	=	x₁ + 0
[a__isNatKind(x₁)]	=	24635
[a__U134^#(x₁,...,x₄)]	=	x₄ + 56407
[U22(x₁, x₂)]	=	x₁ + 0
[U51(x₁, x₂)]	=	x₁ + 0
[a__U132^#(x₁,...,x₄)]	=	x₂ + x₄ + 56409
[a__U103(x₁, x₂, x₃)]	=	x₁ + 0
[length(x₁)]	=	x₁ + 33557
[a__U112(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8922
[U41(x₁, x₂, x₃)]	=	x₁ + 0
[a__U32^#(x₁, x₂)]	=	0
[a__zeros]	=	1
[a__U101(x₁, x₂, x₃)]	=	x₁ + 0
[a__U91^#(x₁, x₂, x₃)]	=	0
[U121(x₁, x₂)]	=	x₁ + 12267
[a__length(x₁)]	=	x₁ + 33557
[U122(x₁)]	=	x₁ + 5037

together with the usable rules

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

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

mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(372)
mark^#(U131(X1,X2,X3,X4))	→	mark^#(X1)	(279)
mark^#(U122(X))	→	mark^#(X)	(277)
mark^#(U134(X1,X2,X3,X4))	→	a__U134^#(mark(X1),X2,X3,X4)	(266)
mark^#(U136(X1,X2,X3,X4))	→	mark^#(X1)	(263)
a__U133^#(tt,IL,M,N)	→	a__U134^#(a__isNatKind(M),IL,M,N)	(262)
mark^#(U133(X1,X2,X3,X4))	→	a__U133^#(mark(X1),X2,X3,X4)	(261)
mark^#(length(X))	→	a__length^#(mark(X))	(357)
a__U131^#(tt,IL,M,N)	→	a__U132^#(a__isNatIListKind(IL),IL,M,N)	(355)
a__U132^#(tt,IL,M,N)	→	a__U133^#(a__isNat(M),IL,M,N)	(354)
mark^#(U136(X1,X2,X3,X4))	→	a__U136^#(mark(X1),X2,X3,X4)	(255)
mark^#(U134(X1,X2,X3,X4))	→	mark^#(X1)	(249)
mark^#(U113(X1,X2,X3))	→	a__U113^#(mark(X1),X2,X3)	(246)
mark^#(U112(X1,X2,X3))	→	a__U112^#(mark(X1),X2,X3)	(339)
a__U114^#(tt,L)	→	mark^#(L)	(338)
mark^#(U114(X1,X2))	→	mark^#(X1)	(239)
mark^#(U132(X1,X2,X3,X4))	→	mark^#(X1)	(334)
a__U135^#(tt,IL,M,N)	→	a__U136^#(a__isNatKind(N),IL,M,N)	(333)
mark^#(U131(X1,X2,X3,X4))	→	a__U131^#(mark(X1),X2,X3,X4)	(235)
mark^#(U111(X1,X2,X3))	→	mark^#(X1)	(331)
mark^#(U133(X1,X2,X3,X4))	→	mark^#(X1)	(327)
mark^#(take(X1,X2))	→	mark^#(X1)	(328)
mark^#(U113(X1,X2,X3))	→	mark^#(X1)	(228)
mark^#(U121(X1,X2))	→	mark^#(X1)	(222)
mark^#(U135(X1,X2,X3,X4))	→	a__U135^#(mark(X1),X2,X3,X4)	(317)
a__U136^#(tt,IL,M,N)	→	mark^#(N)	(219)
mark^#(U135(X1,X2,X3,X4))	→	mark^#(X1)	(214)
a__U134^#(tt,IL,M,N)	→	a__U135^#(a__isNat(N),IL,M,N)	(307)
mark^#(U111(X1,X2,X3))	→	a__U111^#(mark(X1),X2,X3)	(200)
mark^#(U114(X1,X2))	→	a__U114^#(mark(X1),X2)	(290)
mark^#(length(X))	→	mark^#(X)	(288)
mark^#(U112(X1,X2,X3))	→	mark^#(X1)	(179)
mark^#(take(X1,X2))	→	mark^#(X2)	(281)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__length^#(cons(N,L))	→	a__U111^#(a__isNatList(L),L,N)	(205)
a__U112^#(tt,L,N)	→	a__U113^#(a__isNat(N),L,N)	(343)
a__U114^#(tt,L)	→	a__length^#(mark(L))	(194)
a__U113^#(tt,L,N)	→	a__U114^#(a__isNatKind(N),L)	(250)
a__U111^#(tt,L,N)	→	a__U112^#(a__isNatIListKind(L),L,N)	(342)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[a__U94^#(x₁, x₂, x₃)]

[a__isNatKind^#(x₁)]

[isNatKind(x₁)]

30422

30423

[a__U131^#(x₁,...,x₄)]

[U21(x₁, x₂)]

1	0
0	0

· x₁ +

[a__U102(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[a__U45(x₁, x₂)]

30422

[isNatList(x₁)]

0	1
0	0

· x₁ +

[a__U71^#(x₁)]

[U11(x₁, x₂)]

30423

[a__U92^#(x₁, x₂, x₃)]

[a__U104(x₁, x₂, x₃)]

30422

[U136(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[a__U112^#(x₁, x₂, x₃)]

1	0
1	1

· x₂ +

30421

[s(x₁)]

x₁ +

30422

[a__U133^#(x₁,...,x₄)]

[U105(x₁, x₂)]

30422

[a__U31^#(x₁, x₂)]

[a__U132(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__U33^#(x₁)]

[a__U93^#(x₁, x₂, x₃)]

[a__U114(x₁, x₂)]

1	0
1	0

· x₂ +

68394

12839

[a__isNatIList(x₁)]

1	1
1	0

· x₁ +

30422

[a__U33(x₁)]

1	0
0	0

· x₁ +

30422

[U106(x₁)]

30422

[a__isNatIListKind^#(x₁)]

[a__U23^#(x₁)]

[a__U95(x₁, x₂)]

30422

[U42(x₁, x₂, x₃)]

1	0
1	0

· x₁ +

1	1
1	1

· x₃ +

[U91(x₁, x₂, x₃)]

1	0
0	0

· x₃ +

[a__isNat^#(x₁)]

[a__U106^#(x₁)]

[a__U136^#(x₁,...,x₄)]

[take(x₁, x₂)]

1	0
0	0

· x₁ +

1	0
0	0

· x₂ +

73677

30422

[U71(x₁)]

30422

30423

[a__U62(x₁)]

1	0
1	0

· x₁ +

21120

[a__U44(x₁, x₂, x₃)]

30422

[U131(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[isNatIList(x₁)]

1	1
0	0

· x₁ +

30422

[U135(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[U101(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[a__U43^#(x₁, x₂, x₃)]

[U95(x₁, x₂)]

30422

[U111(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

1	0
1	0

· x₂ +

37972

[U132(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[U43(x₁, x₂, x₃)]

1	0
1	0

· x₁ +

11346

[a__U13^#(x₁)]

[a__U121(x₁, x₂)]

1	0
1	0

· x₂ +

30422

[a__U135^#(x₁,...,x₄)]

[a__U44^#(x₁, x₂, x₃)]

[U103(x₁, x₂, x₃)]

30422

[a__U111(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

1	0
1	0

· x₂ +

37972

12839

[a__U103^#(x₁, x₂, x₃)]

[U44(x₁, x₂, x₃)]

30422

[a__U46^#(x₁)]

[a__U114^#(x₁, x₂)]

1	0
1	1

· x₂ +

30419

[a__U51^#(x₁, x₂)]

[U23(x₁)]

30422

[a__U22(x₁, x₂)]

1	0
0	0

· x₁ +

[U93(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[a__U94(x₁, x₂, x₃)]

30422

[a__U106(x₁)]

30422

[a__U11^#(x₁, x₂)]

[U94(x₁, x₂, x₃)]

30422

[zeros]

30422

[a__U31(x₁, x₂)]

1	1
1	0

· x₂ +

30422

[a__U51(x₁, x₂)]

1	0
1	0

· x₂ +

[a__U81(x₁)]

30422

[a__take^#(x₁, x₂)]

[U12(x₁, x₂)]

30423

[a__isNatList(x₁)]

0	1
0	0

· x₁ +

[a__U43(x₁, x₂, x₃)]

1	0
1	0

· x₁ +

11346

[a__U62^#(x₁)]

[a__U136(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__U42^#(x₁, x₂, x₃)]

[a__U41(x₁, x₂, x₃)]

1	1
1	1

· x₃ +

30422

[a__U134(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__U122^#(x₁)]

[a__U12^#(x₁, x₂)]

[U104(x₁, x₂, x₃)]

30422

[a__U122(x₁)]

x₁ +

30422

[a__U21^#(x₁, x₂)]

[a__isNatIList^#(x₁)]

[a__U81^#(x₁)]

[a__U61^#(x₁, x₂)]

[U113(x₁, x₂, x₃)]

1	0
1	0

· x₂ +

68394

[mark^#(x₁)]

[0]

[a__zeros^#]

[a__U113^#(x₁, x₂, x₃)]

1	0
1	1

· x₂ +

30420

[U134(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[a__U21(x₁, x₂)]

1	0
0	0

· x₁ +

[a__U32(x₁, x₂)]

1	1
1	0

· x₂ +

30422

[a__U91(x₁, x₂, x₃)]

1	0
0	0

· x₃ +

[a__U111^#(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

1	0
1	1

· x₂ +

[nil]

30422

[isNatIListKind(x₁)]

1	0
0	0

· x₁ +

[U114(x₁, x₂)]

1	0
1	0

· x₂ +

68394

[U62(x₁)]

1	0
0	0

· x₁ +

21120

[a__U52^#(x₁)]

[a__U102^#(x₁, x₂, x₃)]

[U45(x₁, x₂)]

30422

[mark(x₁)]

1	0
1	0

· x₁ +

[U133(x₁,...,x₄)]

1	0
0	0

· x₂ +

1	0
0	0

· x₃ +

1	0
0	0

· x₄ +

104099

[a__U101^#(x₁, x₂, x₃)]

[a__U11(x₁, x₂)]

30423

[U32(x₁, x₂)]

1	1
1	0

· x₂ +

30422

[a__U42(x₁, x₂, x₃)]

1	0
1	0

· x₁ +

1	1
1	1

· x₃ +

[a__U93(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[U33(x₁)]

1	0
0	0

· x₁ +

30422

[a__U45^#(x₁, x₂)]

[a__U52(x₁)]

1	0
1	0

· x₁ +

[a__U96^#(x₁)]

[a__U135(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__length^#(x₁)]

0	1
1	0

· x₁ +

30417

[a__U105^#(x₁, x₂)]

[a__U12(x₁, x₂)]

30423

[a__isNatIListKind(x₁)]

1	0
1	0

· x₁ +

[a__U104^#(x₁, x₂, x₃)]

[isNat(x₁)]

0	1
0	0

· x₁ +

30423

[U46(x₁)]

30422

[a__U121^#(x₁, x₂)]

[U52(x₁)]

1	0
0	0

· x₁ +

[U61(x₁, x₂)]

1	0
1	0

· x₁ +

1	0
0	0

· x₂ +

43255

[a__U46(x₁)]

30422

[a__U22^#(x₁, x₂)]

[a__U113(x₁, x₂, x₃)]

1	0
1	0

· x₂ +

68394

12839

[U96(x₁)]

30422

[a__U13(x₁)]

30423

[U31(x₁, x₂)]

1	1
1	0

· x₂ +

30422

[a__isNatList^#(x₁)]

[a__U71(x₁)]

30422

30423

[U92(x₁, x₂, x₃)]

1	0
0	0

· x₃ +

[U112(x₁, x₂, x₃)]

1	0
1	0

· x₂ +

68394

[cons(x₁, x₂)]

x₁ +

1	1
1	1

· x₂ +

[a__U92(x₁, x₂, x₃)]

1	0
0	0

· x₃ +

[a__U61(x₁, x₂)]

1	0
1	0

· x₁ +

1	0
1	0

· x₂ +

43255

[U102(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[a__U105(x₁, x₂)]

30422

[a__take(x₁, x₂)]

1	0
1	0

· x₁ +

1	0
1	0

· x₂ +

73677

73678

[U81(x₁)]

30422

[a__U95^#(x₁, x₂)]

[a__U41^#(x₁, x₂, x₃)]

[tt]

30422

[a__U131(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__isNat(x₁)]

0	1
0	0

· x₁ +

30423

[U13(x₁)]

30423

[a__U133(x₁,...,x₄)]

1	0
1	0

· x₂ +

1	0
1	0

· x₃ +

1	0
1	0

· x₄ +

104099

104100

[a__U23(x₁)]

30422

[a__U96(x₁)]

30422

[a__isNatKind(x₁)]

30422

30423

[a__U134^#(x₁,...,x₄)]

[U22(x₁, x₂)]

1	0
0	0

· x₁ +

[U51(x₁, x₂)]

1	0
0	0

· x₂ +

[a__U132^#(x₁,...,x₄)]

[a__U103(x₁, x₂, x₃)]

30422

[length(x₁)]

1	0
1	0

· x₁ +

37972

[a__U112(x₁, x₂, x₃)]

1	0
1	0

· x₂ +

68394

12839

[U41(x₁, x₂, x₃)]

1	1
1	1

· x₃ +

30422

[a__U32^#(x₁, x₂)]

[a__zeros]

30422

30423

[a__U101(x₁, x₂, x₃)]

1	0
0	0

· x₁ +

[a__U91^#(x₁, x₂, x₃)]

[U121(x₁, x₂)]

1	0
0	0

· x₂ +

30422

[a__length(x₁)]

1	0
1	0

· x₁ +

37972

12839

[U122(x₁)]

1	0
0	0

· x₁ +

30422

together with the usable rules

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

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

a__length^#(cons(N,L))	→	a__U111^#(a__isNatList(L),L,N)	(205)
a__U112^#(tt,L,N)	→	a__U113^#(a__isNat(N),L,N)	(343)
a__U114^#(tt,L)	→	a__length^#(mark(L))	(194)
a__U113^#(tt,L,N)	→	a__U114^#(a__isNatKind(N),L)	(250)
a__U111^#(tt,L,N)	→	a__U112^#(a__isNatIListKind(L),L,N)	(342)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

mark^#(U43(X1,X2,X3))	→	mark^#(X1)	(245)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(332)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(299)
mark^#(U101(X1,X2,X3))	→	mark^#(X1)	(292)
mark^#(U13(X))	→	mark^#(X)	(202)
mark^#(U32(X1,X2))	→	mark^#(X1)	(310)
mark^#(U44(X1,X2,X3))	→	mark^#(X1)	(244)
mark^#(U94(X1,X2,X3))	→	mark^#(X1)	(348)
mark^#(cons(X1,X2))	→	mark^#(X1)	(318)
mark^#(U96(X))	→	mark^#(X)	(289)
mark^#(U51(X1,X2))	→	mark^#(X1)	(283)
mark^#(U45(X1,X2))	→	mark^#(X1)	(221)
mark^#(U62(X))	→	mark^#(X)	(210)
mark^#(U12(X1,X2))	→	mark^#(X1)	(369)
mark^#(U33(X))	→	mark^#(X)	(240)
mark^#(U102(X1,X2,X3))	→	mark^#(X1)	(257)
mark^#(U21(X1,X2))	→	mark^#(X1)	(247)
mark^#(U11(X1,X2))	→	mark^#(X1)	(233)
mark^#(U95(X1,X2))	→	mark^#(X1)	(285)
mark^#(U52(X))	→	mark^#(X)	(349)
mark^#(U106(X))	→	mark^#(X)	(208)
mark^#(U23(X))	→	mark^#(X)	(198)
mark^#(U46(X))	→	mark^#(X)	(303)
mark^#(U61(X1,X2))	→	mark^#(X1)	(213)
mark^#(U93(X1,X2,X3))	→	mark^#(X1)	(274)
mark^#(U81(X))	→	mark^#(X)	(206)
mark^#(U105(X1,X2))	→	mark^#(X1)	(302)
mark^#(U71(X))	→	mark^#(X)	(187)
mark^#(s(X))	→	mark^#(X)	(287)
mark^#(U103(X1,X2,X3))	→	mark^#(X1)	(344)
mark^#(U104(X1,X2,X3))	→	mark^#(X1)	(309)
mark^#(U22(X1,X2))	→	mark^#(X1)	(273)
mark^#(U31(X1,X2))	→	mark^#(X1)	(305)
mark^#(U91(X1,X2,X3))	→	mark^#(X1)	(337)
mark^#(U92(X1,X2,X3))	→	mark^#(X1)	(326)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	0
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	x₁ + 4
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + 5
[a__U102(x₁, x₂, x₃)]	=	x₂ + x₃ + 7
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 32
[isNatList(x₁)]	=	3
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₁ + 4
[a__U92^#(x₁, x₂, x₃)]	=	0
[a__U104(x₁, x₂, x₃)]	=	x₁ + x₃ + 10
[U136(x₁,...,x₄)]	=	x₁ + x₄ + 31775
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 8945
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + 24633
[a__U31^#(x₁, x₂)]	=	0
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 5
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	0
[a__U114(x₁, x₂)]	=	x₂ + 8943
[a__isNatIList(x₁)]	=	x₁ + 2
[a__U33(x₁)]	=	8
[U106(x₁)]	=	x₁ + 16
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₁ + 11
[U42(x₁, x₂, x₃)]	=	x₁ + 25
[U91(x₁, x₂, x₃)]	=	x₁ + 4
[a__isNat^#(x₁)]	=	0
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 56410
[U71(x₁)]	=	x₁ + 3
[a__U62(x₁)]	=	x₁ + 2
[a__U44(x₁, x₂, x₃)]	=	x₂ + 33
[U131(x₁,...,x₄)]	=	2
[isNatIList(x₁)]	=	3
[U135(x₁,...,x₄)]	=	x₁ + x₃ + 13
[U101(x₁, x₂, x₃)]	=	x₁ + 2
[a__U43^#(x₁, x₂, x₃)]	=	0
[U95(x₁, x₂)]	=	x₁ + 12
[U111(x₁, x₂, x₃)]	=	x₁ + x₂ + 8941
[U132(x₁,...,x₄)]	=	x₃ + 31779
[U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 28
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₁ + 1
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	0
[U103(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 7
[a__U111(x₁, x₂, x₃)]	=	x₃ + 8940
[a__U103^#(x₁, x₂, x₃)]	=	0
[U44(x₁, x₂, x₃)]	=	x₁ + x₃ + 34
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 10
[a__U22(x₁, x₂)]	=	x₂ + 10
[U93(x₁, x₂, x₃)]	=	x₁ + x₃ + 6
[a__U94(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 9
[a__U106(x₁)]	=	x₁ + 15
[a__U11^#(x₁, x₂)]	=	0
[U94(x₁, x₂, x₃)]	=	x₁ + 10
[zeros]	=	0
[a__U31(x₁, x₂)]	=	x₁ + 1
[a__U51(x₁, x₂)]	=	x₂ + 3
[a__U81(x₁)]	=	4
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + 8
[a__isNatList(x₁)]	=	2
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₃ + 27
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 15
[a__U42^#(x₁, x₂, x₃)]	=	0
[a__U41(x₁, x₂, x₃)]	=	23
[a__U134(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 10
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	0
[U104(x₁, x₂, x₃)]	=	x₁ + 11
[a__U122(x₁)]	=	7
[a__U21^#(x₁, x₂)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₂ + 8943
[mark^#(x₁)]	=	x₁ + 24634
[0]	=	3481
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + 11
[a__U21(x₁, x₂)]	=	x₁ + x₂ + 4
[a__U32(x₁, x₂)]	=	x₂ + 7
[a__U91(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	8
[isNatIListKind(x₁)]	=	3
[U114(x₁, x₂)]	=	x₁ + 8944
[U62(x₁)]	=	x₁ + 3
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	0
[U45(x₁, x₂)]	=	x₁ + 33
[mark(x₁)]	=	1
[U133(x₁,...,x₄)]	=	x₁ + x₃ + 31778
[a__U101^#(x₁, x₂, x₃)]	=	0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 3
[U32(x₁, x₂)]	=	x₁ + 8
[a__U42(x₁, x₂, x₃)]	=	x₂ + 24
[a__U93(x₁, x₂, x₃)]	=	x₁ + 5
[U33(x₁)]	=	x₁ + 9
[a__U45^#(x₁, x₂)]	=	0
[a__U52(x₁)]	=	4
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₁ + x₄ + 12
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	0
[a__U12(x₁, x₂)]	=	x₁ + x₂ + 7
[a__isNatIListKind(x₁)]	=	2
[a__U104^#(x₁, x₂, x₃)]	=	0
[isNat(x₁)]	=	5
[U46(x₁)]	=	x₁ + 3
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	x₁ + 5
[U61(x₁, x₂)]	=	x₁ + x₂ + 4
[a__U46(x₁)]	=	2
[a__U22^#(x₁, x₂)]	=	0
[a__U113(x₁, x₂, x₃)]	=	x₃ + 8942
[U96(x₁)]	=	x₁ + 18
[a__U13(x₁)]	=	13
[U31(x₁, x₂)]	=	x₁ + 2
[a__isNatList^#(x₁)]	=	0
[a__U71(x₁)]	=	x₁ + 2
[U92(x₁, x₂, x₃)]	=	x₁ + x₂ + 2
[U112(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8942
[cons(x₁, x₂)]	=	x₁ + 20
[a__U92(x₁, x₂, x₃)]	=	x₁ + 1
[a__U61(x₁, x₂)]	=	3
[U102(x₁, x₂, x₃)]	=	x₁ + 8
[a__U105(x₁, x₂)]	=	16
[a__take(x₁, x₂)]	=	2
[U81(x₁)]	=	x₁ + 5
[a__U95^#(x₁, x₂)]	=	0
[a__U41^#(x₁, x₂, x₃)]	=	0
[tt]	=	5
[a__U131(x₁,...,x₄)]	=	x₁ + x₃ + x₄ + 1
[a__isNat(x₁)]	=	4
[U13(x₁)]	=	x₁ + 14
[a__U133(x₁,...,x₄)]	=	x₁ + x₄ + 7
[a__U23(x₁)]	=	x₁ + 9
[a__U96(x₁)]	=	17
[a__isNatKind(x₁)]	=	3
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₁ + 11
[U51(x₁, x₂)]	=	x₁ + 4
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₁ + 6
[length(x₁)]	=	3473
[a__U112(x₁, x₂, x₃)]	=	8941
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 24
[a__U32^#(x₁, x₂)]	=	0
[a__zeros]	=	2
[a__U101(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U91^#(x₁, x₂, x₃)]	=	0
[U121(x₁, x₂)]	=	x₁ + x₂ + 12267
[a__length(x₁)]	=	x₁ + 3472
[U122(x₁)]	=	8

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

mark^#(U43(X1,X2,X3))	→	mark^#(X1)	(245)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(332)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(299)
mark^#(U101(X1,X2,X3))	→	mark^#(X1)	(292)
mark^#(U13(X))	→	mark^#(X)	(202)
mark^#(U32(X1,X2))	→	mark^#(X1)	(310)
mark^#(U44(X1,X2,X3))	→	mark^#(X1)	(244)
mark^#(U94(X1,X2,X3))	→	mark^#(X1)	(348)
mark^#(cons(X1,X2))	→	mark^#(X1)	(318)
mark^#(U96(X))	→	mark^#(X)	(289)
mark^#(U51(X1,X2))	→	mark^#(X1)	(283)
mark^#(U45(X1,X2))	→	mark^#(X1)	(221)
mark^#(U62(X))	→	mark^#(X)	(210)
mark^#(U12(X1,X2))	→	mark^#(X1)	(369)
mark^#(U33(X))	→	mark^#(X)	(240)
mark^#(U102(X1,X2,X3))	→	mark^#(X1)	(257)
mark^#(U21(X1,X2))	→	mark^#(X1)	(247)
mark^#(U11(X1,X2))	→	mark^#(X1)	(233)
mark^#(U95(X1,X2))	→	mark^#(X1)	(285)
mark^#(U52(X))	→	mark^#(X)	(349)
mark^#(U106(X))	→	mark^#(X)	(208)
mark^#(U23(X))	→	mark^#(X)	(198)
mark^#(U46(X))	→	mark^#(X)	(303)
mark^#(U61(X1,X2))	→	mark^#(X1)	(213)
mark^#(U93(X1,X2,X3))	→	mark^#(X1)	(274)
mark^#(U81(X))	→	mark^#(X)	(206)
mark^#(U105(X1,X2))	→	mark^#(X1)	(302)
mark^#(U71(X))	→	mark^#(X)	(187)
mark^#(s(X))	→	mark^#(X)	(287)
mark^#(U103(X1,X2,X3))	→	mark^#(X1)	(344)
mark^#(U104(X1,X2,X3))	→	mark^#(X1)	(309)
mark^#(U22(X1,X2))	→	mark^#(X1)	(273)
mark^#(U31(X1,X2))	→	mark^#(X1)	(305)
mark^#(U91(X1,X2,X3))	→	mark^#(X1)	(337)
mark^#(U92(X1,X2,X3))	→	mark^#(X1)	(326)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__isNatList^#(cons(V1,V2))	→	a__U91^#(a__isNatKind(V1),V1,V2)	(275)
a__U93^#(tt,V1,V2)	→	a__U94^#(a__isNatIListKind(V2),V1,V2)	(367)
a__U92^#(tt,V1,V2)	→	a__U93^#(a__isNatIListKind(V2),V1,V2)	(269)
a__U104^#(tt,V1,V2)	→	a__U105^#(a__isNat(V1),V2)	(363)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNatKind(V1),V1,V2)	(360)
a__U43^#(tt,V1,V2)	→	a__U44^#(a__isNatIListKind(V2),V1,V2)	(259)
a__U31^#(tt,V)	→	a__U32^#(a__isNatIListKind(V),V)	(358)
a__U105^#(tt,V2)	→	a__isNatIList^#(V2)	(353)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(253)
a__U101^#(tt,V1,V2)	→	a__U102^#(a__isNatKind(V1),V1,V2)	(350)
a__U91^#(tt,V1,V2)	→	a__U92^#(a__isNatKind(V1),V1,V2)	(345)
a__U11^#(tt,V1)	→	a__U12^#(a__isNatIListKind(V1),V1)	(340)
a__U104^#(tt,V1,V2)	→	a__isNat^#(V1)	(234)
a__U12^#(tt,V1)	→	a__isNatList^#(V1)	(231)
a__isNatList^#(take(V1,V2))	→	a__U101^#(a__isNatKind(V1),V1,V2)	(324)
a__isNatIList^#(V)	→	a__U31^#(a__isNatIListKind(V),V)	(227)
a__U103^#(tt,V1,V2)	→	a__U104^#(a__isNatIListKind(V2),V1,V2)	(321)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNatKind(V1),V1,V2)	(223)
a__U45^#(tt,V2)	→	a__isNatIList^#(V2)	(319)
a__U32^#(tt,V)	→	a__isNatList^#(V)	(315)
a__U102^#(tt,V1,V2)	→	a__U103^#(a__isNatIListKind(V2),V1,V2)	(209)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(207)
a__U94^#(tt,V1,V2)	→	a__U95^#(a__isNat(V1),V2)	(204)
a__U94^#(tt,V1,V2)	→	a__isNat^#(V1)	(304)
a__U44^#(tt,V1,V2)	→	a__isNat^#(V1)	(195)
a__U44^#(tt,V1,V2)	→	a__U45^#(a__isNat(V1),V2)	(298)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(192)
a__U42^#(tt,V1,V2)	→	a__U43^#(a__isNatIListKind(V2),V1,V2)	(293)
a__U95^#(tt,V2)	→	a__isNatList^#(V2)	(291)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(183)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	4271
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + 4257
[a__U102(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8502
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 4262
[isNatList(x₁)]	=	8506
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₂ + 4257
[a__U92^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8512
[a__U104(x₁, x₂, x₃)]	=	x₂ + 8509
[U136(x₁,...,x₄)]	=	x₄ + 8519
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 0
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + 8511
[a__U31^#(x₁, x₂)]	=	x₂ + 8514
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 2
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8512
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 4246
[a__isNatIList(x₁)]	=	x₁ + 4255
[a__U33(x₁)]	=	8514
[U106(x₁)]	=	8512
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₂ + 8510
[U42(x₁, x₂, x₃)]	=	x₁ + 8515
[U91(x₁, x₂, x₃)]	=	x₁ + x₃ + 8507
[a__isNat^#(x₁)]	=	x₁ + 8512
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 4265
[U71(x₁)]	=	2
[a__U62(x₁)]	=	8512
[a__U44(x₁, x₂, x₃)]	=	x₃ + 8516
[U131(x₁,...,x₄)]	=	x₄ + 2
[isNatIList(x₁)]	=	4256
[U135(x₁,...,x₄)]	=	x₂ + 8518
[U101(x₁, x₂, x₃)]	=	x₂ + 12772
[a__U43^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8515
[U95(x₁, x₂)]	=	8511
[U111(x₁, x₂, x₃)]	=	2
[U132(x₁,...,x₄)]	=	x₁ + 3
[U43(x₁, x₂, x₃)]	=	x₂ + 4
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₂ + 4256
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8515
[U103(x₁, x₂, x₃)]	=	x₂ + 17016
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U103^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8518
[U44(x₁, x₂, x₃)]	=	x₁ + 8517
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 8512
[a__U22(x₁, x₂)]	=	x₂ + 4257
[U93(x₁, x₂, x₃)]	=	8509
[a__U94(x₁, x₂, x₃)]	=	x₂ + x₃ + 8509
[a__U106(x₁)]	=	8511
[a__U11^#(x₁, x₂)]	=	x₂ + 8512
[U94(x₁, x₂, x₃)]	=	x₃ + 8510
[zeros]	=	4256
[a__U31(x₁, x₂)]	=	4256
[a__U51(x₁, x₂)]	=	8512
[a__U81(x₁)]	=	8511
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + x₂ + 4258
[a__isNatList(x₁)]	=	x₁ + 8505
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 3
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₂ + 8518
[a__U42^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8515
[a__U41(x₁, x₂, x₃)]	=	x₁ + 1
[a__U134(x₁,...,x₄)]	=	x₂ + x₄ + 8516
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	x₂ + 8512
[U104(x₁, x₂, x₃)]	=	8510
[a__U122(x₁)]	=	4257
[a__U21^#(x₁, x₂)]	=	x₂ + 8512
[a__isNatIList^#(x₁)]	=	x₁ + 8515
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₂ + 8516
[mark^#(x₁)]	=	24634
[0]	=	4255
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + 8517
[a__U21(x₁, x₂)]	=	4256
[a__U32(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U91(x₁, x₂, x₃)]	=	8506
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	4258
[isNatIListKind(x₁)]	=	1
[U114(x₁, x₂)]	=	0
[U62(x₁)]	=	8512
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8519
[U45(x₁, x₂)]	=	4263
[mark(x₁)]	=	4254
[U133(x₁,...,x₄)]	=	x₂ + x₃ + 8516
[a__U101^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8520
[a__U11(x₁, x₂)]	=	4256
[U32(x₁, x₂)]	=	x₁ + 17
[a__U42(x₁, x₂, x₃)]	=	x₂ + 8514
[a__U93(x₁, x₂, x₃)]	=	x₃ + 8508
[U33(x₁)]	=	8515
[a__U45^#(x₁, x₂)]	=	x₂ + 8515
[a__U52(x₁)]	=	8512
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₃ + x₄ + 8517
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	x₂ + 8516
[a__U12(x₁, x₂)]	=	x₂ + 4257
[a__isNatIListKind(x₁)]	=	8512
[a__U104^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 5
[isNat(x₁)]	=	x₁ + 4256
[U46(x₁)]	=	x₁ + 4256
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	8512
[U61(x₁, x₂)]	=	8512
[a__U46(x₁)]	=	4255
[a__U22^#(x₁, x₂)]	=	x₂ + 8512
[a__U113(x₁, x₂, x₃)]	=	x₃ + 8515
[U96(x₁)]	=	x₁ + 8512
[a__U13(x₁)]	=	4258
[U31(x₁, x₂)]	=	x₁ + 4257
[a__isNatList^#(x₁)]	=	x₁ + 8512
[a__U71(x₁)]	=	x₁ + 1
[U92(x₁, x₂, x₃)]	=	x₁ + x₂ + 8508
[U112(x₁, x₂, x₃)]	=	x₂ + 8515
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U92(x₁, x₂, x₃)]	=	x₃ + 8507
[a__U61(x₁, x₂)]	=	8512
[U102(x₁, x₂, x₃)]	=	x₁ + 8503
[a__U105(x₁, x₂)]	=	x₂ + 8510
[a__take(x₁, x₂)]	=	4255
[U81(x₁)]	=	8512
[a__U95^#(x₁, x₂)]	=	x₂ + 8512
[a__U41^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8515
[tt]	=	8512
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 1
[a__isNat(x₁)]	=	4255
[U13(x₁)]	=	4259
[a__U133(x₁,...,x₄)]	=	x₄ + 8515
[a__U23(x₁)]	=	8511
[a__U96(x₁)]	=	8511
[a__isNatKind(x₁)]	=	4270
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₂ + 4258
[U51(x₁, x₂)]	=	8512
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₃ + 17015
[length(x₁)]	=	x₁ + 0
[a__U112(x₁, x₂, x₃)]	=	x₂ + 8514
[U41(x₁, x₂, x₃)]	=	x₁ + 2
[a__U32^#(x₁, x₂)]	=	x₂ + 8513
[a__zeros]	=	4255
[a__U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 12771
[a__U91^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8512
[U121(x₁, x₂)]	=	x₁ + 12267
[a__length(x₁)]	=	x₁ + 8505
[U122(x₁)]	=	x₁ + 4258

together with the usable rules

a__U61(X1,X2)	→	U61(X1,X2)	(168)
a__isNatIListKind(zeros)	→	tt	(54)
a__U52(tt)	→	tt	(36)
a__U62(X)	→	U62(X)	(169)
a__U51(X1,X2)	→	U51(X1,X2)	(166)
a__isNatIListKind(X)	→	isNatIListKind(X)	(130)
a__isNatIListKind(take(V1,V2))	→	a__U61(a__isNatKind(V1),V2)	(56)
a__U52(X)	→	U52(X)	(167)
a__isNatIListKind(cons(V1,V2))	→	a__U51(a__isNatKind(V1),V2)	(55)
a__U62(tt)	→	tt	(38)
a__isNatIListKind(nil)	→	tt	(53)
a__U61(tt,V2)	→	a__U62(a__isNatIListKind(V2))	(37)
a__U51(tt,V2)	→	a__U52(a__isNatIListKind(V2))	(35)

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

a__U104^#(tt,V1,V2)	→	a__U105^#(a__isNat(V1),V2)	(363)
a__U31^#(tt,V)	→	a__U32^#(a__isNatIListKind(V),V)	(358)
a__U105^#(tt,V2)	→	a__isNatIList^#(V2)	(353)
a__U101^#(tt,V1,V2)	→	a__U102^#(a__isNatKind(V1),V1,V2)	(350)
a__U104^#(tt,V1,V2)	→	a__isNat^#(V1)	(234)
a__isNatList^#(take(V1,V2))	→	a__U101^#(a__isNatKind(V1),V1,V2)	(324)
a__isNatIList^#(V)	→	a__U31^#(a__isNatIListKind(V),V)	(227)
a__U103^#(tt,V1,V2)	→	a__U104^#(a__isNatIListKind(V2),V1,V2)	(321)
a__U32^#(tt,V)	→	a__isNatList^#(V)	(315)
a__U102^#(tt,V1,V2)	→	a__U103^#(a__isNatIListKind(V2),V1,V2)	(209)
a__U44^#(tt,V1,V2)	→	a__isNat^#(V1)	(195)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__U44^#(tt,V1,V2)	→	a__U45^#(a__isNat(V1),V2)	(298)
a__U45^#(tt,V2)	→	a__isNatIList^#(V2)	(319)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNatKind(V1),V1,V2)	(360)
a__U42^#(tt,V1,V2)	→	a__U43^#(a__isNatIListKind(V2),V1,V2)	(293)
a__U43^#(tt,V1,V2)	→	a__U44^#(a__isNatIListKind(V2),V1,V2)	(259)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNatKind(V1),V1,V2)	(223)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	x₁ + 0
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	55
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + 54
[a__U102(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4249
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 4261
[isNatList(x₁)]	=	44
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₂ + 54
[a__U92^#(x₁, x₂, x₃)]	=	8512
[a__U104(x₁, x₂, x₃)]	=	x₂ + 27
[U136(x₁,...,x₄)]	=	x₄ + 62
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 0
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + 29
[a__U31^#(x₁, x₂)]	=	8514
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 1
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	8512
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 6
[a__isNatIList(x₁)]	=	x₁ + 27
[a__U33(x₁)]	=	58
[U106(x₁)]	=	30
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₂ + 54
[U42(x₁, x₂, x₃)]	=	x₁ + 59
[U91(x₁, x₂, x₃)]	=	x₁ + x₃ + 51
[a__isNat^#(x₁)]	=	8512
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 4258
[U71(x₁)]	=	2
[a__U62(x₁)]	=	56
[a__U44(x₁, x₂, x₃)]	=	x₃ + 59
[U131(x₁,...,x₄)]	=	x₄ + 2
[isNatIList(x₁)]	=	28
[U135(x₁,...,x₄)]	=	x₂ + 61
[U101(x₁, x₂, x₃)]	=	x₂ + 4303
[a__U43^#(x₁, x₂, x₃)]	=	x₃ + 8513
[U95(x₁, x₂)]	=	55
[U111(x₁, x₂, x₃)]	=	2
[U132(x₁,...,x₄)]	=	x₁ + 2
[U43(x₁, x₂, x₃)]	=	x₂ + 3
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₂ + 28
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	x₃ + 8512
[U103(x₁, x₂, x₃)]	=	x₂ + 4307
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U103^#(x₁, x₂, x₃)]	=	8518
[U44(x₁, x₂, x₃)]	=	x₁ + 60
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 56
[a__U22(x₁, x₂)]	=	x₂ + 54
[U93(x₁, x₂, x₃)]	=	53
[a__U94(x₁, x₂, x₃)]	=	x₂ + x₃ + 53
[a__U106(x₁)]	=	29
[a__U11^#(x₁, x₂)]	=	8512
[U94(x₁, x₂, x₃)]	=	x₃ + 54
[zeros]	=	28
[a__U31(x₁, x₂)]	=	28
[a__U51(x₁, x₂)]	=	56
[a__U81(x₁)]	=	55
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + x₂ + 55
[a__isNatList(x₁)]	=	x₁ + 43
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 2
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₂ + 61
[a__U42^#(x₁, x₂, x₃)]	=	x₃ + 8514
[a__U41(x₁, x₂, x₃)]	=	x₁ + 1
[a__U134(x₁,...,x₄)]	=	x₂ + x₄ + 59
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	8512
[U104(x₁, x₂, x₃)]	=	28
[a__U122(x₁)]	=	29
[a__U21^#(x₁, x₂)]	=	8512
[a__isNatIList^#(x₁)]	=	x₁ + 8510
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₂ + 8537
[mark^#(x₁)]	=	24634
[0]	=	35
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + 60
[a__U21(x₁, x₂)]	=	53
[a__U32(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U91(x₁, x₂, x₃)]	=	50
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	30
[isNatIListKind(x₁)]	=	1
[U114(x₁, x₂)]	=	0
[U62(x₁)]	=	1
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	8519
[U45(x₁, x₂)]	=	4262
[mark(x₁)]	=	26
[U133(x₁,...,x₄)]	=	x₂ + x₃ + 59
[a__U101^#(x₁, x₂, x₃)]	=	8520
[a__U11(x₁, x₂)]	=	53
[U32(x₁, x₂)]	=	x₁ + 17
[a__U42(x₁, x₂, x₃)]	=	x₂ + 58
[a__U93(x₁, x₂, x₃)]	=	x₃ + 52
[U33(x₁)]	=	59
[a__U45^#(x₁, x₂)]	=	x₂ + 8511
[a__U52(x₁)]	=	56
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₃ + x₄ + 60
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	8516
[a__U12(x₁, x₂)]	=	x₂ + 54
[a__isNatIListKind(x₁)]	=	57
[a__U104^#(x₁, x₂, x₃)]	=	x₁ + 5
[isNat(x₁)]	=	x₁ + 53
[U46(x₁)]	=	x₁ + 28
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	1
[U61(x₁, x₂)]	=	1
[a__U46(x₁)]	=	27
[a__U22^#(x₁, x₂)]	=	8512
[a__U113(x₁, x₂, x₃)]	=	x₃ + 59
[U96(x₁)]	=	x₁ + 56
[a__U13(x₁)]	=	55
[U31(x₁, x₂)]	=	x₁ + 29
[a__isNatList^#(x₁)]	=	8512
[a__U71(x₁)]	=	x₁ + 1
[U92(x₁, x₂, x₃)]	=	x₁ + x₂ + 52
[U112(x₁, x₂, x₃)]	=	x₂ + 59
[cons(x₁, x₂)]	=	x₁ + x₂ + 6
[a__U92(x₁, x₂, x₃)]	=	x₃ + 51
[a__U61(x₁, x₂)]	=	57
[U102(x₁, x₂, x₃)]	=	x₁ + 4250
[a__U105(x₁, x₂)]	=	x₂ + 28
[a__take(x₁, x₂)]	=	27
[U81(x₁)]	=	56
[a__U95^#(x₁, x₂)]	=	8512
[a__U41^#(x₁, x₂, x₃)]	=	x₃ + 8515
[tt]	=	56
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 1
[a__isNat(x₁)]	=	52
[U13(x₁)]	=	56
[a__U133(x₁,...,x₄)]	=	x₄ + 58
[a__U23(x₁)]	=	55
[a__U96(x₁)]	=	55
[a__isNatKind(x₁)]	=	54
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₂ + 55
[U51(x₁, x₂)]	=	56
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₃ + 4306
[length(x₁)]	=	x₁ + 0
[a__U112(x₁, x₂, x₃)]	=	x₂ + 58
[U41(x₁, x₂, x₃)]	=	x₁ + 2
[a__U32^#(x₁, x₂)]	=	8513
[a__zeros]	=	27
[a__U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 4302
[a__U91^#(x₁, x₂, x₃)]	=	8512
[U121(x₁, x₂)]	=	x₁ + 12267
[a__length(x₁)]	=	x₁ + 37
[U122(x₁)]	=	x₁ + 30

together with the usable rules

a__U61(X1,X2)	→	U61(X1,X2)	(168)
a__isNatIListKind(zeros)	→	tt	(54)
a__U52(tt)	→	tt	(36)
a__U62(X)	→	U62(X)	(169)
a__U51(X1,X2)	→	U51(X1,X2)	(166)
a__isNatIListKind(X)	→	isNatIListKind(X)	(130)
a__isNatIListKind(take(V1,V2))	→	a__U61(a__isNatKind(V1),V2)	(56)
a__U52(X)	→	U52(X)	(167)
a__isNatIListKind(cons(V1,V2))	→	a__U51(a__isNatKind(V1),V2)	(55)
a__U62(tt)	→	tt	(38)
a__isNatIListKind(nil)	→	tt	(53)
a__U61(tt,V2)	→	a__U62(a__isNatIListKind(V2))	(37)
a__U51(tt,V2)	→	a__U52(a__isNatIListKind(V2))	(35)

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

a__U44^#(tt,V1,V2)	→	a__U45^#(a__isNat(V1),V2)	(298)
a__U45^#(tt,V2)	→	a__isNatIList^#(V2)	(319)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNatKind(V1),V1,V2)	(360)
a__U42^#(tt,V1,V2)	→	a__U43^#(a__isNatIListKind(V2),V1,V2)	(293)
a__U43^#(tt,V1,V2)	→	a__U44^#(a__isNatIListKind(V2),V1,V2)	(259)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNatKind(V1),V1,V2)	(223)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__U11^#(tt,V1)	→	a__U12^#(a__isNatIListKind(V1),V1)	(340)
a__U94^#(tt,V1,V2)	→	a__isNat^#(V1)	(304)
a__U94^#(tt,V1,V2)	→	a__U95^#(a__isNat(V1),V2)	(204)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(207)
a__U95^#(tt,V2)	→	a__isNatList^#(V2)	(291)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(183)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(253)
a__U12^#(tt,V1)	→	a__isNatList^#(V1)	(231)
a__isNatList^#(cons(V1,V2))	→	a__U91^#(a__isNatKind(V1),V1,V2)	(275)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(192)
a__U91^#(tt,V1,V2)	→	a__U92^#(a__isNatKind(V1),V1,V2)	(345)
a__U92^#(tt,V1,V2)	→	a__U93^#(a__isNatIListKind(V2),V1,V2)	(269)
a__U93^#(tt,V1,V2)	→	a__U94^#(a__isNatIListKind(V2),V1,V2)	(367)

1.1.2.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 8457
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	55
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + 48
[a__U102(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 34
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 4261
[isNatList(x₁)]	=	44
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₂ + 54
[a__U92^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8515
[a__U104(x₁, x₂, x₃)]	=	x₂ + 27
[U136(x₁,...,x₄)]	=	x₄ + 75
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 0
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + 29
[a__U31^#(x₁, x₂)]	=	8514
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 2
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8514
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 6
[a__isNatIList(x₁)]	=	x₁ + 27
[a__U33(x₁)]	=	58
[U106(x₁)]	=	30
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₂ + 54
[U42(x₁, x₂, x₃)]	=	x₁ + 59
[U91(x₁, x₂, x₃)]	=	x₁ + x₃ + 51
[a__isNat^#(x₁)]	=	x₁ + 8512
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 43
[U71(x₁)]	=	2
[a__U62(x₁)]	=	56
[a__U44(x₁, x₂, x₃)]	=	x₃ + 60
[U131(x₁,...,x₄)]	=	x₄ + 2
[isNatIList(x₁)]	=	28
[U135(x₁,...,x₄)]	=	x₂ + 74
[U101(x₁, x₂, x₃)]	=	x₂ + 88
[a__U43^#(x₁, x₂, x₃)]	=	8513
[U95(x₁, x₂)]	=	55
[U111(x₁, x₂, x₃)]	=	2
[U132(x₁,...,x₄)]	=	x₁ + 3
[U43(x₁, x₂, x₃)]	=	x₂ + 4
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₂ + 28
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	8512
[U103(x₁, x₂, x₃)]	=	x₂ + 92
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U103^#(x₁, x₂, x₃)]	=	8518
[U44(x₁, x₂, x₃)]	=	x₁ + 61
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 50
[a__U22(x₁, x₂)]	=	x₂ + 48
[U93(x₁, x₂, x₃)]	=	53
[a__U94(x₁, x₂, x₃)]	=	x₂ + x₃ + 53
[a__U106(x₁)]	=	29
[a__U11^#(x₁, x₂)]	=	x₂ + 8513
[U94(x₁, x₂, x₃)]	=	x₃ + 54
[zeros]	=	28
[a__U31(x₁, x₂)]	=	28
[a__U51(x₁, x₂)]	=	56
[a__U81(x₁)]	=	55
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + x₂ + 55
[a__isNatList(x₁)]	=	x₁ + 43
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 3
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₂ + 74
[a__U42^#(x₁, x₂, x₃)]	=	8514
[a__U41(x₁, x₂, x₃)]	=	x₁ + 1
[a__U134(x₁,...,x₄)]	=	x₂ + x₄ + 72
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	x₂ + 8512
[U104(x₁, x₂, x₃)]	=	28
[a__U122(x₁)]	=	29
[a__U21^#(x₁, x₂)]	=	x₂ + 8512
[a__isNatIList^#(x₁)]	=	8510
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₂ + 8537
[mark^#(x₁)]	=	24634
[0]	=	31
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + 73
[a__U21(x₁, x₂)]	=	47
[a__U32(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U91(x₁, x₂, x₃)]	=	50
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	30
[isNatIListKind(x₁)]	=	1
[U114(x₁, x₂)]	=	0
[U62(x₁)]	=	1
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	8519
[U45(x₁, x₂)]	=	4262
[mark(x₁)]	=	26
[U133(x₁,...,x₄)]	=	x₂ + x₃ + 60
[a__U101^#(x₁, x₂, x₃)]	=	8520
[a__U11(x₁, x₂)]	=	53
[U32(x₁, x₂)]	=	x₁ + 17
[a__U42(x₁, x₂, x₃)]	=	x₂ + 58
[a__U93(x₁, x₂, x₃)]	=	x₃ + 52
[U33(x₁)]	=	59
[a__U45^#(x₁, x₂)]	=	8511
[a__U52(x₁)]	=	56
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₃ + x₄ + 73
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	8516
[a__U12(x₁, x₂)]	=	x₂ + 54
[a__isNatIListKind(x₁)]	=	56
[a__U104^#(x₁, x₂, x₃)]	=	x₁ + 5
[isNat(x₁)]	=	x₁ + 47
[U46(x₁)]	=	x₁ + 56
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	1
[U61(x₁, x₂)]	=	56
[a__U46(x₁)]	=	55
[a__U22^#(x₁, x₂)]	=	x₂ + 8512
[a__U113(x₁, x₂, x₃)]	=	x₃ + 59
[U96(x₁)]	=	x₁ + 56
[a__U13(x₁)]	=	55
[U31(x₁, x₂)]	=	x₁ + 29
[a__isNatList^#(x₁)]	=	x₁ + 8511
[a__U71(x₁)]	=	x₁ + 1
[U92(x₁, x₂, x₃)]	=	x₁ + x₂ + 52
[U112(x₁, x₂, x₃)]	=	x₂ + 59
[cons(x₁, x₂)]	=	x₁ + x₂ + 6
[a__U92(x₁, x₂, x₃)]	=	x₃ + 51
[a__U61(x₁, x₂)]	=	56
[U102(x₁, x₂, x₃)]	=	x₁ + 4250
[a__U105(x₁, x₂)]	=	x₂ + 28
[a__take(x₁, x₂)]	=	27
[U81(x₁)]	=	56
[a__U95^#(x₁, x₂)]	=	x₂ + 8512
[a__U41^#(x₁, x₂, x₃)]	=	8515
[tt]	=	56
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 1
[a__isNat(x₁)]	=	46
[U13(x₁)]	=	56
[a__U133(x₁,...,x₄)]	=	x₄ + 59
[a__U23(x₁)]	=	49
[a__U96(x₁)]	=	55
[a__isNatKind(x₁)]	=	54
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₂ + 49
[U51(x₁, x₂)]	=	1
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₃ + 91
[length(x₁)]	=	x₁ + 2
[a__U112(x₁, x₂, x₃)]	=	x₂ + 58
[U41(x₁, x₂, x₃)]	=	x₁ + 2
[a__U32^#(x₁, x₂)]	=	8513
[a__zeros]	=	27
[a__U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 87
[a__U91^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 8516
[U121(x₁, x₂)]	=	x₁ + 12267
[a__length(x₁)]	=	x₁ + 37
[U122(x₁)]	=	x₁ + 30

together with the usable rules

a__U61(X1,X2)	→	U61(X1,X2)	(168)
a__isNatIListKind(zeros)	→	tt	(54)
a__U52(tt)	→	tt	(36)
a__U62(X)	→	U62(X)	(169)
a__U51(X1,X2)	→	U51(X1,X2)	(166)
a__isNatIListKind(X)	→	isNatIListKind(X)	(130)
a__isNatIListKind(take(V1,V2))	→	a__U61(a__isNatKind(V1),V2)	(56)
a__U52(X)	→	U52(X)	(167)
a__isNatIListKind(cons(V1,V2))	→	a__U51(a__isNatKind(V1),V2)	(55)
a__U62(tt)	→	tt	(38)
a__isNatIListKind(nil)	→	tt	(53)
a__U61(tt,V2)	→	a__U62(a__isNatIListKind(V2))	(37)
a__U51(tt,V2)	→	a__U52(a__isNatIListKind(V2))	(35)

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

a__U11^#(tt,V1)	→	a__U12^#(a__isNatIListKind(V1),V1)	(340)
a__U94^#(tt,V1,V2)	→	a__isNat^#(V1)	(304)
a__U94^#(tt,V1,V2)	→	a__U95^#(a__isNat(V1),V2)	(204)
a__U95^#(tt,V2)	→	a__isNatList^#(V2)	(291)
a__U12^#(tt,V1)	→	a__isNatList^#(V1)	(231)
a__isNatList^#(cons(V1,V2))	→	a__U91^#(a__isNatKind(V1),V1,V2)	(275)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(192)
a__U91^#(tt,V1,V2)	→	a__U92^#(a__isNatKind(V1),V1,V2)	(345)
a__U92^#(tt,V1,V2)	→	a__U93^#(a__isNatIListKind(V2),V1,V2)	(269)
a__U93^#(tt,V1,V2)	→	a__U94^#(a__isNatIListKind(V2),V1,V2)	(367)

could be deleted.

1.1.2.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(207)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(183)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(253)

1.1.2.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	x₁ + 8457
[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	x₁ + 7
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + x₂ + 6
[a__U102(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 187
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 4261
[isNatList(x₁)]	=	x₁ + 1
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₁ + x₂ + 6
[a__U92^#(x₁, x₂, x₃)]	=	8515
[a__U104(x₁, x₂, x₃)]	=	x₂ + 0
[U136(x₁,...,x₄)]	=	x₃ + x₄ + 4
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 3
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U31^#(x₁, x₂)]	=	8514
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 0
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	8514
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 53853
[a__isNatIList(x₁)]	=	x₁ + 4
[a__U33(x₁)]	=	58
[U106(x₁)]	=	8
[a__isNatIListKind^#(x₁)]	=	0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₂ + 6
[U42(x₁, x₂, x₃)]	=	x₁ + x₂ + 10
[U91(x₁, x₂, x₃)]	=	x₁ + x₃ + 21
[a__isNat^#(x₁)]	=	x₁ + 8510
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 24
[U71(x₁)]	=	17985
[a__U62(x₁)]	=	8
[a__U44(x₁, x₂, x₃)]	=	x₃ + 9
[U131(x₁,...,x₄)]	=	x₂ + 26
[isNatIList(x₁)]	=	1
[U135(x₁,...,x₄)]	=	x₂ + x₄ + 12
[U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 193
[a__U43^#(x₁, x₂, x₃)]	=	8513
[U95(x₁, x₂)]	=	x₁ + 7
[U111(x₁, x₂, x₃)]	=	x₃ + 53840
[U132(x₁,...,x₄)]	=	x₁ + x₂ + 63
[U43(x₁, x₂, x₃)]	=	x₂ + 20424
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₂ + 93
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	8512
[U103(x₁, x₂, x₃)]	=	x₂ + 201
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 53841
[a__U103^#(x₁, x₂, x₃)]	=	8518
[U44(x₁, x₂, x₃)]	=	x₁ + x₃ + 6
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U23(x₁)]	=	x₁ + 8
[a__U22(x₁, x₂)]	=	x₂ + 6
[U93(x₁, x₂, x₃)]	=	10258
[a__U94(x₁, x₂, x₃)]	=	x₂ + x₃ + 5
[a__U106(x₁)]	=	7
[a__U11^#(x₁, x₂)]	=	8513
[U94(x₁, x₂, x₃)]	=	x₁ + x₃ + 1
[zeros]	=	3
[a__U31(x₁, x₂)]	=	5
[a__U51(x₁, x₂)]	=	8
[a__U81(x₁)]	=	7
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + x₂ + 51
[a__isNatList(x₁)]	=	x₁ + 18
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₂ + 12
[a__U42^#(x₁, x₂, x₃)]	=	8514
[a__U41(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[a__U134(x₁,...,x₄)]	=	x₂ + x₄ + 10
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	8512
[U104(x₁, x₂, x₃)]	=	x₂ + 22549
[a__U122(x₁)]	=	94
[a__U21^#(x₁, x₂)]	=	x₂ + 8512
[a__isNatIList^#(x₁)]	=	8510
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[U113(x₁, x₂, x₃)]	=	x₂ + 28216
[mark^#(x₁)]	=	24634
[0]	=	4
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + x₄ + 11
[a__U21(x₁, x₂)]	=	5
[a__U32(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U91(x₁, x₂, x₃)]	=	20
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	95
[isNatIListKind(x₁)]	=	10
[U114(x₁, x₂)]	=	10780
[U62(x₁)]	=	5
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	8519
[U45(x₁, x₂)]	=	4262
[mark(x₁)]	=	x₁ + 2
[U133(x₁,...,x₄)]	=	x₂ + x₃ + x₄ + 10
[a__U101^#(x₁, x₂, x₃)]	=	8520
[a__U11(x₁, x₂)]	=	5
[U32(x₁, x₂)]	=	24132
[a__U42(x₁, x₂, x₃)]	=	x₂ + 9
[a__U93(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U33(x₁)]	=	59
[a__U45^#(x₁, x₂)]	=	8511
[a__U52(x₁)]	=	8
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₃ + x₄ + 11
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	8516
[a__U12(x₁, x₂)]	=	x₂ + 6
[a__isNatIListKind(x₁)]	=	34
[a__U104^#(x₁, x₂, x₃)]	=	x₁ + 5
[isNat(x₁)]	=	x₁ + 2
[U46(x₁)]	=	x₁ + 9259
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	4
[U61(x₁, x₂)]	=	8
[a__U46(x₁)]	=	0
[a__U22^#(x₁, x₂)]	=	x₂ + 8511
[a__U113(x₁, x₂, x₃)]	=	x₁ + x₃ + 53850
[U96(x₁)]	=	x₁ + 8
[a__U13(x₁)]	=	7
[U31(x₁, x₂)]	=	x₁ + 6
[a__isNatList^#(x₁)]	=	8511
[a__U71(x₁)]	=	x₁ + 0
[U92(x₁, x₂, x₃)]	=	x₂ + 16
[U112(x₁, x₂, x₃)]	=	x₂ + 53851
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U92(x₁, x₂, x₃)]	=	x₁ + x₃ + 15
[a__U61(x₁, x₂)]	=	34
[U102(x₁, x₂, x₃)]	=	x₁ + 188
[a__U105(x₁, x₂)]	=	x₂ + 1
[a__take(x₁, x₂)]	=	x₁ + 25
[U81(x₁)]	=	8
[a__U95^#(x₁, x₂)]	=	8512
[a__U41^#(x₁, x₂, x₃)]	=	8515
[tt]	=	8
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 25
[a__isNat(x₁)]	=	x₁ + 1
[U13(x₁)]	=	52
[a__U133(x₁,...,x₄)]	=	x₄ + 9
[a__U23(x₁)]	=	7
[a__U96(x₁)]	=	7
[a__isNatKind(x₁)]	=	6
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₂ + 7
[U51(x₁, x₂)]	=	2
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₃ + 196
[length(x₁)]	=	x₁ + 3
[a__U112(x₁, x₂, x₃)]	=	x₂ + 53850
[U41(x₁, x₂, x₃)]	=	x₂ + 26863
[a__U32^#(x₁, x₂)]	=	8513
[a__zeros]	=	7
[a__U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 192
[a__U91^#(x₁, x₂, x₃)]	=	8516
[U121(x₁, x₂)]	=	x₁ + 94
[a__length(x₁)]	=	x₁ + 53857
[U122(x₁)]	=	x₁ + 20

together with the usable rules

a__U61(X1,X2)	→	U61(X1,X2)	(168)
a__isNatIListKind(zeros)	→	tt	(54)
a__U52(tt)	→	tt	(36)
a__U62(X)	→	U62(X)	(169)
a__U51(X1,X2)	→	U51(X1,X2)	(166)
a__isNatIListKind(X)	→	isNatIListKind(X)	(130)
a__isNatIListKind(take(V1,V2))	→	a__U61(a__isNatKind(V1),V2)	(56)
a__U52(X)	→	U52(X)	(167)
a__isNatIListKind(cons(V1,V2))	→	a__U51(a__isNatKind(V1),V2)	(55)
a__U62(tt)	→	tt	(38)
a__isNatIListKind(nil)	→	tt	(53)
a__U61(tt,V2)	→	a__U62(a__isNatIListKind(V2))	(37)
a__U51(tt,V2)	→	a__U52(a__isNatIListKind(V2))	(35)

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

a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(207)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(183)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(253)

could be deleted.

1.1.2.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

a__isNatIListKind^#(take(V1,V2))	→	a__isNatKind^#(V1)	(270)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(264)
a__U61^#(tt,V2)	→	a__isNatIListKind^#(V2)	(248)
a__isNatIListKind^#(take(V1,V2))	→	a__U61^#(a__isNatKind(V1),V2)	(336)
a__U51^#(tt,V2)	→	a__isNatIListKind^#(V2)	(238)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(323)
a__isNatIListKind^#(cons(V1,V2))	→	a__U51^#(a__isNatKind(V1),V2)	(226)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(186)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__U94^#(x₁, x₂, x₃)]	=	x₁ + 8457
[a__isNatKind^#(x₁)]	=	x₁ + 0
[isNatKind(x₁)]	=	x₁ + 9
[a__U131^#(x₁,...,x₄)]	=	56408
[U21(x₁, x₂)]	=	x₁ + x₂ + 10
[a__U102(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 40
[a__U45(x₁, x₂)]	=	x₁ + x₂ + 4261
[isNatList(x₁)]	=	x₁ + 22
[a__U71^#(x₁)]	=	0
[U11(x₁, x₂)]	=	x₁ + x₂ + 4
[a__U92^#(x₁, x₂, x₃)]	=	8515
[a__U104(x₁, x₂, x₃)]	=	x₂ + 0
[U136(x₁,...,x₄)]	=	x₃ + x₄ + 1
[a__U112^#(x₁, x₂, x₃)]	=	2
[s(x₁)]	=	x₁ + 2
[a__U133^#(x₁,...,x₄)]	=	56408
[U105(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U31^#(x₁, x₂)]	=	8514
[a__U132(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 0
[a__U33^#(x₁)]	=	0
[a__U93^#(x₁, x₂, x₃)]	=	8514
[a__U114(x₁, x₂)]	=	x₁ + x₂ + 27055
[a__isNatIList(x₁)]	=	x₁ + 8
[a__U33(x₁)]	=	58
[U106(x₁)]	=	3
[a__isNatIListKind^#(x₁)]	=	x₁ + 0
[a__U23^#(x₁)]	=	0
[a__U95(x₁, x₂)]	=	x₂ + 5
[U42(x₁, x₂, x₃)]	=	x₁ + x₂ + 16
[U91(x₁, x₂, x₃)]	=	x₁ + x₃ + 30
[a__isNat^#(x₁)]	=	8510
[a__U106^#(x₁)]	=	0
[a__U136^#(x₁,...,x₄)]	=	24635
[take(x₁, x₂)]	=	x₁ + x₂ + 21
[U71(x₁)]	=	6710
[a__U62(x₁)]	=	10
[a__U44(x₁, x₂, x₃)]	=	x₃ + 472
[U131(x₁,...,x₄)]	=	x₂ + 18
[isNatIList(x₁)]	=	3
[U135(x₁,...,x₄)]	=	x₂ + x₄ + 15
[U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 48
[a__U43^#(x₁, x₂, x₃)]	=	8513
[U95(x₁, x₂)]	=	x₁ + 28720
[U111(x₁, x₂, x₃)]	=	x₃ + 27040
[U132(x₁,...,x₄)]	=	x₁ + x₂ + 63
[U43(x₁, x₂, x₃)]	=	x₂ + 20424
[a__U13^#(x₁)]	=	0
[a__U121(x₁, x₂)]	=	x₂ + 25
[a__U135^#(x₁,...,x₄)]	=	24636
[a__U44^#(x₁, x₂, x₃)]	=	8512
[U103(x₁, x₂, x₃)]	=	x₂ + 52
[a__U111(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 27041
[a__U103^#(x₁, x₂, x₃)]	=	8518
[U44(x₁, x₂, x₃)]	=	x₁ + x₃ + 469
[a__U46^#(x₁)]	=	0
[a__U114^#(x₁, x₂)]	=	1
[a__U51^#(x₁, x₂)]	=	x₂ + 2
[U23(x₁)]	=	x₁ + 9721
[a__U22(x₁, x₂)]	=	x₂ + 8
[U93(x₁, x₂, x₃)]	=	10258
[a__U94(x₁, x₂, x₃)]	=	x₂ + x₃ + 4
[a__U106(x₁)]	=	2
[a__U11^#(x₁, x₂)]	=	8513
[U94(x₁, x₂, x₃)]	=	x₁ + x₃ + 1
[zeros]	=	1
[a__U31(x₁, x₂)]	=	9
[a__U51(x₁, x₂)]	=	10
[a__U81(x₁)]	=	9
[a__take^#(x₁, x₂)]	=	81043
[U12(x₁, x₂)]	=	x₁ + x₂ + 49
[a__isNatList(x₁)]	=	x₁ + 25
[a__U43(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[a__U62^#(x₁)]	=	0
[a__U136(x₁,...,x₄)]	=	x₂ + 25
[a__U42^#(x₁, x₂, x₃)]	=	8514
[a__U41(x₁, x₂, x₃)]	=	x₁ + x₂ + 4
[a__U134(x₁,...,x₄)]	=	x₂ + x₄ + 14
[a__U122^#(x₁)]	=	0
[a__U12^#(x₁, x₂)]	=	8512
[U104(x₁, x₂, x₃)]	=	x₂ + 27772
[a__U122(x₁)]	=	94
[a__U21^#(x₁, x₂)]	=	8512
[a__isNatIList^#(x₁)]	=	8510
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	x₂ + 1
[U113(x₁, x₂, x₃)]	=	x₂ + 7109
[mark^#(x₁)]	=	24634
[0]	=	2
[a__zeros^#]	=	0
[a__U113^#(x₁, x₂, x₃)]	=	1
[U134(x₁,...,x₄)]	=	x₁ + x₄ + 15
[a__U21(x₁, x₂)]	=	7
[a__U32(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U91(x₁, x₂, x₃)]	=	29
[a__U111^#(x₁, x₂, x₃)]	=	0
[nil]	=	95
[isNatIListKind(x₁)]	=	10
[U114(x₁, x₂)]	=	3044
[U62(x₁)]	=	5
[a__U52^#(x₁)]	=	0
[a__U102^#(x₁, x₂, x₃)]	=	8519
[U45(x₁, x₂)]	=	4262
[mark(x₁)]	=	x₁ + 2
[U133(x₁,...,x₄)]	=	x₂ + x₃ + x₄ + 12
[a__U101^#(x₁, x₂, x₃)]	=	8520
[a__U11(x₁, x₂)]	=	3
[U32(x₁, x₂)]	=	24132
[a__U42(x₁, x₂, x₃)]	=	x₂ + 15
[a__U93(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U33(x₁)]	=	59
[a__U45^#(x₁, x₂)]	=	8511
[a__U52(x₁)]	=	10
[a__U96^#(x₁)]	=	0
[a__U135(x₁,...,x₄)]	=	x₁ + x₃ + x₄ + 14
[a__length^#(x₁)]	=	1
[a__U105^#(x₁, x₂)]	=	8516
[a__U12(x₁, x₂)]	=	x₂ + 4
[a__isNatIListKind(x₁)]	=	34
[a__U104^#(x₁, x₂, x₃)]	=	x₁ + 5
[isNat(x₁)]	=	x₁ + 22560
[U46(x₁)]	=	x₁ + 1
[a__U121^#(x₁, x₂)]	=	0
[U52(x₁)]	=	5
[U61(x₁, x₂)]	=	1
[a__U46(x₁)]	=	0
[a__U22^#(x₁, x₂)]	=	8511
[a__U113(x₁, x₂, x₃)]	=	x₁ + x₃ + 27052
[U96(x₁)]	=	x₁ + 31698
[a__U13(x₁)]	=	5
[U31(x₁, x₂)]	=	x₁ + 10
[a__isNatList^#(x₁)]	=	8511
[a__U71(x₁)]	=	x₁ + 0
[U92(x₁, x₂, x₃)]	=	x₂ + 23
[U112(x₁, x₂, x₃)]	=	x₂ + 27053
[cons(x₁, x₂)]	=	x₁ + x₂ + 3
[a__U92(x₁, x₂, x₃)]	=	x₁ + x₃ + 22
[a__U61(x₁, x₂)]	=	34
[U102(x₁, x₂, x₃)]	=	x₁ + 41
[a__U105(x₁, x₂)]	=	x₂ + 1
[a__take(x₁, x₂)]	=	x₁ + 22
[U81(x₁)]	=	20449
[a__U95^#(x₁, x₂)]	=	8512
[a__U41^#(x₁, x₂, x₃)]	=	8515
[tt]	=	10
[a__U131(x₁,...,x₄)]	=	x₁ + x₂ + x₄ + 17
[a__isNat(x₁)]	=	x₁ + 1
[U13(x₁)]	=	50
[a__U133(x₁,...,x₄)]	=	x₄ + 11
[a__U23(x₁)]	=	9
[a__U96(x₁)]	=	6
[a__isNatKind(x₁)]	=	8
[a__U134^#(x₁,...,x₄)]	=	56407
[U22(x₁, x₂)]	=	x₂ + 9
[U51(x₁, x₂)]	=	2
[a__U132^#(x₁,...,x₄)]	=	56409
[a__U103(x₁, x₂, x₃)]	=	x₃ + 51
[length(x₁)]	=	x₁ + 1
[a__U112(x₁, x₂, x₃)]	=	x₂ + 27052
[U41(x₁, x₂, x₃)]	=	x₂ + 26867
[a__U32^#(x₁, x₂)]	=	8513
[a__zeros]	=	4
[a__U101(x₁, x₂, x₃)]	=	x₂ + x₃ + 47
[a__U91^#(x₁, x₂, x₃)]	=	8516
[U121(x₁, x₂)]	=	x₁ + 26
[a__length(x₁)]	=	x₁ + 27062
[U122(x₁)]	=	x₁ + 20

together with the usable rules

a__U61(X1,X2)	→	U61(X1,X2)	(168)
a__isNatIListKind(zeros)	→	tt	(54)
a__U52(tt)	→	tt	(36)
a__U62(X)	→	U62(X)	(169)
a__U51(X1,X2)	→	U51(X1,X2)	(166)
a__isNatIListKind(X)	→	isNatIListKind(X)	(130)
a__isNatIListKind(take(V1,V2))	→	a__U61(a__isNatKind(V1),V2)	(56)
a__U52(X)	→	U52(X)	(167)
a__isNatIListKind(cons(V1,V2))	→	a__U51(a__isNatKind(V1),V2)	(55)
a__U62(tt)	→	tt	(38)
a__isNatIListKind(nil)	→	tt	(53)
a__U61(tt,V2)	→	a__U62(a__isNatIListKind(V2))	(37)
a__U51(tt,V2)	→	a__U52(a__isNatIListKind(V2))	(35)

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

a__isNatIListKind^#(take(V1,V2))	→	a__isNatKind^#(V1)	(270)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(264)
a__U61^#(tt,V2)	→	a__isNatIListKind^#(V2)	(248)
a__isNatIListKind^#(take(V1,V2))	→	a__U61^#(a__isNatKind(V1),V2)	(336)
a__U51^#(tt,V2)	→	a__isNatIListKind^#(V2)	(238)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(323)
a__isNatIListKind^#(cons(V1,V2))	→	a__U51^#(a__isNatKind(V1),V2)	(226)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(186)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.