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

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  a__length#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(66)
  a__length#(cons(N,L))	→	a__isNat#(N)	(67)
  a__length#(cons(N,L))	→	a__isNatList#(L)	(68)
  a__uLength#(tt,L)	→	mark#(L)	(70)
  mark#(length(X))	→	mark#(X)	(78)
  mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(80)
  a__take#(0,IL)	→	a__isNatIList#(IL)	(57)
  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)	(58)
  mark#(take(X1,X2))	→	mark#(X1)	(81)
  mark#(take(X1,X2))	→	mark#(X2)	(82)
  mark#(uTake2(X1,X2,X3,X4))	→	a__uTake2#(mark(X1),X2,X3,X4)	(85)
  mark#(uTake2(X1,X2,X3,X4))	→	mark#(X1)	(86)
  mark#(uLength(X1,X2))	→	mark#(X1)	(88)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL)))	(59)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(M)	(60)
  a__take#(s(M),cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(61)
  a__take#(s(M),cons(N,IL))	→	a__isNat#(N)	(62)
  a__take#(s(M),cons(N,IL))	→	a__isNatIList#(IL)	(63)

  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__and#(tt,T)	→	mark#(T)	(43)
    mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(71)
    mark#(and(X1,X2))	→	mark#(X1)	(72)
    mark#(and(X1,X2))	→	mark#(X2)	(73)
    mark#(isNatIList(X))	→	a__isNatIList#(X)	(74)
    a__isNatIList#(IL)	→	a__isNatList#(IL)	(44)
    a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(50)
    a__isNatList#(cons(N,L))	→	a__isNat#(N)	(51)
    a__isNat#(s(N))	→	a__isNat#(N)	(45)
    a__isNat#(length(L))	→	a__isNatList#(L)	(46)
    a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(52)
    a__isNatList#(take(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(53)
    a__isNatList#(take(N,IL))	→	a__isNat#(N)	(54)
    a__isNatList#(take(N,IL))	→	a__isNatIList#(IL)	(55)
    a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(47)
    a__isNatIList#(cons(N,IL))	→	a__isNat#(N)	(48)
    a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(49)
    mark#(isNatList(X))	→	a__isNatList#(X)	(75)
    mark#(isNat(X))	→	a__isNat#(X)	(76)
    mark#(uTake1(X))	→	mark#(X)	(84)
    mark#(s(X))	→	mark#(X)	(89)
    mark#(cons(X1,X2))	→	mark#(X1)	(90)

    1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

    mark#(cons(X1,X2))

    →

    mark#(X1)

    (90)

    could be deleted.

    1.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

    mark#(uTake1(X))

    →

    mark#(X)

    (84)

    could be deleted.

    1.1.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pairs

    a__isNatList#(take(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(53)
    a__isNatList#(take(N,IL))	→	a__isNat#(N)	(54)
    a__isNatList#(take(N,IL))	→	a__isNatIList#(IL)	(55)

    could be deleted.

    1.1.1.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

    a__isNat#(length(L))

    →

    a__isNatList#(L)

    (46)

    could be deleted.

    1.1.1.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#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(71)
      a__and#(tt,T)	→	mark#(T)	(43)
      mark#(and(X1,X2))	→	mark#(X1)	(72)
      mark#(and(X1,X2))	→	mark#(X2)	(73)
      mark#(isNatIList(X))	→	a__isNatIList#(X)	(74)
      a__isNatIList#(IL)	→	a__isNatList#(IL)	(44)
      a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(50)
      a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(52)
      a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(47)
      a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(49)
      mark#(isNatList(X))	→	a__isNatList#(X)	(75)
      mark#(s(X))	→	mark#(X)	(89)

      1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

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

      the pair

      a__isNatIList#(IL)

      →

      a__isNatList#(IL)

      (44)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

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

      the pair

      mark#(and(X1,X2))

      →

      mark#(X1)

      (72)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

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

      the pairs

      mark#(and(X1,X2))	→	mark#(X2)	(73)
      a__isNatList#(cons(N,L))	→	a__and#(a__isNat(N),a__isNatList(L))	(50)
      a__isNatList#(cons(N,L))	→	a__isNatList#(L)	(52)
      a__isNatIList#(cons(N,IL))	→	a__and#(a__isNat(N),a__isNatIList(IL))	(47)
      a__isNatIList#(cons(N,IL))	→	a__isNatIList#(IL)	(49)

      could be deleted.

      1.1.1.1.1.1.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

        a__and#(tt,T)	→	mark#(T)	(43)
        mark#(and(X1,X2))	→	a__and#(mark(X1),mark(X2))	(71)
        mark#(s(X))	→	mark#(X)	(89)

        1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

        Using the linear polynomial interpretation over the naturals

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

        the pair

        mark#(and(X1,X2))

        →

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

        (71)

        could be deleted.

        1.1.1.1.1.1.1.1.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)

          (89)

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

          Using the linear polynomial interpretation over the naturals

          [s(x1)]	=	1 · x1
          [mark#(x1)]	=	1 · x1

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

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Size-Change Termination

          Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

          mark#(s(X))	→	mark#(X)	(89)
          1	>	1

          As there is no critical graph in the transitive closure, there are no infinite chains.

    • The 2^nd component contains the pair

      a__isNat#(s(N))

      →

      a__isNat#(N)

      (45)

      1.1.1.1.1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [s(x1)]	=	1 · x1
      [a__isNat#(x1)]	=	1 · x1

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

      1.1.1.1.1.1.1.1.1.2.1 Size-Change Termination

      Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

      a__isNat#(s(N))	→	a__isNat#(N)	(45)
      1	>	1

      As there is no critical graph in the transitive closure, there are no infinite chains.

  • The 2^nd component contains the pair

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

    1.1.1.1.2 Reduction Pair Processor

    Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

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

    the pair

    a__uLength#(tt,L)

    →

    a__length#(mark(L))

    (69)

    could be deleted.

    1.1.1.1.2.1 Size-Change Termination

    Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

    a__length#(cons(N,L))	→	a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)	(65)
    1	>	2

    As there is no critical graph in the transitive closure, there are no infinite chains.