Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/OvConsOS_nokinds_noand_GM)

The rewrite relation of the following TRS is considered.

a__zeros	→	cons(0,zeros)	(1)
a__U11(tt)	→	tt	(2)
a__U21(tt)	→	tt	(3)
a__U31(tt)	→	tt	(4)
a__U41(tt,V2)	→	a__U42(a__isNatIList(V2))	(5)
a__U42(tt)	→	tt	(6)
a__U51(tt,V2)	→	a__U52(a__isNatList(V2))	(7)
a__U52(tt)	→	tt	(8)
a__U61(tt,V2)	→	a__U62(a__isNatIList(V2))	(9)
a__U62(tt)	→	tt	(10)
a__U71(tt,L,N)	→	a__U72(a__isNat(N),L)	(11)
a__U72(tt,L)	→	s(a__length(mark(L)))	(12)
a__U81(tt)	→	nil	(13)
a__U91(tt,IL,M,N)	→	a__U92(a__isNat(M),IL,M,N)	(14)
a__U92(tt,IL,M,N)	→	a__U93(a__isNat(N),IL,M,N)	(15)
a__U93(tt,IL,M,N)	→	cons(mark(N),take(M,IL))	(16)
a__isNat(0)	→	tt	(17)
a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(18)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(19)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(20)
a__isNatIList(zeros)	→	tt	(21)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(22)
a__isNatList(nil)	→	tt	(23)
a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(24)
a__isNatList(take(V1,V2))	→	a__U61(a__isNat(V1),V2)	(25)
a__length(nil)	→	0	(26)
a__length(cons(N,L))	→	a__U71(a__isNatList(L),L,N)	(27)
a__take(0,IL)	→	a__U81(a__isNatIList(IL))	(28)
a__take(s(M),cons(N,IL))	→	a__U91(a__isNatIList(IL),IL,M,N)	(29)
mark(zeros)	→	a__zeros	(30)
mark(U11(X))	→	a__U11(mark(X))	(31)
mark(U21(X))	→	a__U21(mark(X))	(32)
mark(U31(X))	→	a__U31(mark(X))	(33)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(34)
mark(U42(X))	→	a__U42(mark(X))	(35)
mark(isNatIList(X))	→	a__isNatIList(X)	(36)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(37)
mark(U52(X))	→	a__U52(mark(X))	(38)
mark(isNatList(X))	→	a__isNatList(X)	(39)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(40)
mark(U62(X))	→	a__U62(mark(X))	(41)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(42)
mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(43)
mark(isNat(X))	→	a__isNat(X)	(44)
mark(length(X))	→	a__length(mark(X))	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(U91(X1,X2,X3,X4))	→	a__U91(mark(X1),X2,X3,X4)	(47)
mark(U92(X1,X2,X3,X4))	→	a__U92(mark(X1),X2,X3,X4)	(48)
mark(U93(X1,X2,X3,X4))	→	a__U93(mark(X1),X2,X3,X4)	(49)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(50)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(51)
mark(0)	→	0	(52)
mark(tt)	→	tt	(53)
mark(s(X))	→	s(mark(X))	(54)
mark(nil)	→	nil	(55)
a__zeros	→	zeros	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X)	→	U21(X)	(58)
a__U31(X)	→	U31(X)	(59)
a__U41(X1,X2)	→	U41(X1,X2)	(60)
a__U42(X)	→	U42(X)	(61)
a__isNatIList(X)	→	isNatIList(X)	(62)
a__U51(X1,X2)	→	U51(X1,X2)	(63)
a__U52(X)	→	U52(X)	(64)
a__isNatList(X)	→	isNatList(X)	(65)
a__U61(X1,X2)	→	U61(X1,X2)	(66)
a__U62(X)	→	U62(X)	(67)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(68)
a__U72(X1,X2)	→	U72(X1,X2)	(69)
a__isNat(X)	→	isNat(X)	(70)
a__length(X)	→	length(X)	(71)
a__U81(X)	→	U81(X)	(72)
a__U91(X1,X2,X3,X4)	→	U91(X1,X2,X3,X4)	(73)
a__U92(X1,X2,X3,X4)	→	U92(X1,X2,X3,X4)	(74)
a__U93(X1,X2,X3,X4)	→	U93(X1,X2,X3,X4)	(75)
a__take(X1,X2)	→	take(X1,X2)	(76)

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.

mark^#(U72(X1,X2))	→	mark^#(X1)	(77)
a__isNatIList^#(V)	→	a__U31^#(a__isNatList(V))	(78)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(79)
mark^#(U11(X))	→	mark^#(X)	(80)
a__U93^#(tt,IL,M,N)	→	mark^#(N)	(81)
a__U51^#(tt,V2)	→	a__isNatList^#(V2)	(82)
a__isNatList^#(take(V1,V2))	→	a__isNat^#(V1)	(83)
a__isNatList^#(take(V1,V2))	→	a__U61^#(a__isNat(V1),V2)	(84)
a__U91^#(tt,IL,M,N)	→	a__isNat^#(M)	(85)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatList(V1))	(86)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(87)
a__take^#(0,IL)	→	a__U81^#(a__isNatIList(IL))	(88)
mark^#(take(X1,X2))	→	mark^#(X1)	(89)
mark^#(U31(X))	→	a__U31^#(mark(X))	(90)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(91)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(U21(X))	→	a__U21^#(mark(X))	(93)
mark^#(zeros)	→	a__zeros^#	(94)
mark^#(U42(X))	→	mark^#(X)	(95)
a__length^#(cons(N,L))	→	a__U71^#(a__isNatList(L),L,N)	(96)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(97)
mark^#(s(X))	→	mark^#(X)	(98)
mark^#(U93(X1,X2,X3,X4))	→	mark^#(X1)	(99)
a__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(100)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(101)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(102)
mark^#(U62(X))	→	a__U62^#(mark(X))	(103)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(104)
a__U61^#(tt,V2)	→	a__U62^#(a__isNatIList(V2))	(105)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(106)
mark^#(cons(X1,X2))	→	mark^#(X1)	(107)
a__U51^#(tt,V2)	→	a__U52^#(a__isNatList(V2))	(108)
a__U92^#(tt,IL,M,N)	→	a__isNat^#(N)	(109)
mark^#(U62(X))	→	mark^#(X)	(110)
mark^#(length(X))	→	mark^#(X)	(111)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(112)
mark^#(U51(X1,X2))	→	mark^#(X1)	(113)
mark^#(U21(X))	→	mark^#(X)	(114)
mark^#(length(X))	→	a__length^#(mark(X))	(115)
mark^#(isNat(X))	→	a__isNat^#(X)	(116)
mark^#(U31(X))	→	mark^#(X)	(117)
a__U61^#(tt,V2)	→	a__isNatIList^#(V2)	(118)
mark^#(U52(X))	→	mark^#(X)	(119)
mark^#(U81(X))	→	a__U81^#(mark(X))	(120)
mark^#(U93(X1,X2,X3,X4))	→	a__U93^#(mark(X1),X2,X3,X4)	(121)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(122)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(123)
a__U72^#(tt,L)	→	mark^#(L)	(124)
mark^#(take(X1,X2))	→	mark^#(X2)	(125)
mark^#(U42(X))	→	a__U42^#(mark(X))	(126)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(127)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(128)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(129)
mark^#(U61(X1,X2))	→	mark^#(X1)	(130)
mark^#(U11(X))	→	a__U11^#(mark(X))	(131)
a__U71^#(tt,L,N)	→	a__isNat^#(N)	(132)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(133)
mark^#(U92(X1,X2,X3,X4))	→	a__U92^#(mark(X1),X2,X3,X4)	(134)
a__U72^#(tt,L)	→	a__length^#(mark(L))	(135)
mark^#(U52(X))	→	a__U52^#(mark(X))	(136)
a__isNat^#(s(V1))	→	a__U21^#(a__isNat(V1))	(137)
a__U71^#(tt,L,N)	→	a__U72^#(a__isNat(N),L)	(138)
a__U92^#(tt,IL,M,N)	→	a__U93^#(a__isNat(N),IL,M,N)	(139)
a__U91^#(tt,IL,M,N)	→	a__U92^#(a__isNat(M),IL,M,N)	(140)
mark^#(U61(X1,X2))	→	a__U61^#(mark(X1),X2)	(141)
mark^#(U91(X1,X2,X3,X4))	→	mark^#(X1)	(142)
a__take^#(s(M),cons(N,IL))	→	a__U91^#(a__isNatIList(IL),IL,M,N)	(143)
mark^#(U72(X1,X2))	→	a__U72^#(mark(X1),X2)	(144)
a__take^#(0,IL)	→	a__isNatIList^#(IL)	(145)
mark^#(U81(X))	→	mark^#(X)	(146)
mark^#(U91(X1,X2,X3,X4))	→	a__U91^#(mark(X1),X2,X3,X4)	(147)
a__take^#(s(M),cons(N,IL))	→	a__isNatIList^#(IL)	(148)
a__U41^#(tt,V2)	→	a__U42^#(a__isNatIList(V2))	(149)
mark^#(U92(X1,X2,X3,X4))	→	mark^#(X1)	(150)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(U92(X1,X2,X3,X4))	→	mark^#(X1)	(150)
mark^#(U31(X))	→	mark^#(X)	(117)
mark^#(U21(X))	→	mark^#(X)	(114)
mark^#(length(X))	→	a__length^#(mark(X))	(115)
mark^#(U51(X1,X2))	→	mark^#(X1)	(113)
mark^#(U91(X1,X2,X3,X4))	→	a__U91^#(mark(X1),X2,X3,X4)	(147)
mark^#(length(X))	→	mark^#(X)	(111)
mark^#(U62(X))	→	mark^#(X)	(110)
mark^#(U81(X))	→	mark^#(X)	(146)
mark^#(U72(X1,X2))	→	a__U72^#(mark(X1),X2)	(144)
mark^#(cons(X1,X2))	→	mark^#(X1)	(107)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(106)
a__take^#(s(M),cons(N,IL))	→	a__U91^#(a__isNatIList(IL),IL,M,N)	(143)
mark^#(U91(X1,X2,X3,X4))	→	mark^#(X1)	(142)
a__U91^#(tt,IL,M,N)	→	a__U92^#(a__isNat(M),IL,M,N)	(140)
a__U92^#(tt,IL,M,N)	→	a__U93^#(a__isNat(N),IL,M,N)	(139)
a__U71^#(tt,L,N)	→	a__U72^#(a__isNat(N),L)	(138)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(102)
a__U72^#(tt,L)	→	a__length^#(mark(L))	(135)
mark^#(U92(X1,X2,X3,X4))	→	a__U92^#(mark(X1),X2,X3,X4)	(134)
mark^#(U93(X1,X2,X3,X4))	→	mark^#(X1)	(99)
mark^#(s(X))	→	mark^#(X)	(98)
a__length^#(cons(N,L))	→	a__U71^#(a__isNatList(L),L,N)	(96)
mark^#(U42(X))	→	mark^#(X)	(95)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(take(X1,X2))	→	mark^#(X1)	(89)
mark^#(U61(X1,X2))	→	mark^#(X1)	(130)
mark^#(take(X1,X2))	→	mark^#(X2)	(125)
a__U72^#(tt,L)	→	mark^#(L)	(124)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(122)
a__U93^#(tt,IL,M,N)	→	mark^#(N)	(81)
mark^#(U93(X1,X2,X3,X4))	→	a__U93^#(mark(X1),X2,X3,X4)	(121)
mark^#(U11(X))	→	mark^#(X)	(80)
mark^#(U72(X1,X2))	→	mark^#(X1)	(77)
mark^#(U52(X))	→	mark^#(X)	(119)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 0
[isNatList(x₁)]	=	1
[a__U72^#(x₁, x₂)]	=	x₂ + 7579
[a__U71^#(x₁, x₂, x₃)]	=	x₂ + 7579
[U11(x₁)]	=	x₁ + 0
[a__U92^#(x₁,...,x₄)]	=	x₄ + 2
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁)]	=	0
[a__U93^#(x₁,...,x₄)]	=	x₄ + 1
[a__isNatIList(x₁)]	=	1
[U42(x₁)]	=	x₁ + 0
[U91(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[a__isNat^#(x₁)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 5
[U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 7580
[a__U62(x₁)]	=	x₁ + 0
[isNatIList(x₁)]	=	1
[a__U51^#(x₁, x₂)]	=	0
[U93(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[U72(x₁, x₂)]	=	x₁ + x₂ + 7580
[a__U11^#(x₁)]	=	0
[zeros]	=	17067
[a__U31(x₁)]	=	x₁ + 0
[a__U51(x₁, x₂)]	=	x₁ + 0
[a__U81(x₁)]	=	x₁ + 1
[a__take^#(x₁, x₂)]	=	x₂ + 4
[a__isNatList(x₁)]	=	1
[a__U62^#(x₁)]	=	0
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₁ + 0
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[a__zeros^#]	=	0
[a__U21(x₁)]	=	x₁ + 0
[a__U91(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[nil]	=	2
[U62(x₁)]	=	x₁ + 0
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁, x₂)]	=	x₁ + x₂ + 7580
[a__U11(x₁)]	=	x₁ + 0
[a__U42(x₁)]	=	x₁ + 0
[a__U93(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[a__U52(x₁)]	=	x₁ + 0
[a__length^#(x₁)]	=	x₁ + 7579
[isNat(x₁)]	=	1
[U52(x₁)]	=	x₁ + 0
[U61(x₁, x₂)]	=	x₁ + 0
[U31(x₁)]	=	x₁ + 0
[a__isNatList^#(x₁)]	=	0
[a__U71(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 7580
[U92(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U92(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 4
[a__U61(x₁, x₂)]	=	x₁ + 0
[a__take(x₁, x₂)]	=	x₁ + x₂ + 5
[U81(x₁)]	=	x₁ + 1
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	1
[a__isNat(x₁)]	=	1
[U51(x₁, x₂)]	=	x₁ + 0
[length(x₁)]	=	x₁ + 7581
[U41(x₁, x₂)]	=	x₁ + 0
[a__zeros]	=	17067
[a__U91^#(x₁,...,x₄)]	=	x₂ + x₄ + 3
[a__length(x₁)]	=	x₁ + 7581

together with the usable rules

a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(18)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(50)
a__U31(tt)	→	tt	(4)
a__U92(tt,IL,M,N)	→	a__U93(a__isNat(N),IL,M,N)	(15)
a__U52(tt)	→	tt	(8)
mark(s(X))	→	s(mark(X))	(54)
a__zeros	→	cons(0,zeros)	(1)
a__U21(tt)	→	tt	(3)
a__U93(tt,IL,M,N)	→	cons(mark(N),take(M,IL))	(16)
a__isNatIList(zeros)	→	tt	(21)
mark(isNatIList(X))	→	a__isNatIList(X)	(36)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(68)
a__length(nil)	→	0	(26)
a__U51(X1,X2)	→	U51(X1,X2)	(63)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(19)
mark(U21(X))	→	a__U21(mark(X))	(32)
a__isNat(0)	→	tt	(17)
a__U41(X1,X2)	→	U41(X1,X2)	(60)
a__length(cons(N,L))	→	a__U71(a__isNatList(L),L,N)	(27)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(34)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(22)
a__take(0,IL)	→	a__U81(a__isNatIList(IL))	(28)
a__isNatList(X)	→	isNatList(X)	(65)
mark(isNat(X))	→	a__isNat(X)	(44)
a__U41(tt,V2)	→	a__U42(a__isNatIList(V2))	(5)
a__U81(X)	→	U81(X)	(72)
mark(U31(X))	→	a__U31(mark(X))	(33)
a__U52(X)	→	U52(X)	(64)
a__U62(tt)	→	tt	(10)
mark(isNatList(X))	→	a__isNatList(X)	(39)
a__U51(tt,V2)	→	a__U52(a__isNatList(V2))	(7)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(20)
a__isNatList(take(V1,V2))	→	a__U61(a__isNat(V1),V2)	(25)
mark(U93(X1,X2,X3,X4))	→	a__U93(mark(X1),X2,X3,X4)	(49)
mark(0)	→	0	(52)
mark(zeros)	→	a__zeros	(30)
a__isNatIList(X)	→	isNatIList(X)	(62)
a__U91(tt,IL,M,N)	→	a__U92(a__isNat(M),IL,M,N)	(14)
a__zeros	→	zeros	(56)
mark(U11(X))	→	a__U11(mark(X))	(31)
a__U72(tt,L)	→	s(a__length(mark(L)))	(12)
a__U72(X1,X2)	→	U72(X1,X2)	(69)
mark(length(X))	→	a__length(mark(X))	(45)
a__isNatList(nil)	→	tt	(23)
a__isNat(X)	→	isNat(X)	(70)
a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(24)
a__take(X1,X2)	→	take(X1,X2)	(76)
a__U11(X)	→	U11(X)	(57)
a__U71(tt,L,N)	→	a__U72(a__isNat(N),L)	(11)
a__U61(tt,V2)	→	a__U62(a__isNatIList(V2))	(9)
a__U81(tt)	→	nil	(13)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(51)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(40)
a__U62(X)	→	U62(X)	(67)
mark(nil)	→	nil	(55)
a__U31(X)	→	U31(X)	(59)
a__U42(tt)	→	tt	(6)
mark(U52(X))	→	a__U52(mark(X))	(38)
a__U42(X)	→	U42(X)	(61)
a__U21(X)	→	U21(X)	(58)
a__U92(X1,X2,X3,X4)	→	U92(X1,X2,X3,X4)	(74)
a__U93(X1,X2,X3,X4)	→	U93(X1,X2,X3,X4)	(75)
mark(U92(X1,X2,X3,X4))	→	a__U92(mark(X1),X2,X3,X4)	(48)
a__length(X)	→	length(X)	(71)
mark(tt)	→	tt	(53)
mark(U91(X1,X2,X3,X4))	→	a__U91(mark(X1),X2,X3,X4)	(47)
a__U91(X1,X2,X3,X4)	→	U91(X1,X2,X3,X4)	(73)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(37)
mark(U62(X))	→	a__U62(mark(X))	(41)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(42)
mark(U81(X))	→	a__U81(mark(X))	(46)
a__U61(X1,X2)	→	U61(X1,X2)	(66)
mark(U42(X))	→	a__U42(mark(X))	(35)
a__take(s(M),cons(N,IL))	→	a__U91(a__isNatIList(IL),IL,M,N)	(29)
mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(43)
a__U11(tt)	→	tt	(2)

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

mark^#(U92(X1,X2,X3,X4))	→	mark^#(X1)	(150)
mark^#(length(X))	→	a__length^#(mark(X))	(115)
mark^#(U91(X1,X2,X3,X4))	→	a__U91^#(mark(X1),X2,X3,X4)	(147)
mark^#(length(X))	→	mark^#(X)	(111)
mark^#(U81(X))	→	mark^#(X)	(146)
mark^#(U72(X1,X2))	→	a__U72^#(mark(X1),X2)	(144)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(106)
a__take^#(s(M),cons(N,IL))	→	a__U91^#(a__isNatIList(IL),IL,M,N)	(143)
mark^#(U91(X1,X2,X3,X4))	→	mark^#(X1)	(142)
a__U91^#(tt,IL,M,N)	→	a__U92^#(a__isNat(M),IL,M,N)	(140)
a__U92^#(tt,IL,M,N)	→	a__U93^#(a__isNat(N),IL,M,N)	(139)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(102)
mark^#(U92(X1,X2,X3,X4))	→	a__U92^#(mark(X1),X2,X3,X4)	(134)
mark^#(U93(X1,X2,X3,X4))	→	mark^#(X1)	(99)
mark^#(take(X1,X2))	→	mark^#(X1)	(89)
mark^#(take(X1,X2))	→	mark^#(X2)	(125)
a__U72^#(tt,L)	→	mark^#(L)	(124)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(122)
a__U93^#(tt,IL,M,N)	→	mark^#(N)	(81)
mark^#(U93(X1,X2,X3,X4))	→	a__U93^#(mark(X1),X2,X3,X4)	(121)
mark^#(U72(X1,X2))	→	mark^#(X1)	(77)

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__U71^#(a__isNatList(L),L,N)	(96)
a__U72^#(tt,L)	→	a__length^#(mark(L))	(135)
a__U71^#(tt,L,N)	→	a__U72^#(a__isNat(N),L)	(138)

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

[U21(x₁)]

0	0
0	1

· x₁ +

[isNatList(x₁)]

0	0
1	0

· x₁ +

32254

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

1	0
0	0

· x₁ +

0	1
0	0

· x₂ +

42088

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

1	1
0	0

· x₁ +

0	1
0	0

· x₂ +

[U11(x₁)]

42089

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

[s(x₁)]

0	1
0	1

· x₁ +

9835

[a__U31^#(x₁)]

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

[a__isNatIList(x₁)]

1	1
0	1

· x₁ +

71781

[U42(x₁)]

0	0
0	1

· x₁ +

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

0	0
0	1

· x₃ +

2511

69237

[a__isNat^#(x₁)]

[take(x₁, x₂)]

0	0
0	1

· x₁ +

9835

59402

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

0	0
0	1

· x₁ +

1	1
0	1

· x₂ +

32254

38705

[a__U62(x₁)]

42089

[isNatIList(x₁)]

1	1
0	1

· x₁ +

71781

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

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

0	1
0	1

· x₁ +

0	0
0	1

· x₃ +

27149

27148

[U72(x₁, x₂)]

0	0
0	1

· x₂ +

10169

80794

[a__U11^#(x₁)]

[zeros]

9834

[a__U31(x₁)]

42089

[a__U51(x₁, x₂)]

42089

[a__U81(x₁)]

9835

9460

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

[a__isNatList(x₁)]

0	0
1	0

· x₁ +

32254

[a__U62^#(x₁)]

[a__U42^#(x₁)]

[a__U41(x₁, x₂)]

0	0
0	1

· x₁ +

1	0
1	1

· x₂ +

29692

[a__U21^#(x₁)]

[a__isNatIList^#(x₁)]

[a__U81^#(x₁)]

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

[mark^#(x₁)]

[0]

73623

[a__zeros^#]

[a__U21(x₁)]

0	0
0	1

· x₁ +

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

0	0
0	1

· x₃ +

69238

69237

[nil]

9835

2664

[U62(x₁)]

42089

[a__U52^#(x₁)]

[mark(x₁)]

1	1
0	1

· x₁ +

[a__U72(x₁, x₂)]

0	1
0	1

· x₂ +

70960

80794

[a__U11(x₁)]

42089

[a__U42(x₁)]

0	0
0	1

· x₁ +

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

0	1
0	1

· x₁ +

0	0
0	1

· x₃ +

27149

27148

[a__U52(x₁)]

42089

[a__length^#(x₁)]

0	1
0	0

· x₁ +

42088

[isNat(x₁)]

42089

[U52(x₁)]

42089

[U61(x₁, x₂)]

42089

[U31(x₁)]

42089

[a__isNatList^#(x₁)]

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

0	0
0	1

· x₁ +

1	1
0	1

· x₂ +

70960

38705

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

0	1
0	1

· x₁ +

0	0
0	1

· x₃ +

24271

27148

[cons(x₁, x₂)]

0	0
1	1

· x₂ +

9835

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

0	1
0	1

· x₁ +

0	0
0	1

· x₃ +

27149

27148

[a__U61(x₁, x₂)]

42089

[a__take(x₁, x₂)]

0	0
0	1

· x₁ +

69238

59402

[U81(x₁)]

374

9460

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

[tt]

42089

[a__isNat(x₁)]

42089

[U51(x₁, x₂)]

42089

[length(x₁)]

0	0
0	1

· x₁ +

14818

70959

[U41(x₁, x₂)]

0	0
0	1

· x₁ +

1	0
1	1

· x₂ +

29692

[a__zeros]

9835

9834

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

[a__length(x₁)]

0	1
0	1

· x₁ +

70960

70959

together with the usable rules

a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(18)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(50)
a__U31(tt)	→	tt	(4)
a__U92(tt,IL,M,N)	→	a__U93(a__isNat(N),IL,M,N)	(15)
a__U52(tt)	→	tt	(8)
mark(s(X))	→	s(mark(X))	(54)
a__zeros	→	cons(0,zeros)	(1)
a__U21(tt)	→	tt	(3)
a__U93(tt,IL,M,N)	→	cons(mark(N),take(M,IL))	(16)
a__isNatIList(zeros)	→	tt	(21)
mark(isNatIList(X))	→	a__isNatIList(X)	(36)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(68)
a__length(nil)	→	0	(26)
a__U51(X1,X2)	→	U51(X1,X2)	(63)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(19)
mark(U21(X))	→	a__U21(mark(X))	(32)
a__isNat(0)	→	tt	(17)
a__U41(X1,X2)	→	U41(X1,X2)	(60)
a__length(cons(N,L))	→	a__U71(a__isNatList(L),L,N)	(27)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(34)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(22)
a__take(0,IL)	→	a__U81(a__isNatIList(IL))	(28)
a__isNatList(X)	→	isNatList(X)	(65)
mark(isNat(X))	→	a__isNat(X)	(44)
a__U41(tt,V2)	→	a__U42(a__isNatIList(V2))	(5)
a__U81(X)	→	U81(X)	(72)
mark(U31(X))	→	a__U31(mark(X))	(33)
a__U52(X)	→	U52(X)	(64)
a__U62(tt)	→	tt	(10)
mark(isNatList(X))	→	a__isNatList(X)	(39)
a__U51(tt,V2)	→	a__U52(a__isNatList(V2))	(7)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(20)
a__isNatList(take(V1,V2))	→	a__U61(a__isNat(V1),V2)	(25)
mark(U93(X1,X2,X3,X4))	→	a__U93(mark(X1),X2,X3,X4)	(49)
mark(0)	→	0	(52)
mark(zeros)	→	a__zeros	(30)
a__isNatIList(X)	→	isNatIList(X)	(62)
a__U91(tt,IL,M,N)	→	a__U92(a__isNat(M),IL,M,N)	(14)
a__zeros	→	zeros	(56)
mark(U11(X))	→	a__U11(mark(X))	(31)
a__U72(tt,L)	→	s(a__length(mark(L)))	(12)
a__U72(X1,X2)	→	U72(X1,X2)	(69)
mark(length(X))	→	a__length(mark(X))	(45)
a__isNatList(nil)	→	tt	(23)
a__isNat(X)	→	isNat(X)	(70)
a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(24)
a__take(X1,X2)	→	take(X1,X2)	(76)
a__U11(X)	→	U11(X)	(57)
a__U71(tt,L,N)	→	a__U72(a__isNat(N),L)	(11)
a__U61(tt,V2)	→	a__U62(a__isNatIList(V2))	(9)
a__U81(tt)	→	nil	(13)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(51)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(40)
a__U62(X)	→	U62(X)	(67)
mark(nil)	→	nil	(55)
a__U31(X)	→	U31(X)	(59)
a__U42(tt)	→	tt	(6)
mark(U52(X))	→	a__U52(mark(X))	(38)
a__U42(X)	→	U42(X)	(61)
a__U21(X)	→	U21(X)	(58)
a__U92(X1,X2,X3,X4)	→	U92(X1,X2,X3,X4)	(74)
a__U93(X1,X2,X3,X4)	→	U93(X1,X2,X3,X4)	(75)
mark(U92(X1,X2,X3,X4))	→	a__U92(mark(X1),X2,X3,X4)	(48)
a__length(X)	→	length(X)	(71)
mark(tt)	→	tt	(53)
mark(U91(X1,X2,X3,X4))	→	a__U91(mark(X1),X2,X3,X4)	(47)
a__U91(X1,X2,X3,X4)	→	U91(X1,X2,X3,X4)	(73)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(37)
mark(U62(X))	→	a__U62(mark(X))	(41)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(42)
mark(U81(X))	→	a__U81(mark(X))	(46)
a__U61(X1,X2)	→	U61(X1,X2)	(66)
mark(U42(X))	→	a__U42(mark(X))	(35)
a__take(s(M),cons(N,IL))	→	a__U91(a__isNatIList(IL),IL,M,N)	(29)
mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(43)
a__U11(tt)	→	tt	(2)

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

a__length^#(cons(N,L))	→	a__U71^#(a__isNatList(L),L,N)	(96)
a__U72^#(tt,L)	→	a__length^#(mark(L))	(135)
a__U71^#(tt,L,N)	→	a__U72^#(a__isNat(N),L)	(138)

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^#(s(X))	→	mark^#(X)	(98)
mark^#(U21(X))	→	mark^#(X)	(114)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(U31(X))	→	mark^#(X)	(117)
mark^#(U11(X))	→	mark^#(X)	(80)
mark^#(cons(X1,X2))	→	mark^#(X1)	(107)
mark^#(U61(X1,X2))	→	mark^#(X1)	(130)
mark^#(U52(X))	→	mark^#(X)	(119)
mark^#(U51(X1,X2))	→	mark^#(X1)	(113)
mark^#(U62(X))	→	mark^#(X)	(110)
mark^#(U42(X))	→	mark^#(X)	(95)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 15
[isNatList(x₁)]	=	13
[a__U72^#(x₁, x₂)]	=	7579
[a__U71^#(x₁, x₂, x₃)]	=	7578
[U11(x₁)]	=	x₁ + 15
[a__U92^#(x₁,...,x₄)]	=	2
[s(x₁)]	=	x₁ + 1
[a__U31^#(x₁)]	=	0
[a__U93^#(x₁,...,x₄)]	=	1
[a__isNatIList(x₁)]	=	12
[U42(x₁)]	=	x₁ + 15
[U91(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 13
[a__isNat^#(x₁)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[U71(x₁, x₂, x₃)]	=	x₁ + 13
[a__U62(x₁)]	=	14
[isNatIList(x₁)]	=	x₁ + 13
[a__U51^#(x₁, x₂)]	=	0
[U93(x₁,...,x₄)]	=	x₁ + x₄ + 2
[U72(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U11^#(x₁)]	=	0
[zeros]	=	13
[a__U31(x₁)]	=	13
[a__U51(x₁, x₂)]	=	13
[a__U81(x₁)]	=	19
[a__take^#(x₁, x₂)]	=	4
[a__isNatList(x₁)]	=	12
[a__U62^#(x₁)]	=	0
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₂ + 13
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	18
[a__zeros^#]	=	0
[a__U21(x₁)]	=	14
[a__U91(x₁,...,x₄)]	=	12
[nil]	=	12
[U62(x₁)]	=	x₁ + 15
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	11
[a__U72(x₁, x₂)]	=	x₁ + 1
[a__U11(x₁)]	=	14
[a__U42(x₁)]	=	14
[a__U93(x₁,...,x₄)]	=	x₁ + x₂ + 1
[a__U52(x₁)]	=	14
[a__length^#(x₁)]	=	7580
[isNat(x₁)]	=	14
[U52(x₁)]	=	x₁ + 15
[U61(x₁, x₂)]	=	x₁ + 14
[U31(x₁)]	=	x₁ + 14
[a__isNatList^#(x₁)]	=	0
[a__U71(x₁, x₂, x₃)]	=	x₃ + 12
[U92(x₁,...,x₄)]	=	x₁ + 14
[cons(x₁, x₂)]	=	x₁ + 6
[a__U92(x₁,...,x₄)]	=	x₂ + x₃ + x₄ + 13
[a__U61(x₁, x₂)]	=	x₂ + 13
[a__take(x₁, x₂)]	=	x₁ + x₂ + 0
[U81(x₁)]	=	x₁ + 20
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	15
[a__isNat(x₁)]	=	13
[U51(x₁, x₂)]	=	x₁ + 14
[length(x₁)]	=	x₁ + 7581
[U41(x₁, x₂)]	=	x₁ + 14
[a__zeros]	=	12
[a__U91^#(x₁,...,x₄)]	=	3
[a__length(x₁)]	=	x₁ + 5

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

mark^#(s(X))	→	mark^#(X)	(98)
mark^#(U21(X))	→	mark^#(X)	(114)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(U31(X))	→	mark^#(X)	(117)
mark^#(U11(X))	→	mark^#(X)	(80)
mark^#(cons(X1,X2))	→	mark^#(X1)	(107)
mark^#(U61(X1,X2))	→	mark^#(X1)	(130)
mark^#(U52(X))	→	mark^#(X)	(119)
mark^#(U51(X1,X2))	→	mark^#(X1)	(113)
mark^#(U62(X))	→	mark^#(X)	(110)
mark^#(U42(X))	→	mark^#(X)	(95)

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__U61^#(tt,V2)	→	a__isNatIList^#(V2)	(118)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(112)
a__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(100)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(97)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(91)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(129)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(127)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(123)
a__isNatList^#(take(V1,V2))	→	a__U61^#(a__isNat(V1),V2)	(84)
a__isNatList^#(take(V1,V2))	→	a__isNat^#(V1)	(83)
a__U51^#(tt,V2)	→	a__isNatList^#(V2)	(82)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(79)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 49125
[isNatList(x₁)]	=	24560
[a__U72^#(x₁, x₂)]	=	7579
[a__U71^#(x₁, x₂, x₃)]	=	7578
[U11(x₁)]	=	x₁ + 24567
[a__U92^#(x₁,...,x₄)]	=	2
[s(x₁)]	=	x₁ + 24564
[a__U31^#(x₁)]	=	0
[a__U93^#(x₁,...,x₄)]	=	1
[a__isNatIList(x₁)]	=	24559
[U42(x₁)]	=	x₁ + 24562
[U91(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 49123
[a__isNat^#(x₁)]	=	x₁ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 24580
[U71(x₁, x₂, x₃)]	=	x₁ + 24560
[a__U62(x₁)]	=	24561
[isNatIList(x₁)]	=	x₁ + 24560
[a__U51^#(x₁, x₂)]	=	x₂ + 0
[U93(x₁,...,x₄)]	=	x₁ + x₄ + 24566
[U72(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U11^#(x₁)]	=	0
[zeros]	=	24560
[a__U31(x₁)]	=	24560
[a__U51(x₁, x₂)]	=	24560
[a__U81(x₁)]	=	24566
[a__take^#(x₁, x₂)]	=	4
[a__isNatList(x₁)]	=	24559
[a__U62^#(x₁)]	=	0
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₂ + 24560
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	x₁ + 1
[a__U81^#(x₁)]	=	0
[a__U61^#(x₁, x₂)]	=	x₂ + 2
[mark^#(x₁)]	=	0
[0]	=	24565
[a__zeros^#]	=	0
[a__U21(x₁)]	=	49124
[a__U91(x₁,...,x₄)]	=	49122
[nil]	=	24559
[U62(x₁)]	=	x₁ + 24562
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	24558
[a__U72(x₁, x₂)]	=	x₁ + 1
[a__U11(x₁)]	=	24566
[a__U42(x₁)]	=	24561
[a__U93(x₁,...,x₄)]	=	x₁ + 24565
[a__U52(x₁)]	=	49124
[a__length^#(x₁)]	=	7580
[isNat(x₁)]	=	24560
[U52(x₁)]	=	x₁ + 49125
[U61(x₁, x₂)]	=	x₁ + 24561
[U31(x₁)]	=	x₁ + 24561
[a__isNatList^#(x₁)]	=	x₁ + 0
[a__U71(x₁, x₂, x₃)]	=	x₃ + 24559
[U92(x₁,...,x₄)]	=	x₁ + 49124
[cons(x₁, x₂)]	=	x₁ + x₂ + 24553
[a__U92(x₁,...,x₄)]	=	x₂ + x₃ + x₄ + 49123
[a__U61(x₁, x₂)]	=	x₂ + 24560
[a__take(x₁, x₂)]	=	x₁ + x₂ + 0
[U81(x₁)]	=	x₁ + 24567
[a__U41^#(x₁, x₂)]	=	x₂ + 24553
[tt]	=	49125
[a__isNat(x₁)]	=	x₁ + 24559
[U51(x₁, x₂)]	=	x₁ + 24561
[length(x₁)]	=	x₁ + 6
[U41(x₁, x₂)]	=	x₁ + 24561
[a__zeros]	=	24559
[a__U91^#(x₁,...,x₄)]	=	3
[a__length(x₁)]	=	x₁ + 5

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

a__U61^#(tt,V2)	→	a__isNatIList^#(V2)	(118)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(112)
a__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(100)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(97)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(91)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(129)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(127)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(123)
a__isNatList^#(take(V1,V2))	→	a__U61^#(a__isNat(V1),V2)	(84)
a__isNatList^#(take(V1,V2))	→	a__isNat^#(V1)	(83)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(79)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.