Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_DLMMU04_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  mark#(s(X))	→	mark#(X)	(90)
  a__isNatList#(take(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(66)
  a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
  mark#(length(X))	→	mark#(X)	(65)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(M)	(64)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(88)
  mark#(uLength(X1,X2))	→	a__uLength#(mark(X1),X2)	(63)
  a__take#(s(M),cons(N,IL))	→	a__uTake2#(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(62)
  a__isNat#(s(N))	→	a__isNat#(N)	(61)
  a__isNatIList#(IL)	→	a__isNatList#(IL)	(86)
  a__isNatIList#(cons(N,IL))	→	a__isNat#(N)	(60)
  a__isNatList#(cons(N,L))	→	a__isNat#(N)	(85)
  a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(N)	(84)
  mark#(isNatList(X))	→	a__isNatList#(X)	(83)
  mark#(uTake2(X1,X2,X3,X4))	→	a__uTake2#(mark(X1),X2,X3,X4)	(82)
  a__isNatList#(take(N,IL))	→	a__isNat#(N)	(81)
  mark#(cons(X1,X2))	→	mark#(X1)	(58)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL)))	(56)
  mark#(uLength(X1,X2))	→	mark#(X1)	(79)
  a__take#(s(M),cons(N,IL))	→	a__isNatIList#(IL)	(78)
  a__length#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(55)
  mark#(take(X1,X2))	→	mark#(X1)	(54)
  a__isNatList#(take(N,IL))	→	a__isNatIList#(IL)	(77)
  mark#(isNat(X))	→	a__isNat#(X)	(53)
  a__uLength#(tt,L)	→	mark#(L)	(76)
  mark#(and(X1,X2))	→	mark#(X2)	(52)
  a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
  a__isNat#(length(L))	→	a__isNatList#(L)	(74)
  mark#(and(X1,X2))	→	mark#(X1)	(51)
  a__uTake2#(tt,M,N,IL)	→	mark#(N)	(73)
  mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(72)
  mark#(uTake2(X1,X2,X3,X4))	→	mark#(X1)	(50)
  a__uLength#(tt,L)	→	a__length#(mark(L))	(71)
  a__length#(cons(N,L))	→	a__isNat#(N)	(49)
  a__length#(cons(N,L))	→	a__isNatList#(L)	(48)
  a__take#(0,IL)	→	a__isNatIList#(IL)	(70)
  mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
  a__length#(cons(N,L))	→	a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)	(69)
  mark#(take(X1,X2))	→	mark#(X2)	(68)
  mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
  mark#(length(X))	→	a__length#(mark(X))	(45)
  a__and#(tt,T)	→	mark#(T)	(44)
  a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)
  mark#(uTake1(X))	→	mark#(X)	(67)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [a__uLength#(x1, x2)]	=	x2 + 4684
  [a__uTake2#(x1,...,x4)]	=	x3 + 1
  [isNatList(x1)]	=	0
  [s(x1)]	=	x1 + 0
  [a__isNatIList(x1)]	=	0
  [a__isNat#(x1)]	=	0
  [take(x1, x2)]	=	x1 + x2 + 14100
  [and(x1, x2)]	=	x1 + x2 + 0
  [isNatIList(x1)]	=	0
  [zeros]	=	1
  [a__take#(x1, x2)]	=	x2 + 2
  [uTake2(x1,...,x4)]	=	x1 + x2 + x3 + x4 + 14100
  [a__isNatList(x1)]	=	0
  [a__isNatIList#(x1)]	=	0
  [uLength(x1, x2)]	=	x1 + x2 + 4685
  [mark#(x1)]	=	x1 + 0
  [a__uTake1#(x1)]	=	0
  [0]	=	0
  [a__uTake2(x1,...,x4)]	=	x1 + x2 + x3 + x4 + 14100
  [a__and#(x1, x2)]	=	x2 + 0
  [a__zeros#]	=	0
  [nil]	=	3490
  [mark(x1)]	=	x1 + 0
  [a__length#(x1)]	=	x1 + 4684
  [isNat(x1)]	=	0
  [a__uLength(x1, x2)]	=	x1 + x2 + 4685
  [a__uTake1(x1)]	=	x1 + 13214
  [a__isNatList#(x1)]	=	0
  [cons(x1, x2)]	=	x1 + x2 + 0
  [a__take(x1, x2)]	=	x1 + x2 + 14100
  [tt]	=	0
  [uTake1(x1)]	=	x1 + 13214
  [a__isNat(x1)]	=	0
  [a__and(x1, x2)]	=	x1 + x2 + 0
  [length(x1)]	=	x1 + 4685
  [a__zeros]	=	1
  [a__length(x1)]	=	x1 + 4685

  together with the usable rules

  mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
  a__isNat(s(N))	→	a__isNat(N)	(4)
  a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
  a__isNatList(nil)	→	tt	(8)
  a__and(tt,T)	→	mark(T)	(1)
  a__isNat(0)	→	tt	(3)
  a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
  mark(isNat(X))	→	a__isNat(X)	(21)
  a__isNat(X)	→	isNat(X)	(36)
  mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
  mark(isNatIList(X))	→	a__isNatIList(X)	(19)
  mark(nil)	→	nil	(32)
  a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
  mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
  a__isNatIList(X)	→	isNatIList(X)	(34)
  mark(length(X))	→	a__length(mark(X))	(22)
  mark(tt)	→	tt	(28)
  a__isNat(length(L))	→	a__isNatList(L)	(5)
  a__and(X1,X2)	→	and(X1,X2)	(33)
  a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
  a__take(X1,X2)	→	take(X1,X2)	(39)
  a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
  mark(isNatList(X))	→	a__isNatList(X)	(20)
  mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
  mark(s(X))	→	s(mark(X))	(30)
  a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
  a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
  mark(zeros)	→	a__zeros	(23)
  mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
  a__zeros	→	cons(0,zeros)	(11)
  a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
  a__uTake1(tt)	→	nil	(13)
  a__uTake1(X)	→	uTake1(X)	(40)
  a__isNatIList(zeros)	→	tt	(6)
  a__zeros	→	zeros	(38)
  a__length(X)	→	length(X)	(37)
  a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
  a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
  a__isNatList(X)	→	isNatList(X)	(35)
  mark(0)	→	0	(29)
  a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

  mark#(length(X))	→	mark#(X)	(65)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(M)	(64)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(88)
  mark#(uLength(X1,X2))	→	a__uLength#(mark(X1),X2)	(63)
  a__take#(s(M),cons(N,IL))	→	a__uTake2#(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(62)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(N)	(84)
  mark#(uTake2(X1,X2,X3,X4))	→	a__uTake2#(mark(X1),X2,X3,X4)	(82)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL)))	(56)
  mark#(uLength(X1,X2))	→	mark#(X1)	(79)
  a__take#(s(M),cons(N,IL))	→	a__isNatIList#(IL)	(78)
  a__length#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(55)
  mark#(take(X1,X2))	→	mark#(X1)	(54)
  a__uLength#(tt,L)	→	mark#(L)	(76)
  a__uTake2#(tt,M,N,IL)	→	mark#(N)	(73)
  mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(72)
  mark#(uTake2(X1,X2,X3,X4))	→	mark#(X1)	(50)
  a__length#(cons(N,L))	→	a__isNat#(N)	(49)
  a__length#(cons(N,L))	→	a__isNatList#(L)	(48)
  a__take#(0,IL)	→	a__isNatIList#(IL)	(70)
  mark#(take(X1,X2))	→	mark#(X2)	(68)
  mark#(length(X))	→	a__length#(mark(X))	(45)
  mark#(uTake1(X))	→	mark#(X)	(67)

  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__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)	(69)
    a__uLength#(tt,L)	→	a__length#(mark(L))	(71)

    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__uLength#(x1, x2)]	=	1 0 0 0 · x1 + 0 1 0 0 · x2 + 0 0
    [a__uTake2#(x1,...,x4)]	=	0 0
    [isNatList(x1)]	=	0 0 1 0 · x1 + 1 1
    [s(x1)]	=	x1 + 3 3
    [a__isNatIList(x1)]	=	1 0 1 0 · x1 + 4 4
    [a__isNat#(x1)]	=	0 0
    [take(x1, x2)]	=	0 0 0 1 · x1 + x2 + 3 3
    [and(x1, x2)]	=	0 0 0 1 · x2 + 1 0
    [isNatIList(x1)]	=	0 0 1 0 · x1 + 1 4
    [zeros]	=	0 43642
    [a__take#(x1, x2)]	=	0 0
    [uTake2(x1,...,x4)]	=	0 0 0 1 · x2 + 0 0 1 1 · x4 + 1 6
    [a__isNatList(x1)]	=	1 0 1 0 · x1 + 2 1
    [a__isNatIList#(x1)]	=	0 0
    [uLength(x1, x2)]	=	0 0 0 1 · x1 + 0 0 0 1 · x2 + 1 26150
    [mark#(x1)]	=	0 0
    [a__uTake1#(x1)]	=	0 0
    [0]	=	2 1
    [a__uTake2(x1,...,x4)]	=	0 1 0 1 · x2 + 1 1 1 1 · x4 + 7 6
    [a__and#(x1, x2)]	=	0 0
    [a__zeros#]	=	0 0
    [nil]	=	3 2
    [mark(x1)]	=	0 1 0 1 · x1 + 1 0
    [a__length#(x1)]	=	1 0 0 0 · x1 + 2 0
    [isNat(x1)]	=	0 0 1 1 · x1 + 1 1
    [a__uLength(x1, x2)]	=	0 1 0 1 · x1 + 0 1 0 1 · x2 + 9292 26150
    [a__uTake1(x1)]	=	3 2
    [a__isNatList#(x1)]	=	0 0
    [cons(x1, x2)]	=	1 1 1 1 · x2 + 1 0
    [a__take(x1, x2)]	=	0 1 0 1 · x1 + x2 + 3 3
    [tt]	=	4 4
    [uTake1(x1)]	=	1 2
    [a__isNat(x1)]	=	1 0 1 1 · x1 + 2 1
    [a__and(x1, x2)]	=	0 1 0 1 · x2 + 1 0
    [length(x1)]	=	x1 + 9292 26151
    [a__zeros]	=	43643 43642
    [a__length(x1)]	=	x1 + 9292 26151

    together with the usable rules

    mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
    a__isNat(s(N))	→	a__isNat(N)	(4)
    a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
    a__isNatList(nil)	→	tt	(8)
    a__and(tt,T)	→	mark(T)	(1)
    a__isNat(0)	→	tt	(3)
    a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
    mark(isNat(X))	→	a__isNat(X)	(21)
    a__isNat(X)	→	isNat(X)	(36)
    mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
    mark(isNatIList(X))	→	a__isNatIList(X)	(19)
    mark(nil)	→	nil	(32)
    a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
    mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
    a__isNatIList(X)	→	isNatIList(X)	(34)
    mark(length(X))	→	a__length(mark(X))	(22)
    mark(tt)	→	tt	(28)
    a__isNat(length(L))	→	a__isNatList(L)	(5)
    a__and(X1,X2)	→	and(X1,X2)	(33)
    a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
    a__take(X1,X2)	→	take(X1,X2)	(39)
    a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
    mark(isNatList(X))	→	a__isNatList(X)	(20)
    mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
    mark(s(X))	→	s(mark(X))	(30)
    a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
    a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
    mark(zeros)	→	a__zeros	(23)
    mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
    a__zeros	→	cons(0,zeros)	(11)
    a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
    a__uTake1(tt)	→	nil	(13)
    a__uTake1(X)	→	uTake1(X)	(40)
    a__isNatIList(zeros)	→	tt	(6)
    a__zeros	→	zeros	(38)
    a__length(X)	→	length(X)	(37)
    a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
    a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
    a__isNatList(X)	→	isNatList(X)	(35)
    mark(0)	→	0	(29)
    a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

    a__length#(cons(N,L))	→	a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)	(69)
    a__uLength#(tt,L)	→	a__length#(mark(L))	(71)

    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#(and(X1,X2))	→	mark#(X2)	(52)
    mark#(and(X1,X2))	→	mark#(X1)	(51)
    mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
    a__isNat#(s(N))	→	a__isNat#(N)	(61)
    a__and#(tt,T)	→	mark#(T)	(44)
    mark#(isNat(X))	→	a__isNat#(X)	(53)
    mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
    a__isNat#(length(L))	→	a__isNatList#(L)	(74)
    a__isNatList#(take(N,IL))	→	a__isNatIList#(IL)	(77)
    a__isNatList#(take(N,IL))	→	a__isNat#(N)	(81)
    a__isNatList#(take(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(66)
    a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
    a__isNatIList#(cons(N,IL))	→	a__isNat#(N)	(60)
    a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
    mark#(isNatList(X))	→	a__isNatList#(X)	(83)
    mark#(s(X))	→	mark#(X)	(90)
    mark#(cons(X1,X2))	→	mark#(X1)	(58)
    a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
    a__isNatList#(cons(N,L))	→	a__isNat#(N)	(85)
    a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)
    a__isNatIList#(IL)	→	a__isNatList#(IL)	(86)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [a__uLength#(x1, x2)]	=	4684
    [a__uTake2#(x1,...,x4)]	=	1
    [isNatList(x1)]	=	x1 + 11176
    [s(x1)]	=	x1 + 0
    [a__isNatIList(x1)]	=	x1 + 11177
    [a__isNat#(x1)]	=	x1 + 0
    [take(x1, x2)]	=	x1 + x2 + 37005
    [and(x1, x2)]	=	x1 + x2 + 0
    [isNatIList(x1)]	=	x1 + 11177
    [zeros]	=	24376
    [a__take#(x1, x2)]	=	2
    [uTake2(x1,...,x4)]	=	x2 + x3 + x4 + 37005
    [a__isNatList(x1)]	=	x1 + 11176
    [a__isNatIList#(x1)]	=	x1 + 11178
    [uLength(x1, x2)]	=	x2 + 11178
    [mark#(x1)]	=	x1 + 1
    [a__uTake1#(x1)]	=	0
    [0]	=	0
    [a__uTake2(x1,...,x4)]	=	x2 + x3 + x4 + 37005
    [a__and#(x1, x2)]	=	x2 + 1
    [a__zeros#]	=	0
    [nil]	=	25828
    [mark(x1)]	=	x1 + 0
    [a__length#(x1)]	=	4684
    [isNat(x1)]	=	x1 + 0
    [a__uLength(x1, x2)]	=	x2 + 11178
    [a__uTake1(x1)]	=	x1 + 25828
    [a__isNatList#(x1)]	=	x1 + 11177
    [cons(x1, x2)]	=	x1 + x2 + 0
    [a__take(x1, x2)]	=	x1 + x2 + 37005
    [tt]	=	0
    [uTake1(x1)]	=	x1 + 25828
    [a__isNat(x1)]	=	x1 + 0
    [a__and(x1, x2)]	=	x1 + x2 + 0
    [length(x1)]	=	x1 + 11178
    [a__zeros]	=	24376
    [a__length(x1)]	=	x1 + 11178

    together with the usable rules

    mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
    a__isNat(s(N))	→	a__isNat(N)	(4)
    a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
    a__isNatList(nil)	→	tt	(8)
    a__and(tt,T)	→	mark(T)	(1)
    a__isNat(0)	→	tt	(3)
    a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
    mark(isNat(X))	→	a__isNat(X)	(21)
    a__isNat(X)	→	isNat(X)	(36)
    mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
    mark(isNatIList(X))	→	a__isNatIList(X)	(19)
    mark(nil)	→	nil	(32)
    a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
    mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
    a__isNatIList(X)	→	isNatIList(X)	(34)
    mark(length(X))	→	a__length(mark(X))	(22)
    mark(tt)	→	tt	(28)
    a__isNat(length(L))	→	a__isNatList(L)	(5)
    a__and(X1,X2)	→	and(X1,X2)	(33)
    a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
    a__take(X1,X2)	→	take(X1,X2)	(39)
    a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
    mark(isNatList(X))	→	a__isNatList(X)	(20)
    mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
    mark(s(X))	→	s(mark(X))	(30)
    a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
    a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
    mark(zeros)	→	a__zeros	(23)
    mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
    a__zeros	→	cons(0,zeros)	(11)
    a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
    a__uTake1(tt)	→	nil	(13)
    a__uTake1(X)	→	uTake1(X)	(40)
    a__isNatIList(zeros)	→	tt	(6)
    a__zeros	→	zeros	(38)
    a__length(X)	→	length(X)	(37)
    a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
    a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
    a__isNatList(X)	→	isNatList(X)	(35)
    mark(0)	→	0	(29)
    a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

    mark#(isNat(X))	→	a__isNat#(X)	(53)
    a__isNat#(length(L))	→	a__isNatList#(L)	(74)
    a__isNatList#(take(N,IL))	→	a__isNatIList#(IL)	(77)
    a__isNatList#(take(N,IL))	→	a__isNat#(N)	(81)
    a__isNatList#(take(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(66)
    a__isNatIList#(cons(N,IL))	→	a__isNat#(N)	(60)
    a__isNatList#(cons(N,L))	→	a__isNat#(N)	(85)
    a__isNatIList#(IL)	→	a__isNatList#(IL)	(86)

    could be deleted.

    1.1.1.1.2.1 Dependency Graph Processor

    The dependency pairs are split into 2 components.

    • The 1^st component contains the pair

      a__isNat#(s(N))

      →

      a__isNat#(N)

      (61)

      1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [a__uLength#(x1, x2)]	=	4684
      [a__uTake2#(x1,...,x4)]	=	1
      [isNatList(x1)]	=	8
      [s(x1)]	=	x1 + 1
      [a__isNatIList(x1)]	=	6
      [a__isNat#(x1)]	=	x1 + 0
      [take(x1, x2)]	=	x1 + x2 + 1
      [and(x1, x2)]	=	4
      [isNatIList(x1)]	=	x1 + 1
      [zeros]	=	24376
      [a__take#(x1, x2)]	=	2
      [uTake2(x1,...,x4)]	=	x1 + x2 + x4 + 3
      [a__isNatList(x1)]	=	x1 + 7
      [a__isNatIList#(x1)]	=	11178
      [uLength(x1, x2)]	=	45632
      [mark#(x1)]	=	1
      [a__uTake1#(x1)]	=	0
      [0]	=	1
      [a__uTake2(x1,...,x4)]	=	x2 + x3 + 2
      [a__and#(x1, x2)]	=	1
      [a__zeros#]	=	0
      [nil]	=	7
      [mark(x1)]	=	x1 + 4
      [a__length#(x1)]	=	4684
      [isNat(x1)]	=	2
      [a__uLength(x1, x2)]	=	x1 + 45633
      [a__uTake1(x1)]	=	6
      [a__isNatList#(x1)]	=	11177
      [cons(x1, x2)]	=	x1 + 1
      [a__take(x1, x2)]	=	x2 + 0
      [tt]	=	15
      [uTake1(x1)]	=	x1 + 1
      [a__isNat(x1)]	=	x1 + 1
      [a__and(x1, x2)]	=	x2 + 3
      [length(x1)]	=	2
      [a__zeros]	=	24375
      [a__length(x1)]	=	45643

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

      a__isNat#(s(N))

      →

      a__isNat#(N)

      (61)

      could be deleted.

      1.1.1.1.2.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.

    • The 2^nd component contains the pair

      mark#(and(X1,X2))	→	mark#(X2)	(52)
      mark#(and(X1,X2))	→	mark#(X1)	(51)
      mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
      a__and#(tt,T)	→	mark#(T)	(44)
      mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
      a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
      a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
      mark#(isNatList(X))	→	a__isNatList#(X)	(83)
      mark#(s(X))	→	mark#(X)	(90)
      mark#(cons(X1,X2))	→	mark#(X1)	(58)
      a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
      a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)

      1.1.1.1.2.1.2 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [a__uLength#(x1, x2)]	=	4684
      [a__uTake2#(x1,...,x4)]	=	1
      [isNatList(x1)]	=	0
      [s(x1)]	=	x1 + 0
      [a__isNatIList(x1)]	=	0
      [a__isNat#(x1)]	=	0
      [take(x1, x2)]	=	x2 + 1
      [and(x1, x2)]	=	x1 + x2 + 0
      [isNatIList(x1)]	=	0
      [zeros]	=	20362
      [a__take#(x1, x2)]	=	2
      [uTake2(x1,...,x4)]	=	x3 + 1
      [a__isNatList(x1)]	=	0
      [a__isNatIList#(x1)]	=	1
      [uLength(x1, x2)]	=	45962
      [mark#(x1)]	=	x1 + 1
      [a__uTake1#(x1)]	=	0
      [0]	=	20361
      [a__uTake2(x1,...,x4)]	=	x3 + 1
      [a__and#(x1, x2)]	=	x2 + 1
      [a__zeros#]	=	0
      [nil]	=	1
      [mark(x1)]	=	x1 + 0
      [a__length#(x1)]	=	4684
      [isNat(x1)]	=	0
      [a__uLength(x1, x2)]	=	45962
      [a__uTake1(x1)]	=	1
      [a__isNatList#(x1)]	=	1
      [cons(x1, x2)]	=	x1 + 1
      [a__take(x1, x2)]	=	x2 + 1
      [tt]	=	0
      [uTake1(x1)]	=	1
      [a__isNat(x1)]	=	0
      [a__and(x1, x2)]	=	x1 + x2 + 0
      [length(x1)]	=	45962
      [a__zeros]	=	20362
      [a__length(x1)]	=	45962

      together with the usable rules

      mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
      a__isNat(s(N))	→	a__isNat(N)	(4)
      a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
      a__isNatList(nil)	→	tt	(8)
      a__and(tt,T)	→	mark(T)	(1)
      a__isNat(0)	→	tt	(3)
      a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
      mark(isNat(X))	→	a__isNat(X)	(21)
      a__isNat(X)	→	isNat(X)	(36)
      mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
      mark(isNatIList(X))	→	a__isNatIList(X)	(19)
      mark(nil)	→	nil	(32)
      a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
      mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
      a__isNatIList(X)	→	isNatIList(X)	(34)
      mark(length(X))	→	a__length(mark(X))	(22)
      mark(tt)	→	tt	(28)
      a__isNat(length(L))	→	a__isNatList(L)	(5)
      a__and(X1,X2)	→	and(X1,X2)	(33)
      a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
      a__take(X1,X2)	→	take(X1,X2)	(39)
      a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
      mark(isNatList(X))	→	a__isNatList(X)	(20)
      mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
      mark(s(X))	→	s(mark(X))	(30)
      a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
      a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
      mark(zeros)	→	a__zeros	(23)
      mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
      a__zeros	→	cons(0,zeros)	(11)
      a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
      a__uTake1(tt)	→	nil	(13)
      a__uTake1(X)	→	uTake1(X)	(40)
      a__isNatIList(zeros)	→	tt	(6)
      a__zeros	→	zeros	(38)
      a__length(X)	→	length(X)	(37)
      a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
      a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
      a__isNatList(X)	→	isNatList(X)	(35)
      mark(0)	→	0	(29)
      a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

      mark#(cons(X1,X2))

      →

      mark#(X1)

      (58)

      could be deleted.

      1.1.1.1.2.1.2.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        mark#(and(X1,X2))	→	mark#(X2)	(52)
        mark#(and(X1,X2))	→	mark#(X1)	(51)
        mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
        a__and#(tt,T)	→	mark#(T)	(44)
        mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
        a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
        a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
        mark#(isNatList(X))	→	a__isNatList#(X)	(83)
        mark#(s(X))	→	mark#(X)	(90)
        a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
        a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)

        1.1.1.1.2.1.2.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [a__uLength#(x1, x2)]	=	max(0)
        [a__uTake2#(x1,...,x4)]	=	max(0)
        [isNatList(x1)]	=	x1 + 1
        [s(x1)]	=	x1 + 0
        [a__isNatIList(x1)]	=	x1 + 1
        [a__isNat#(x1)]	=	0
        [take(x1, x2)]	=	max(x1 + 16708, x2 + 1, 0)
        [and(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
        [isNatIList(x1)]	=	x1 + 1
        [zeros]	=	59345
        [a__take#(x1, x2)]	=	max(0)
        [uTake2(x1,...,x4)]	=	max(x2 + 16708, x3 + 16709, x4 + 1, 0)
        [a__isNatList(x1)]	=	x1 + 1
        [a__isNatIList#(x1)]	=	x1 + 4
        [uLength(x1, x2)]	=	max(x1 + 1, x2 + 15946, 0)
        [mark#(x1)]	=	x1 + 3
        [a__uTake1#(x1)]	=	0
        [0]	=	42636
        [a__uTake2(x1,...,x4)]	=	max(x2 + 16708, x3 + 16709, x4 + 1, 0)
        [a__and#(x1, x2)]	=	max(x1 + 0, x2 + 3, 0)
        [a__zeros#]	=	0
        [nil]	=	1
        [mark(x1)]	=	x1 + 0
        [a__length#(x1)]	=	1
        [isNat(x1)]	=	x1 + 16708
        [a__uLength(x1, x2)]	=	max(x1 + 1, x2 + 15946, 0)
        [a__uTake1(x1)]	=	1
        [a__isNatList#(x1)]	=	x1 + 4
        [cons(x1, x2)]	=	max(x1 + 16709, x2 + 0, 0)
        [a__take(x1, x2)]	=	max(x1 + 16708, x2 + 1, 0)
        [tt]	=	2
        [uTake1(x1)]	=	1
        [a__isNat(x1)]	=	x1 + 16708
        [a__and(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
        [length(x1)]	=	x1 + 15946
        [a__zeros]	=	59345
        [a__length(x1)]	=	x1 + 15946

        together with the usable rules

        mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
        a__isNat(s(N))	→	a__isNat(N)	(4)
        a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
        a__isNatList(nil)	→	tt	(8)
        a__and(tt,T)	→	mark(T)	(1)
        a__isNat(0)	→	tt	(3)
        a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
        mark(isNat(X))	→	a__isNat(X)	(21)
        a__isNat(X)	→	isNat(X)	(36)
        mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
        mark(isNatIList(X))	→	a__isNatIList(X)	(19)
        mark(nil)	→	nil	(32)
        a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
        mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
        a__isNatIList(X)	→	isNatIList(X)	(34)
        mark(length(X))	→	a__length(mark(X))	(22)
        mark(tt)	→	tt	(28)
        a__isNat(length(L))	→	a__isNatList(L)	(5)
        a__and(X1,X2)	→	and(X1,X2)	(33)
        a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
        a__take(X1,X2)	→	take(X1,X2)	(39)
        a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
        mark(isNatList(X))	→	a__isNatList(X)	(20)
        mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
        mark(s(X))	→	s(mark(X))	(30)
        a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
        a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
        mark(zeros)	→	a__zeros	(23)
        mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
        a__zeros	→	cons(0,zeros)	(11)
        a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
        a__uTake1(tt)	→	nil	(13)
        a__uTake1(X)	→	uTake1(X)	(40)
        a__isNatIList(zeros)	→	tt	(6)
        a__zeros	→	zeros	(38)
        a__length(X)	→	length(X)	(37)
        a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
        a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
        a__isNatList(X)	→	isNatList(X)	(35)
        mark(0)	→	0	(29)
        a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

        mark#(and(X1,X2))

        →

        mark#(X1)

        (51)

        could be deleted.

        1.1.1.1.2.1.2.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          mark#(and(X1,X2))	→	mark#(X2)	(52)
          mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
          a__and#(tt,T)	→	mark#(T)	(44)
          mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
          a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
          a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
          mark#(isNatList(X))	→	a__isNatList#(X)	(83)
          mark#(s(X))	→	mark#(X)	(90)
          a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
          a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)

          1.1.1.1.2.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the Max-polynomial interpretation

          [a__uLength#(x1, x2)]	=	4684
          [a__uTake2#(x1,...,x4)]	=	1
          [isNatList(x1)]	=	x1 + 1
          [s(x1)]	=	x1 + 0
          [a__isNatIList(x1)]	=	x1 + 1
          [a__isNat#(x1)]	=	0
          [take(x1, x2)]	=	x2 + 2
          [and(x1, x2)]	=	x2 + 2
          [isNatIList(x1)]	=	x1 + 1
          [zeros]	=	41955
          [a__take#(x1, x2)]	=	2
          [uTake2(x1,...,x4)]	=	x4 + 3
          [a__isNatList(x1)]	=	x1 + 1
          [a__isNatIList#(x1)]	=	x1 + 0
          [uLength(x1, x2)]	=	x2 + 31590
          [mark#(x1)]	=	x1 + 0
          [a__uTake1#(x1)]	=	0
          [0]	=	46914
          [a__uTake2(x1,...,x4)]	=	x4 + 4
          [a__and#(x1, x2)]	=	x2 + 0
          [a__zeros#]	=	0
          [nil]	=	4
          [mark(x1)]	=	x1 + 2
          [a__length#(x1)]	=	4684
          [isNat(x1)]	=	x1 + 44279
          [a__uLength(x1, x2)]	=	x2 + 31590
          [a__uTake1(x1)]	=	x1 + 1
          [a__isNatList#(x1)]	=	x1 + 0
          [cons(x1, x2)]	=	x2 + 2
          [a__take(x1, x2)]	=	x2 + 2
          [tt]	=	3
          [uTake1(x1)]	=	x1 + 1
          [a__isNat(x1)]	=	x1 + 44281
          [a__and(x1, x2)]	=	x2 + 2
          [length(x1)]	=	x1 + 31588
          [a__zeros]	=	41957
          [a__length(x1)]	=	x1 + 31588

          together with the usable rules

          mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
          a__isNat(s(N))	→	a__isNat(N)	(4)
          a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
          a__isNatList(nil)	→	tt	(8)
          a__and(tt,T)	→	mark(T)	(1)
          a__isNat(0)	→	tt	(3)
          a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
          mark(isNat(X))	→	a__isNat(X)	(21)
          a__isNat(X)	→	isNat(X)	(36)
          mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
          mark(isNatIList(X))	→	a__isNatIList(X)	(19)
          mark(nil)	→	nil	(32)
          a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
          mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
          a__isNatIList(X)	→	isNatIList(X)	(34)
          mark(length(X))	→	a__length(mark(X))	(22)
          mark(tt)	→	tt	(28)
          a__isNat(length(L))	→	a__isNatList(L)	(5)
          a__and(X1,X2)	→	and(X1,X2)	(33)
          a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
          a__take(X1,X2)	→	take(X1,X2)	(39)
          a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
          mark(isNatList(X))	→	a__isNatList(X)	(20)
          mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
          mark(s(X))	→	s(mark(X))	(30)
          a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
          mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
          a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
          mark(zeros)	→	a__zeros	(23)
          mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
          a__zeros	→	cons(0,zeros)	(11)
          a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
          a__uTake1(tt)	→	nil	(13)
          a__uTake1(X)	→	uTake1(X)	(40)
          a__isNatIList(zeros)	→	tt	(6)
          a__zeros	→	zeros	(38)
          a__length(X)	→	length(X)	(37)
          a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
          a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
          a__isNatList(X)	→	isNatList(X)	(35)
          mark(0)	→	0	(29)
          a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

          mark#(and(X1,X2))	→	mark#(X2)	(52)
          mark#(isNatIList(X))	→	a__isNatIList#(X)	(46)
          a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(59)
          a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(75)
          mark#(isNatList(X))	→	a__isNatList#(X)	(83)
          a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(89)
          a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(43)

          could be deleted.

          1.1.1.1.2.1.2.1.1.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 1 component.

          • The 1^st component contains the pair

            mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(47)
            a__and#(tt,T)	→	mark#(T)	(44)
            mark#(s(X))	→	mark#(X)	(90)

            1.1.1.1.2.1.2.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

            Using the argument filter

            π(a__uLength#)	=	1
            π(s)	=	1
            π(mark#)	=	1
            π(a__and#)	=	2
            π(a__length#)	=	1

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

            prec(a__uTake2#)	=	0		status(a__uTake2#)	=	[1, 4]		list-extension(a__uTake2#)	=	Lex
            prec(isNatList)	=	8		status(isNatList)	=	[1]		list-extension(isNatList)	=	Lex
            prec(a__isNatIList)	=	9		status(a__isNatIList)	=	[1]		list-extension(a__isNatIList)	=	Lex
            prec(a__isNat#)	=	0		status(a__isNat#)	=	[]		list-extension(a__isNat#)	=	Lex
            prec(take)	=	2		status(take)	=	[]		list-extension(take)	=	Lex
            prec(and)	=	6		status(and)	=	[2, 1]		list-extension(and)	=	Lex
            prec(isNatIList)	=	9		status(isNatIList)	=	[1]		list-extension(isNatIList)	=	Lex
            prec(zeros)	=	3		status(zeros)	=	[]		list-extension(zeros)	=	Lex
            prec(a__take#)	=	0		status(a__take#)	=	[1, 2]		list-extension(a__take#)	=	Lex
            prec(uTake2)	=	2		status(uTake2)	=	[3, 4, 2]		list-extension(uTake2)	=	Lex
            prec(a__isNatList)	=	8		status(a__isNatList)	=	[1]		list-extension(a__isNatList)	=	Lex
            prec(a__isNatIList#)	=	0		status(a__isNatIList#)	=	[]		list-extension(a__isNatIList#)	=	Lex
            prec(uLength)	=	9		status(uLength)	=	[]		list-extension(uLength)	=	Lex
            prec(a__uTake1#)	=	0		status(a__uTake1#)	=	[]		list-extension(a__uTake1#)	=	Lex
            prec(0)	=	5		status(0)	=	[]		list-extension(0)	=	Lex
            prec(a__uTake2)	=	3		status(a__uTake2)	=	[]		list-extension(a__uTake2)	=	Lex
            prec(a__zeros#)	=	0		status(a__zeros#)	=	[]		list-extension(a__zeros#)	=	Lex
            prec(nil)	=	5		status(nil)	=	[]		list-extension(nil)	=	Lex
            prec(mark)	=	6		status(mark)	=	[1]		list-extension(mark)	=	Lex
            prec(isNat)	=	0		status(isNat)	=	[]		list-extension(isNat)	=	Lex
            prec(a__uLength)	=	9		status(a__uLength)	=	[]		list-extension(a__uLength)	=	Lex
            prec(a__uTake1)	=	5		status(a__uTake1)	=	[]		list-extension(a__uTake1)	=	Lex
            prec(a__isNatList#)	=	0		status(a__isNatList#)	=	[]		list-extension(a__isNatList#)	=	Lex
            prec(cons)	=	2		status(cons)	=	[1, 2]		list-extension(cons)	=	Lex
            prec(a__take)	=	4		status(a__take)	=	[]		list-extension(a__take)	=	Lex
            prec(tt)	=	7		status(tt)	=	[]		list-extension(tt)	=	Lex
            prec(uTake1)	=	5		status(uTake1)	=	[]		list-extension(uTake1)	=	Lex
            prec(a__isNat)	=	1		status(a__isNat)	=	[]		list-extension(a__isNat)	=	Lex
            prec(a__and)	=	6		status(a__and)	=	[2, 1]		list-extension(a__and)	=	Lex
            prec(length)	=	9		status(length)	=	[]		list-extension(length)	=	Lex
            prec(a__zeros)	=	4		status(a__zeros)	=	[]		list-extension(a__zeros)	=	Lex
            prec(a__length)	=	9		status(a__length)	=	[]		list-extension(a__length)	=	Lex

            and the following Max-polynomial interpretation

            [a__uTake2#(x1,...,x4)]	=	x1 + x4 + 1
            [isNatList(x1)]	=	x1 + 41355
            [a__isNatIList(x1)]	=	x1 + 41356
            [a__isNat#(x1)]	=	1
            [take(x1, x2)]	=	max(x1 + 15622, x2 + 2, 0)
            [and(x1, x2)]	=	max(x1 + 25728, x2 + 0, 0)
            [isNatIList(x1)]	=	x1 + 41356
            [zeros]	=	82707
            [a__take#(x1, x2)]	=	x1 + x2 + 1
            [uTake2(x1,...,x4)]	=	max(x2 + 15622, x3 + 41353, x4 + 2, 0)
            [a__isNatList(x1)]	=	x1 + 41355
            [a__isNatIList#(x1)]	=	1
            [uLength(x1, x2)]	=	max(x2 + 41354, 0)
            [a__uTake1#(x1)]	=	1
            [0]	=	41354
            [a__uTake2(x1,...,x4)]	=	max(x2 + 15622, x3 + 41353, x4 + 2, 0)
            [a__zeros#]	=	0
            [nil]	=	1
            [mark(x1)]	=	x1 + 0
            [isNat(x1)]	=	x1 + 15623
            [a__uLength(x1, x2)]	=	max(x2 + 41354, 0)
            [a__uTake1(x1)]	=	1
            [a__isNatList#(x1)]	=	1
            [cons(x1, x2)]	=	max(x1 + 41352, x2 + 0, 0)
            [a__take(x1, x2)]	=	max(x1 + 15622, x2 + 2, 0)
            [tt]	=	41353
            [uTake1(x1)]	=	1
            [a__isNat(x1)]	=	x1 + 15623
            [a__and(x1, x2)]	=	max(x1 + 25728, x2 + 0, 0)
            [length(x1)]	=	x1 + 41354
            [a__zeros]	=	82707
            [a__length(x1)]	=	x1 + 41354

            together with the usable rules

            mark(and(X1,X2))	→	a__and(mark(X1),mark(X2))	(18)
            a__isNat(s(N))	→	a__isNat(N)	(4)
            a__uTake2(tt,M,N,IL)	→	cons(mark(N),take(M,IL))	(15)
            a__isNatList(nil)	→	tt	(8)
            a__and(tt,T)	→	mark(T)	(1)
            a__isNat(0)	→	tt	(3)
            a__length(cons(N,L))	→	a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)	(16)
            mark(isNat(X))	→	a__isNat(X)	(21)
            a__isNat(X)	→	isNat(X)	(36)
            mark(uTake2(X1,X2,X3,X4))	→	a__uTake2(mark(X1),X2,X3,X4)	(26)
            mark(isNatIList(X))	→	a__isNatIList(X)	(19)
            mark(nil)	→	nil	(32)
            a__uLength(tt,L)	→	s(a__length(mark(L)))	(17)
            mark(uLength(X1,X2))	→	a__uLength(mark(X1),X2)	(27)
            a__isNatIList(X)	→	isNatIList(X)	(34)
            mark(length(X))	→	a__length(mark(X))	(22)
            mark(tt)	→	tt	(28)
            a__isNat(length(L))	→	a__isNatList(L)	(5)
            a__and(X1,X2)	→	and(X1,X2)	(33)
            a__isNatList(take(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(10)
            a__take(X1,X2)	→	take(X1,X2)	(39)
            a__isNatIList(cons(N,IL))	→	a__and(a__isNat(N),a__isNatIList(IL))	(7)
            mark(isNatList(X))	→	a__isNatList(X)	(20)
            mark(uTake1(X))	→	a__uTake1(mark(X))	(25)
            mark(s(X))	→	s(mark(X))	(30)
            a__take(s(M),cons(N,IL))	→	a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)	(14)
            mark(cons(X1,X2))	→	cons(mark(X1),X2)	(31)
            a__take(0,IL)	→	a__uTake1(a__isNatIList(IL))	(12)
            mark(zeros)	→	a__zeros	(23)
            mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(24)
            a__zeros	→	cons(0,zeros)	(11)
            a__isNatList(cons(N,L))	→	a__and(a__isNat(N),a__isNatList(L))	(9)
            a__uTake1(tt)	→	nil	(13)
            a__uTake1(X)	→	uTake1(X)	(40)
            a__isNatIList(zeros)	→	tt	(6)
            a__zeros	→	zeros	(38)
            a__length(X)	→	length(X)	(37)
            a__uTake2(X1,X2,X3,X4)	→	uTake2(X1,X2,X3,X4)	(41)
            a__uLength(X1,X2)	→	uLength(X1,X2)	(42)
            a__isNatList(X)	→	isNatList(X)	(35)
            mark(0)	→	0	(29)
            a__isNatIList(IL)	→	a__isNatList(IL)	(2)

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

            mark#(and(X1,X2))

            →

            a__and#(mark(X1),mark(X2))

            (47)

            could be deleted.

            1.1.1.1.2.1.2.1.1.1.1.1.1.1 Dependency Graph Processor

            The dependency pairs are split into 1 component.

            • The 1^st component contains the pair

              mark#(s(X))

              →

              mark#(X)

              (90)

              1.1.1.1.2.1.2.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

              Using the Max-polynomial interpretation

              [a__uLength#(x1, x2)]	=	4684
              [a__uTake2#(x1,...,x4)]	=	1
              [isNatList(x1)]	=	8139
              [s(x1)]	=	x1 + 2
              [a__isNatIList(x1)]	=	8137
              [a__isNat#(x1)]	=	0
              [take(x1, x2)]	=	8138
              [and(x1, x2)]	=	8140
              [isNatIList(x1)]	=	8138
              [zeros]	=	8138
              [a__take#(x1, x2)]	=	2
              [uTake2(x1,...,x4)]	=	x1 + 8139
              [a__isNatList(x1)]	=	8138
              [a__isNatIList#(x1)]	=	0
              [uLength(x1, x2)]	=	x1 + 8139
              [mark#(x1)]	=	x1 + 1
              [a__uTake1#(x1)]	=	0
              [0]	=	8137
              [a__uTake2(x1,...,x4)]	=	x2 + x3 + x4 + 8138
              [a__and#(x1, x2)]	=	0
              [a__zeros#]	=	0
              [nil]	=	8141
              [mark(x1)]	=	8136
              [a__length#(x1)]	=	4684
              [isNat(x1)]	=	x1 + 8138
              [a__uLength(x1, x2)]	=	8138
              [a__uTake1(x1)]	=	x1 + 1
              [a__isNatList#(x1)]	=	0
              [cons(x1, x2)]	=	8139
              [a__take(x1, x2)]	=	8137
              [tt]	=	8139
              [uTake1(x1)]	=	x1 + 2
              [a__isNat(x1)]	=	8137
              [a__and(x1, x2)]	=	8139
              [length(x1)]	=	8138
              [a__zeros]	=	8137
              [a__length(x1)]	=	8137

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

              mark#(s(X))

              →

              mark#(X)

              (90)

              could be deleted.

              1.1.1.1.2.1.2.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

              The dependency pairs are split into 0 components.