Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_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,L,N)	→	a__U62(a__isNat(N),L)	(9)
a__U62(tt,L)	→	s(a__length(mark(L)))	(10)
a__isNat(0)	→	tt	(11)
a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(12)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(13)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(14)
a__isNatIList(zeros)	→	tt	(15)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(16)
a__isNatList(nil)	→	tt	(17)
a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(18)
a__length(nil)	→	0	(19)
a__length(cons(N,L))	→	a__U61(a__isNatList(L),L,N)	(20)
mark(zeros)	→	a__zeros	(21)
mark(U11(X))	→	a__U11(mark(X))	(22)
mark(U21(X))	→	a__U21(mark(X))	(23)
mark(U31(X))	→	a__U31(mark(X))	(24)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(25)
mark(U42(X))	→	a__U42(mark(X))	(26)
mark(isNatIList(X))	→	a__isNatIList(X)	(27)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(28)
mark(U52(X))	→	a__U52(mark(X))	(29)
mark(isNatList(X))	→	a__isNatList(X)	(30)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(31)
mark(U62(X1,X2))	→	a__U62(mark(X1),X2)	(32)
mark(isNat(X))	→	a__isNat(X)	(33)
mark(length(X))	→	a__length(mark(X))	(34)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(35)
mark(0)	→	0	(36)
mark(tt)	→	tt	(37)
mark(s(X))	→	s(mark(X))	(38)
mark(nil)	→	nil	(39)
a__zeros	→	zeros	(40)
a__U11(X)	→	U11(X)	(41)
a__U21(X)	→	U21(X)	(42)
a__U31(X)	→	U31(X)	(43)
a__U41(X1,X2)	→	U41(X1,X2)	(44)
a__U42(X)	→	U42(X)	(45)
a__isNatIList(X)	→	isNatIList(X)	(46)
a__U51(X1,X2)	→	U51(X1,X2)	(47)
a__U52(X)	→	U52(X)	(48)
a__isNatList(X)	→	isNatList(X)	(49)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(50)
a__U62(X1,X2)	→	U62(X1,X2)	(51)
a__isNat(X)	→	isNat(X)	(52)
a__length(X)	→	length(X)	(53)

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^#(U52(X))	→	mark^#(X)	(54)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(55)
a__U41^#(tt,V2)	→	a__U42^#(a__isNatIList(V2))	(56)
mark^#(length(X))	→	a__length^#(mark(X))	(57)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(58)
mark^#(zeros)	→	a__zeros^#	(59)
mark^#(U42(X))	→	mark^#(X)	(60)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(61)
mark^#(U62(X1,X2))	→	a__U62^#(mark(X1),X2)	(62)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(63)
mark^#(U42(X))	→	a__U42^#(mark(X))	(64)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatList(V1))	(65)
mark^#(U31(X))	→	a__U31^#(mark(X))	(66)
mark^#(U21(X))	→	a__U21^#(mark(X))	(67)
a__U51^#(tt,V2)	→	a__U52^#(a__isNatList(V2))	(68)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(69)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(70)
mark^#(U21(X))	→	mark^#(X)	(71)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(72)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(73)
a__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(74)
a__U51^#(tt,V2)	→	a__isNatList^#(V2)	(75)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(76)
a__U61^#(tt,L,N)	→	a__U62^#(a__isNat(N),L)	(77)
mark^#(U62(X1,X2))	→	mark^#(X1)	(78)
mark^#(U31(X))	→	mark^#(X)	(79)
mark^#(U11(X))	→	a__U11^#(mark(X))	(80)
a__isNat^#(s(V1))	→	a__U21^#(a__isNat(V1))	(81)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(82)
mark^#(isNat(X))	→	a__isNat^#(X)	(83)
a__length^#(cons(N,L))	→	a__U61^#(a__isNatList(L),L,N)	(84)
mark^#(U11(X))	→	mark^#(X)	(85)
a__U62^#(tt,L)	→	mark^#(L)	(86)
a__isNatIList^#(V)	→	a__U31^#(a__isNatList(V))	(87)
mark^#(U51(X1,X2))	→	mark^#(X1)	(88)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(89)
a__U62^#(tt,L)	→	a__length^#(mark(L))	(90)
mark^#(length(X))	→	mark^#(X)	(91)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(93)
mark^#(cons(X1,X2))	→	mark^#(X1)	(94)
mark^#(U52(X))	→	a__U52^#(mark(X))	(95)
a__U61^#(tt,L,N)	→	a__isNat^#(N)	(96)
mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(97)
mark^#(s(X))	→	mark^#(X)	(98)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(99)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(98)
mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(97)
mark^#(U21(X))	→	mark^#(X)	(71)
mark^#(cons(X1,X2))	→	mark^#(X1)	(94)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(93)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(length(X))	→	mark^#(X)	(91)
a__U62^#(tt,L)	→	a__length^#(mark(L))	(90)
mark^#(U51(X1,X2))	→	mark^#(X1)	(88)
a__U62^#(tt,L)	→	mark^#(L)	(86)
mark^#(U62(X1,X2))	→	a__U62^#(mark(X1),X2)	(62)
mark^#(U11(X))	→	mark^#(X)	(85)
a__length^#(cons(N,L))	→	a__U61^#(a__isNatList(L),L,N)	(84)
mark^#(U42(X))	→	mark^#(X)	(60)
mark^#(U31(X))	→	mark^#(X)	(79)
mark^#(U62(X1,X2))	→	mark^#(X1)	(78)
a__U61^#(tt,L,N)	→	a__U62^#(a__isNat(N),L)	(77)
mark^#(length(X))	→	a__length^#(mark(X))	(57)
mark^#(U52(X))	→	mark^#(X)	(54)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 0
[isNatList(x₁)]	=	1
[U11(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁)]	=	0
[a__isNatIList(x₁)]	=	x₁ + 2
[U42(x₁)]	=	x₁ + 1
[a__isNat^#(x₁)]	=	0
[a__U62(x₁, x₂)]	=	x₁ + x₂ + 2
[isNatIList(x₁)]	=	x₁ + 2
[a__U51^#(x₁, x₂)]	=	0
[a__U11^#(x₁)]	=	0
[zeros]	=	1
[a__U31(x₁)]	=	x₁ + 1
[a__U51(x₁, x₂)]	=	x₁ + 0
[a__isNatList(x₁)]	=	1
[a__U62^#(x₁, x₂)]	=	x₂ + 1
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U61^#(x₁, x₂, x₃)]	=	x₂ + 1
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[a__zeros^#]	=	0
[a__U21(x₁)]	=	x₁ + 0
[nil]	=	14586
[U62(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[a__U11(x₁)]	=	x₁ + 0
[a__U42(x₁)]	=	x₁ + 1
[a__U52(x₁)]	=	x₁ + 0
[a__length^#(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	1
[U52(x₁)]	=	x₁ + 0
[U61(x₁, x₂, x₃)]	=	x₁ + x₂ + 2
[U31(x₁)]	=	x₁ + 1
[a__isNatList^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U61(x₁, x₂, x₃)]	=	x₁ + x₂ + 2
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	1
[a__isNat(x₁)]	=	1
[U51(x₁, x₂)]	=	x₁ + 0
[length(x₁)]	=	x₁ + 2
[U41(x₁, x₂)]	=	x₁ + x₂ + 2
[a__zeros]	=	2
[a__length(x₁)]	=	x₁ + 2

together with the usable rules

a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(18)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(50)
a__U31(tt)	→	tt	(4)
a__isNatIList(zeros)	→	tt	(15)
a__U52(tt)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__U21(tt)	→	tt	(3)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(16)
mark(zeros)	→	a__zeros	(21)
mark(0)	→	0	(36)
mark(U42(X))	→	a__U42(mark(X))	(26)
a__length(nil)	→	0	(19)
mark(U62(X1,X2))	→	a__U62(mark(X1),X2)	(32)
a__isNatList(nil)	→	tt	(17)
mark(isNatIList(X))	→	a__isNatIList(X)	(27)
mark(length(X))	→	a__length(mark(X))	(34)
mark(U11(X))	→	a__U11(mark(X))	(22)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(28)
a__U41(X1,X2)	→	U41(X1,X2)	(44)
a__U41(tt,V2)	→	a__U42(a__isNatIList(V2))	(5)
mark(isNat(X))	→	a__isNat(X)	(33)
a__U62(tt,L)	→	s(a__length(mark(L)))	(10)
mark(nil)	→	nil	(39)
a__U51(tt,V2)	→	a__U52(a__isNatList(V2))	(7)
a__length(cons(N,L))	→	a__U61(a__isNatList(L),L,N)	(20)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(25)
a__isNatList(X)	→	isNatList(X)	(49)
a__isNat(X)	→	isNat(X)	(52)
mark(isNatList(X))	→	a__isNatList(X)	(30)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(14)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(31)
a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(12)
a__U42(X)	→	U42(X)	(45)
mark(U21(X))	→	a__U21(mark(X))	(23)
mark(U31(X))	→	a__U31(mark(X))	(24)
a__isNat(0)	→	tt	(11)
a__U61(tt,L,N)	→	a__U62(a__isNat(N),L)	(9)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(13)
a__U62(X1,X2)	→	U62(X1,X2)	(51)
a__zeros	→	zeros	(40)
a__U42(tt)	→	tt	(6)
mark(s(X))	→	s(mark(X))	(38)
a__U52(X)	→	U52(X)	(48)
a__length(X)	→	length(X)	(53)
a__U51(X1,X2)	→	U51(X1,X2)	(47)
mark(tt)	→	tt	(37)
a__U11(X)	→	U11(X)	(41)
a__U21(X)	→	U21(X)	(42)
a__isNatIList(X)	→	isNatIList(X)	(46)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(35)
mark(U52(X))	→	a__U52(mark(X))	(29)
a__U31(X)	→	U31(X)	(43)
a__U11(tt)	→	tt	(2)

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

mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(97)
mark^#(cons(X1,X2))	→	mark^#(X1)	(94)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(93)
mark^#(U41(X1,X2))	→	mark^#(X1)	(92)
mark^#(length(X))	→	mark^#(X)	(91)
a__U62^#(tt,L)	→	mark^#(L)	(86)
mark^#(U62(X1,X2))	→	a__U62^#(mark(X1),X2)	(62)
mark^#(U42(X))	→	mark^#(X)	(60)
mark^#(U31(X))	→	mark^#(X)	(79)
mark^#(U62(X1,X2))	→	mark^#(X1)	(78)
mark^#(length(X))	→	a__length^#(mark(X))	(57)

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__U62^#(tt,L)	→	a__length^#(mark(L))	(90)
a__length^#(cons(N,L))	→	a__U61^#(a__isNatList(L),L,N)	(84)
a__U61^#(tt,L,N)	→	a__U62^#(a__isNat(N),L)	(77)

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₁)]

22136

[isNatList(x₁)]

x₁ +

[U11(x₁)]

0	1
0	1

· x₁ +

[s(x₁)]

22137

[a__U31^#(x₁)]

[a__isNatIList(x₁)]

0	1
0	0

· x₁ +

22137

[U42(x₁)]

22137

[a__isNat^#(x₁)]

[a__U62(x₁, x₂)]

22137

[isNatIList(x₁)]

0	1
0	0

· x₁ +

22136

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

[a__U11^#(x₁)]

[zeros]

[a__U31(x₁)]

0	1
0	0

· x₁ +

22137

[a__U51(x₁, x₂)]

0	1
0	0

· x₁ +

0	0
0	1

· x₂ +

[a__isNatList(x₁)]

x₁ +

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

0	1
0	1

· x₁ +

1	0
1	1

· x₂ +

22136

22137

[a__U42^#(x₁)]

[a__U41(x₁, x₂)]

0	1
0	0

· x₂ +

22137

[a__U21^#(x₁)]

[a__isNatIList^#(x₁)]

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

0	1
0	1

· x₁ +

1	0
1	1

· x₂ +

1	0
1	0

· x₃ +

[mark^#(x₁)]

[0]

22137

[a__zeros^#]

[a__U21(x₁)]

22137

[nil]

19796

22137

[U62(x₁, x₂)]

12699

[a__U52^#(x₁)]

[mark(x₁)]

x₁ +

44271

[a__U11(x₁)]

0	1
0	1

· x₁ +

[a__U42(x₁)]

22137

[a__U52(x₁)]

0	0
0	1

· x₁ +

[a__length^#(x₁)]

1	0
1	1

· x₁ +

[isNat(x₁)]

1	1
1	0

· x₁ +

[U52(x₁)]

0	0
0	1

· x₁ +

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

[U31(x₁)]

0	1
0	0

· x₁ +

22136

[a__isNatList^#(x₁)]

[cons(x₁, x₂)]

1	0
0	0

· x₁ +

1	1
0	1

· x₂ +

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

22137

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

[tt]

22137

[a__isNat(x₁)]

1	1
1	0

· x₁ +

[U51(x₁, x₂)]

0	1
0	0

· x₁ +

0	0
0	1

· x₂ +

[length(x₁)]

0	1
0	1

· x₁ +

[U41(x₁, x₂)]

0	1
0	0

· x₂ +

22136

[a__zeros]

22137

[a__length(x₁)]

0	1
0	1

· x₁ +

44270

together with the usable rules

a__isNatList(cons(V1,V2))	→	a__U51(a__isNat(V1),V2)	(18)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(50)
a__U31(tt)	→	tt	(4)
a__isNatIList(zeros)	→	tt	(15)
a__U52(tt)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__U21(tt)	→	tt	(3)
a__isNatIList(cons(V1,V2))	→	a__U41(a__isNat(V1),V2)	(16)
mark(zeros)	→	a__zeros	(21)
mark(0)	→	0	(36)
mark(U42(X))	→	a__U42(mark(X))	(26)
a__length(nil)	→	0	(19)
mark(U62(X1,X2))	→	a__U62(mark(X1),X2)	(32)
a__isNatList(nil)	→	tt	(17)
mark(isNatIList(X))	→	a__isNatIList(X)	(27)
mark(length(X))	→	a__length(mark(X))	(34)
mark(U11(X))	→	a__U11(mark(X))	(22)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(28)
a__U41(X1,X2)	→	U41(X1,X2)	(44)
a__U41(tt,V2)	→	a__U42(a__isNatIList(V2))	(5)
mark(isNat(X))	→	a__isNat(X)	(33)
a__U62(tt,L)	→	s(a__length(mark(L)))	(10)
mark(nil)	→	nil	(39)
a__U51(tt,V2)	→	a__U52(a__isNatList(V2))	(7)
a__length(cons(N,L))	→	a__U61(a__isNatList(L),L,N)	(20)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(25)
a__isNatList(X)	→	isNatList(X)	(49)
a__isNat(X)	→	isNat(X)	(52)
mark(isNatList(X))	→	a__isNatList(X)	(30)
a__isNatIList(V)	→	a__U31(a__isNatList(V))	(14)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(31)
a__isNat(length(V1))	→	a__U11(a__isNatList(V1))	(12)
a__U42(X)	→	U42(X)	(45)
mark(U21(X))	→	a__U21(mark(X))	(23)
mark(U31(X))	→	a__U31(mark(X))	(24)
a__isNat(0)	→	tt	(11)
a__U61(tt,L,N)	→	a__U62(a__isNat(N),L)	(9)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(13)
a__U62(X1,X2)	→	U62(X1,X2)	(51)
a__zeros	→	zeros	(40)
a__U42(tt)	→	tt	(6)
mark(s(X))	→	s(mark(X))	(38)
a__U52(X)	→	U52(X)	(48)
a__length(X)	→	length(X)	(53)
a__U51(X1,X2)	→	U51(X1,X2)	(47)
mark(tt)	→	tt	(37)
a__U11(X)	→	U11(X)	(41)
a__U21(X)	→	U21(X)	(42)
a__isNatIList(X)	→	isNatIList(X)	(46)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(35)
mark(U52(X))	→	a__U52(mark(X))	(29)
a__U31(X)	→	U31(X)	(43)
a__U11(tt)	→	tt	(2)

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

a__U62^#(tt,L)	→	a__length^#(mark(L))	(90)
a__length^#(cons(N,L))	→	a__U61^#(a__isNatList(L),L,N)	(84)
a__U61^#(tt,L,N)	→	a__U62^#(a__isNat(N),L)	(77)

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^#(U11(X))	→	mark^#(X)	(85)
mark^#(U51(X1,X2))	→	mark^#(X1)	(88)
mark^#(U21(X))	→	mark^#(X)	(71)
mark^#(s(X))	→	mark^#(X)	(98)
mark^#(U52(X))	→	mark^#(X)	(54)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 2
[isNatList(x₁)]	=	3
[U11(x₁)]	=	x₁ + 8
[s(x₁)]	=	x₁ + 13
[a__U31^#(x₁)]	=	0
[a__isNatIList(x₁)]	=	x₁ + 2
[U42(x₁)]	=	x₁ + 8
[a__isNat^#(x₁)]	=	0
[a__U62(x₁, x₂)]	=	x₁ + x₂ + 6
[isNatIList(x₁)]	=	3
[a__U51^#(x₁, x₂)]	=	0
[a__U11^#(x₁)]	=	0
[zeros]	=	3
[a__U31(x₁)]	=	x₁ + 1
[a__U51(x₁, x₂)]	=	x₂ + 6
[a__isNatList(x₁)]	=	x₁ + 2
[a__U62^#(x₁, x₂)]	=	1
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₁ + 6
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U61^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	7
[a__zeros^#]	=	0
[a__U21(x₁)]	=	x₁ + 1
[nil]	=	5
[U62(x₁, x₂)]	=	x₁ + 7
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	1
[a__U11(x₁)]	=	7
[a__U42(x₁)]	=	7
[a__U52(x₁)]	=	7
[a__length^#(x₁)]	=	1
[isNat(x₁)]	=	1
[U52(x₁)]	=	x₁ + 8
[U61(x₁, x₂, x₃)]	=	x₁ + x₃ + 6
[U31(x₁)]	=	x₁ + 2
[a__isNatList^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[a__U61(x₁, x₂, x₃)]	=	5
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	8
[a__isNat(x₁)]	=	0
[U51(x₁, x₂)]	=	x₁ + 7
[length(x₁)]	=	x₁ + 2
[U41(x₁, x₂)]	=	x₁ + x₂ + 7
[a__zeros]	=	2
[a__length(x₁)]	=	x₁ + 1

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

mark^#(U11(X))	→	mark^#(X)	(85)
mark^#(U51(X1,X2))	→	mark^#(X1)	(88)
mark^#(U21(X))	→	mark^#(X)	(71)
mark^#(s(X))	→	mark^#(X)	(98)
mark^#(U52(X))	→	mark^#(X)	(54)

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__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(74)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(55)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 2
[isNatList(x₁)]	=	3
[U11(x₁)]	=	x₁ + 8
[s(x₁)]	=	x₁ + 5
[a__U31^#(x₁)]	=	0
[a__isNatIList(x₁)]	=	x₁ + 2
[U42(x₁)]	=	x₁ + 3
[a__isNat^#(x₁)]	=	0
[a__U62(x₁, x₂)]	=	x₂ + 6
[isNatIList(x₁)]	=	3
[a__U51^#(x₁, x₂)]	=	0
[a__U11^#(x₁)]	=	0
[zeros]	=	3
[a__U31(x₁)]	=	x₁ + 1
[a__U51(x₁, x₂)]	=	x₂ + 6
[a__isNatList(x₁)]	=	x₁ + 2
[a__U62^#(x₁, x₂)]	=	1
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₁ + 5
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	x₁ + 0
[a__U61^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[a__zeros^#]	=	0
[a__U21(x₁)]	=	x₁ + 1
[nil]	=	5
[U62(x₁, x₂)]	=	x₁ + 7
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	1
[a__U11(x₁)]	=	7
[a__U42(x₁)]	=	2
[a__U52(x₁)]	=	7
[a__length^#(x₁)]	=	1
[isNat(x₁)]	=	x₁ + 2
[U52(x₁)]	=	x₁ + 8
[U61(x₁, x₂, x₃)]	=	x₁ + x₃ + 4
[U31(x₁)]	=	x₁ + 2
[a__isNatList^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 3
[a__U61(x₁, x₂, x₃)]	=	3
[a__U41^#(x₁, x₂)]	=	x₂ + 2
[tt]	=	8
[a__isNat(x₁)]	=	1
[U51(x₁, x₂)]	=	x₁ + 7
[length(x₁)]	=	3
[U41(x₁, x₂)]	=	x₁ + x₂ + 6
[a__zeros]	=	2
[a__length(x₁)]	=	2

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

a__U41^#(tt,V2)	→	a__isNatIList^#(V2)	(74)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__isNat(V1),V2)	(55)

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

a__U51^#(tt,V2)	→	a__isNatList^#(V2)	(75)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(73)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(70)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(63)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(58)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁)]	=	x₁ + 2
[isNatList(x₁)]	=	3
[U11(x₁)]	=	x₁ + 3
[s(x₁)]	=	x₁ + 5
[a__U31^#(x₁)]	=	0
[a__isNatIList(x₁)]	=	x₁ + 2
[U42(x₁)]	=	x₁ + 3
[a__isNat^#(x₁)]	=	x₁ + 0
[a__U62(x₁, x₂)]	=	x₂ + 6
[isNatIList(x₁)]	=	3
[a__U51^#(x₁, x₂)]	=	x₂ + 1
[a__U11^#(x₁)]	=	0
[zeros]	=	4
[a__U31(x₁)]	=	x₁ + 1
[a__U51(x₁, x₂)]	=	x₂ + 9
[a__isNatList(x₁)]	=	x₁ + 2
[a__U62^#(x₁, x₂)]	=	1
[a__U42^#(x₁)]	=	0
[a__U41(x₁, x₂)]	=	x₁ + 5
[a__U21^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0
[a__U61^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[a__zeros^#]	=	0
[a__U21(x₁)]	=	x₁ + 1
[nil]	=	5
[U62(x₁, x₂)]	=	x₁ + 7
[a__U52^#(x₁)]	=	0
[mark(x₁)]	=	1
[a__U11(x₁)]	=	2
[a__U42(x₁)]	=	2
[a__U52(x₁)]	=	10
[a__length^#(x₁)]	=	1
[isNat(x₁)]	=	x₁ + 2
[U52(x₁)]	=	x₁ + 11
[U61(x₁, x₂, x₃)]	=	x₁ + x₃ + 4
[U31(x₁)]	=	x₁ + 2
[a__isNatList^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U61(x₁, x₂, x₃)]	=	3
[a__U41^#(x₁, x₂)]	=	2
[tt]	=	11
[a__isNat(x₁)]	=	1
[U51(x₁, x₂)]	=	x₁ + 10
[length(x₁)]	=	x₁ + 3
[U41(x₁, x₂)]	=	x₁ + x₂ + 6
[a__zeros]	=	2
[a__length(x₁)]	=	2

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

a__U51^#(tt,V2)	→	a__isNatList^#(V2)	(75)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(73)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__isNat(V1),V2)	(70)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(63)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(58)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.