Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nokinds_GM)

The rewrite relation of the following TRS is considered.

a__zeros	→	cons(0,zeros)	(1)
a__U11(tt,L)	→	s(a__length(mark(L)))	(2)
a__and(tt,X)	→	mark(X)	(3)
a__isNat(0)	→	tt	(4)
a__isNat(length(V1))	→	a__isNatList(V1)	(5)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__isNatIList(V)	→	a__isNatList(V)	(7)
a__isNatIList(zeros)	→	tt	(8)
a__isNatIList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatIList(V2))	(9)
a__isNatList(nil)	→	tt	(10)
a__isNatList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatList(V2))	(11)
a__length(nil)	→	0	(12)
a__length(cons(N,L))	→	a__U11(a__and(a__isNatList(L),isNat(N)),L)	(13)
mark(zeros)	→	a__zeros	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(15)
mark(length(X))	→	a__length(mark(X))	(16)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(17)
mark(isNat(X))	→	a__isNat(X)	(18)
mark(isNatList(X))	→	a__isNatList(X)	(19)
mark(isNatIList(X))	→	a__isNatIList(X)	(20)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(21)
mark(0)	→	0	(22)
mark(tt)	→	tt	(23)
mark(s(X))	→	s(mark(X))	(24)
mark(nil)	→	nil	(25)
a__zeros	→	zeros	(26)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
a__length(X)	→	length(X)	(28)
a__and(X1,X2)	→	and(X1,X2)	(29)
a__isNat(X)	→	isNat(X)	(30)
a__isNatList(X)	→	isNatList(X)	(31)
a__isNatIList(X)	→	isNatIList(X)	(32)

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.

a__U11^#(tt,L)	→	mark^#(L)	(33)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(34)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(35)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatList(V2))	(36)
mark^#(s(X))	→	mark^#(X)	(37)
mark^#(U11(X1,X2))	→	mark^#(X1)	(38)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(39)
mark^#(zeros)	→	a__zeros^#	(40)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(41)
mark^#(isNat(X))	→	a__isNat^#(X)	(42)
mark^#(length(X))	→	a__length^#(mark(X))	(43)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatIList(V2))	(44)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(45)
a__length^#(cons(N,L))	→	a__and^#(a__isNatList(L),isNat(N))	(46)
a__and^#(tt,X)	→	mark^#(X)	(47)
mark^#(and(X1,X2))	→	mark^#(X1)	(48)
mark^#(cons(X1,X2))	→	mark^#(X1)	(49)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(51)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(52)
a__U11^#(tt,L)	→	a__length^#(mark(L))	(53)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(54)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(55)
a__length^#(cons(N,L))	→	a__U11^#(a__and(a__isNatList(L),isNat(N)),L)	(56)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(57)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(isNatList(X))	→	a__isNatList^#(X)	(57)
mark^#(isNat(X))	→	a__isNat^#(X)	(42)
a__length^#(cons(N,L))	→	a__U11^#(a__and(a__isNatList(L),isNat(N)),L)	(56)
a__isNatIList^#(V)	→	a__isNatList^#(V)	(41)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(55)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(54)
a__U11^#(tt,L)	→	a__length^#(mark(L))	(53)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(39)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(52)
mark^#(U11(X1,X2))	→	mark^#(X1)	(38)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(51)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(s(X))	→	mark^#(X)	(37)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatList(V2))	(36)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(35)
mark^#(cons(X1,X2))	→	mark^#(X1)	(49)
mark^#(and(X1,X2))	→	mark^#(X1)	(48)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(34)
a__and^#(tt,X)	→	mark^#(X)	(47)
a__length^#(cons(N,L))	→	a__and^#(a__isNatList(L),isNat(N))	(46)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(45)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatIList(V2))	(44)
a__U11^#(tt,L)	→	mark^#(L)	(33)
mark^#(length(X))	→	a__length^#(mark(X))	(43)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[isNatList(x₁)]	=	0
[U11(x₁, x₂)]	=	x₁ + x₂ + 2333
[s(x₁)]	=	x₁ + 0
[a__isNatIList(x₁)]	=	x₁ + 19507
[a__isNat^#(x₁)]	=	7177
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[isNatIList(x₁)]	=	x₁ + 19507
[a__U11^#(x₁, x₂)]	=	x₂ + 7178
[zeros]	=	1
[a__isNatList(x₁)]	=	7178
[a__isNatIList^#(x₁)]	=	x₁ + 19507
[mark^#(x₁)]	=	x₁ + 7177
[0]	=	0
[a__and^#(x₁, x₂)]	=	x₂ + 7177
[a__zeros^#]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 7178
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 2333
[a__length^#(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	0
[a__isNatList^#(x₁)]	=	7177
[cons(x₁, x₂)]	=	x₁ + x₂ + 7178
[tt]	=	7178
[a__isNat(x₁)]	=	7178
[a__and(x₁, x₂)]	=	x₁ + x₂ + 0
[length(x₁)]	=	x₁ + 2333
[a__zeros]	=	7179
[a__length(x₁)]	=	x₁ + 2333

together with the usable rules

mark(isNat(X))	→	a__isNat(X)	(18)
a__isNat(0)	→	tt	(4)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(15)
a__isNatIList(zeros)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__and(tt,X)	→	mark(X)	(3)
mark(length(X))	→	a__length(mark(X))	(16)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(21)
a__zeros	→	zeros	(26)
mark(isNatList(X))	→	a__isNatList(X)	(19)
a__isNatIList(X)	→	isNatIList(X)	(32)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(17)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
mark(0)	→	0	(22)
a__length(X)	→	length(X)	(28)
a__isNat(length(V1))	→	a__isNatList(V1)	(5)
a__isNatList(nil)	→	tt	(10)
a__isNatIList(V)	→	a__isNatList(V)	(7)
mark(isNatIList(X))	→	a__isNatIList(X)	(20)
mark(nil)	→	nil	(25)
a__isNat(X)	→	isNat(X)	(30)
mark(zeros)	→	a__zeros	(14)
a__isNatList(X)	→	isNatList(X)	(31)
a__length(nil)	→	0	(12)
mark(tt)	→	tt	(23)
mark(s(X))	→	s(mark(X))	(24)
a__isNatList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatList(V2))	(11)
a__isNatIList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatIList(V2))	(9)
a__length(cons(N,L))	→	a__U11(a__and(a__isNatList(L),isNat(N)),L)	(13)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__and(X1,X2)	→	and(X1,X2)	(29)
a__U11(tt,L)	→	s(a__length(mark(L)))	(2)

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

a__isNatIList^#(V)	→	a__isNatList^#(V)	(41)
a__isNatIList^#(cons(V1,V2))	→	a__isNat^#(V1)	(54)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(39)
mark^#(U11(X1,X2))	→	mark^#(X1)	(38)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(35)
mark^#(cons(X1,X2))	→	mark^#(X1)	(49)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(34)
a__length^#(cons(N,L))	→	a__and^#(a__isNatList(L),isNat(N))	(46)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatIList(V2))	(44)
a__U11^#(tt,L)	→	mark^#(L)	(33)
mark^#(length(X))	→	a__length^#(mark(X))	(43)

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

mark^#(isNat(X))	→	a__isNat^#(X)	(42)
a__and^#(tt,X)	→	mark^#(X)	(47)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(57)
mark^#(and(X1,X2))	→	mark^#(X1)	(48)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(51)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(55)
mark^#(s(X))	→	mark^#(X)	(37)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(45)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatList(V2))	(36)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(52)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[isNatList(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₂ + 2
[s(x₁)]	=	x₁ + 0
[a__isNatIList(x₁)]	=	x₁ + 9
[a__isNat^#(x₁)]	=	x₁ + 7176
[and(x₁, x₂)]	=	x₁ + x₂ + 3
[isNatIList(x₁)]	=	x₁ + 1
[a__U11^#(x₁, x₂)]	=	7178
[zeros]	=	1
[a__isNatList(x₁)]	=	x₁ + 4
[a__isNatIList^#(x₁)]	=	19507
[mark^#(x₁)]	=	x₁ + 7177
[0]	=	0
[a__and^#(x₁, x₂)]	=	x₂ + 7178
[a__zeros^#]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 8
[a__U11(x₁, x₂)]	=	x₂ + 10
[a__length^#(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 0
[a__isNatList^#(x₁)]	=	x₁ + 7177
[cons(x₁, x₂)]	=	x₁ + x₂ + 8
[tt]	=	5
[a__isNat(x₁)]	=	x₁ + 8
[a__and(x₁, x₂)]	=	x₁ + x₂ + 3
[length(x₁)]	=	x₁ + 2
[a__zeros]	=	9
[a__length(x₁)]	=	x₁ + 2

together with the usable rules

mark(isNat(X))	→	a__isNat(X)	(18)
a__isNat(0)	→	tt	(4)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(15)
a__isNatIList(zeros)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__and(tt,X)	→	mark(X)	(3)
mark(length(X))	→	a__length(mark(X))	(16)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(21)
a__zeros	→	zeros	(26)
mark(isNatList(X))	→	a__isNatList(X)	(19)
a__isNatIList(X)	→	isNatIList(X)	(32)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(17)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
mark(0)	→	0	(22)
a__length(X)	→	length(X)	(28)
a__isNat(length(V1))	→	a__isNatList(V1)	(5)
a__isNatList(nil)	→	tt	(10)
a__isNatIList(V)	→	a__isNatList(V)	(7)
mark(isNatIList(X))	→	a__isNatIList(X)	(20)
mark(nil)	→	nil	(25)
a__isNat(X)	→	isNat(X)	(30)
mark(zeros)	→	a__zeros	(14)
a__isNatList(X)	→	isNatList(X)	(31)
a__length(nil)	→	0	(12)
mark(tt)	→	tt	(23)
mark(s(X))	→	s(mark(X))	(24)
a__isNatList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatList(V2))	(11)
a__isNatIList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatIList(V2))	(9)
a__length(cons(N,L))	→	a__U11(a__and(a__isNatList(L),isNat(N)),L)	(13)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__and(X1,X2)	→	and(X1,X2)	(29)
a__U11(tt,L)	→	s(a__length(mark(L)))	(2)

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

mark^#(isNat(X))	→	a__isNat^#(X)	(42)
a__and^#(tt,X)	→	mark^#(X)	(47)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(57)
mark^#(and(X1,X2))	→	mark^#(X1)	(48)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(51)
a__isNat^#(length(V1))	→	a__isNatList^#(V1)	(55)
a__isNatList^#(cons(V1,V2))	→	a__isNat^#(V1)	(45)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNat(V1),isNatList(V2))	(36)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(s(X))

→

mark^#(X)

(37)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[isNatList(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₂ + 7692
[s(x₁)]	=	x₁ + 1
[a__isNatIList(x₁)]	=	x₁ + 5
[a__isNat^#(x₁)]	=	7176
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[isNatIList(x₁)]	=	x₁ + 1
[a__U11^#(x₁, x₂)]	=	7178
[zeros]	=	1
[a__isNatList(x₁)]	=	x₁ + 1
[a__isNatIList^#(x₁)]	=	19507
[mark^#(x₁)]	=	x₁ + 7177
[0]	=	0
[a__and^#(x₁, x₂)]	=	7178
[a__zeros^#]	=	0
[nil]	=	10
[mark(x₁)]	=	x₁ + 4
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 7692
[a__length^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 0
[a__isNatList^#(x₁)]	=	7177
[cons(x₁, x₂)]	=	x₁ + x₂ + 4
[tt]	=	3
[a__isNat(x₁)]	=	x₁ + 3
[a__and(x₁, x₂)]	=	x₁ + x₂ + 1
[length(x₁)]	=	x₁ + 7690
[a__zeros]	=	5
[a__length(x₁)]	=	x₁ + 7690

together with the usable rules

a__isNat(0)	→	tt	(4)
a__isNatIList(zeros)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__zeros	→	zeros	(26)
a__isNatIList(X)	→	isNatIList(X)	(32)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
mark(0)	→	0	(22)
a__length(X)	→	length(X)	(28)
a__isNatList(nil)	→	tt	(10)
mark(nil)	→	nil	(25)
a__isNat(X)	→	isNat(X)	(30)
mark(zeros)	→	a__zeros	(14)
a__isNatList(X)	→	isNatList(X)	(31)
a__length(nil)	→	0	(12)
mark(tt)	→	tt	(23)
a__and(X1,X2)	→	and(X1,X2)	(29)

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

mark^#(s(X))

→

mark^#(X)

(37)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__isNat^#(s(V1))

→

a__isNat^#(V1)

(52)

1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[isNatList(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₂ + 18870
[s(x₁)]	=	x₁ + 1
[a__isNatIList(x₁)]	=	x₁ + 11
[a__isNat^#(x₁)]	=	x₁ + 7176
[and(x₁, x₂)]	=	x₁ + x₂ + 4
[isNatIList(x₁)]	=	x₁ + 1
[a__U11^#(x₁, x₂)]	=	7178
[zeros]	=	1
[a__isNatList(x₁)]	=	x₁ + 3
[a__isNatIList^#(x₁)]	=	19507
[mark^#(x₁)]	=	7177
[0]	=	0
[a__and^#(x₁, x₂)]	=	7178
[a__zeros^#]	=	0
[nil]	=	10
[mark(x₁)]	=	x₁ + 10
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 18870
[a__length^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 0
[a__isNatList^#(x₁)]	=	7177
[cons(x₁, x₂)]	=	x₁ + x₂ + 10
[tt]	=	8
[a__isNat(x₁)]	=	x₁ + 8
[a__and(x₁, x₂)]	=	x₁ + x₂ + 4
[length(x₁)]	=	x₁ + 18867
[a__zeros]	=	11
[a__length(x₁)]	=	x₁ + 18867

together with the usable rules

a__isNat(0)	→	tt	(4)
a__isNatIList(zeros)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__zeros	→	zeros	(26)
a__isNatIList(X)	→	isNatIList(X)	(32)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
mark(0)	→	0	(22)
a__length(X)	→	length(X)	(28)
a__isNatList(nil)	→	tt	(10)
mark(nil)	→	nil	(25)
a__isNat(X)	→	isNat(X)	(30)
mark(zeros)	→	a__zeros	(14)
a__isNatList(X)	→	isNatList(X)	(31)
a__length(nil)	→	0	(12)
mark(tt)	→	tt	(23)
a__and(X1,X2)	→	and(X1,X2)	(29)

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

a__isNat^#(s(V1))

→

a__isNat^#(V1)

(52)

could be deleted.

1.1.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__length^#(cons(N,L))	→	a__U11^#(a__and(a__isNatList(L),isNat(N)),L)	(56)
a__U11^#(tt,L)	→	a__length^#(mark(L))	(53)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

[isNatList(x₁)]

1	0
1	0

· x₁ +

99494

[U11(x₁, x₂)]

0	1
0	1

· x₁ +

1	0
1	0

· x₂ +

25826

11727

[s(x₁)]

x₁ +

[a__isNatIList(x₁)]

1	1
1	0

· x₁ +

191823

144305

[a__isNat^#(x₁)]

[and(x₁, x₂)]

0	1
0	0

· x₁ + x₂ +

21636

15392

[isNatIList(x₁)]

1	1
1	0

· x₁ +

108851

61333

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

x₁ +

0	1
1	0

· x₂ +

[zeros]

555

[a__isNatList(x₁)]

1	0
1	0

· x₁ +

182466

61335

[a__isNatIList^#(x₁)]

[mark^#(x₁)]

[0]

61332

82972

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

[a__zeros^#]

[nil]

82970

23092

[mark(x₁)]

x₁ +

82972

[a__U11(x₁, x₂)]

0	1
0	1

· x₁ +

1	0
1	0

· x₂ +

25826

11727

[a__length^#(x₁)]

0	1
1	0

· x₁ +

109405

61333

[isNat(x₁)]

0	1
1	0

· x₁ +

26434

[a__isNatList^#(x₁)]

[cons(x₁, x₂)]

x₁ +

1	0
1	1

· x₂ +

21640

[tt]

192378

144305

[a__isNat(x₁)]

0	1
1	0

· x₁ +

109406

82973

[a__and(x₁, x₂)]

0	1
0	0

· x₁ + x₂ +

21636

82972

[length(x₁)]

1	0
1	0

· x₁ +

87159

73060

[a__zeros]

82972

83527

[a__length(x₁)]

1	0
1	0

· x₁ +

87159

73060

together with the usable rules

mark(isNat(X))	→	a__isNat(X)	(18)
a__isNat(0)	→	tt	(4)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(15)
a__isNatIList(zeros)	→	tt	(8)
a__zeros	→	cons(0,zeros)	(1)
a__and(tt,X)	→	mark(X)	(3)
mark(length(X))	→	a__length(mark(X))	(16)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(21)
a__zeros	→	zeros	(26)
mark(isNatList(X))	→	a__isNatList(X)	(19)
a__isNatIList(X)	→	isNatIList(X)	(32)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(17)
a__U11(X1,X2)	→	U11(X1,X2)	(27)
mark(0)	→	0	(22)
a__length(X)	→	length(X)	(28)
a__isNat(length(V1))	→	a__isNatList(V1)	(5)
a__isNatList(nil)	→	tt	(10)
a__isNatIList(V)	→	a__isNatList(V)	(7)
mark(isNatIList(X))	→	a__isNatIList(X)	(20)
mark(nil)	→	nil	(25)
a__isNat(X)	→	isNat(X)	(30)
mark(zeros)	→	a__zeros	(14)
a__isNatList(X)	→	isNatList(X)	(31)
a__length(nil)	→	0	(12)
mark(tt)	→	tt	(23)
mark(s(X))	→	s(mark(X))	(24)
a__isNatList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatList(V2))	(11)
a__isNatIList(cons(V1,V2))	→	a__and(a__isNat(V1),isNatIList(V2))	(9)
a__length(cons(N,L))	→	a__U11(a__and(a__isNatList(L),isNat(N)),L)	(13)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__and(X1,X2)	→	and(X1,X2)	(29)
a__U11(tt,L)	→	s(a__length(mark(L)))	(2)

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

a__U11^#(tt,L)

→

a__length^#(mark(L))

(53)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.