Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM99_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ 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

  a__filter#(s(s(X)),cons(Y,Z))	→	mark#(Y)	(36)
  mark#(divides(X1,X2))	→	mark#(X1)	(57)
  mark#(divides(X1,X2))	→	mark#(X2)	(56)
  mark#(cons(X1,X2))	→	mark#(X1)	(55)
  mark#(s(X))	→	mark#(X)	(54)
  mark#(filter(X1,X2))	→	a__filter#(mark(X1),mark(X2))	(53)
  a__filter#(s(s(X)),cons(Y,Z))	→	mark#(X)	(37)
  mark#(filter(X1,X2))	→	mark#(X1)	(52)
  mark#(filter(X1,X2))	→	mark#(X2)	(51)
  mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
  a__if#(false,X,Y)	→	mark#(Y)	(35)
  mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
  mark#(tail(X))	→	a__tail#(mark(X))	(48)
  a__tail#(cons(X,Y))	→	mark#(Y)	(33)
  mark#(tail(X))	→	mark#(X)	(47)
  mark#(head(X))	→	a__head#(mark(X))	(46)
  a__head#(cons(X,Y))	→	mark#(X)	(32)
  mark#(head(X))	→	mark#(X)	(45)
  mark#(from(X))	→	a__from#(mark(X))	(44)
  a__from#(X)	→	mark#(X)	(31)
  mark#(from(X))	→	mark#(X)	(43)
  mark#(sieve(X))	→	a__sieve#(mark(X))	(42)
  a__sieve#(cons(X,Y))	→	mark#(X)	(39)
  mark#(sieve(X))	→	mark#(X)	(41)
  mark#(primes)	→	a__primes#	(40)
  a__primes#	→	a__sieve#(a__from(s(s(0))))	(30)
  a__primes#	→	a__from#(s(s(0)))	(29)
  a__if#(true,X,Y)	→	mark#(X)	(34)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [head(x1)]	=	7 · x1 + 1
  [a__sieve(x1)]	=	0 · x1 + 0
  [filter(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [a__head(x1)]	=	7 · x1 + 1
  [0]	=	0
  [a__from(x1)]	=	0 · x1 + 0
  [sieve(x1)]	=	0 · x1 + 0
  [a__primes#]	=	0
  [a__tail#(x1)]	=	0 · x1 + -∞
  [tail(x1)]	=	0 · x1 + 0
  [primes]	=	0
  [a__if#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + -∞
  [a__from#(x1)]	=	0 · x1 + 0
  [a__filter#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [mark(x1)]	=	0 · x1 + -∞
  [true]	=	0
  [a__primes]	=	0
  [cons(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + -∞
  [a__head#(x1)]	=	0 · x1 + 0
  [divides(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [false]	=	0
  [a__sieve#(x1)]	=	0 · x1 + 0
  [mark#(x1)]	=	0 · x1 + 0
  [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + -∞
  [a__tail(x1)]	=	0 · x1 + 0
  [a__filter(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [from(x1)]	=	0 · x1 + 0
  [s(x1)]	=	0 · x1 + -∞

  together with the usable rules

  a__primes	→	a__sieve(a__from(s(s(0))))	(1)
  a__from(X)	→	cons(mark(X),from(s(X)))	(2)
  a__head(cons(X,Y))	→	mark(X)	(3)
  a__tail(cons(X,Y))	→	mark(Y)	(4)
  a__if(true,X,Y)	→	mark(X)	(5)
  a__if(false,X,Y)	→	mark(Y)	(6)
  a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
  a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
  mark(primes)	→	a__primes	(9)
  mark(sieve(X))	→	a__sieve(mark(X))	(10)
  mark(from(X))	→	a__from(mark(X))	(11)
  mark(head(X))	→	a__head(mark(X))	(12)
  mark(tail(X))	→	a__tail(mark(X))	(13)
  mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
  mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
  mark(s(X))	→	s(mark(X))	(16)
  mark(0)	→	0	(17)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
  mark(true)	→	true	(19)
  mark(false)	→	false	(20)
  mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
  a__primes	→	primes	(22)
  a__sieve(X)	→	sieve(X)	(23)
  a__from(X)	→	from(X)	(24)
  a__head(X)	→	head(X)	(25)
  a__tail(X)	→	tail(X)	(26)
  a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
  a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

  mark#(head(X))	→	a__head#(mark(X))	(46)
  mark#(head(X))	→	mark#(X)	(45)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    a__filter#(s(s(X)),cons(Y,Z))	→	mark#(Y)	(36)
    mark#(divides(X1,X2))	→	mark#(X1)	(57)
    mark#(divides(X1,X2))	→	mark#(X2)	(56)
    mark#(cons(X1,X2))	→	mark#(X1)	(55)
    mark#(s(X))	→	mark#(X)	(54)
    mark#(filter(X1,X2))	→	a__filter#(mark(X1),mark(X2))	(53)
    a__filter#(s(s(X)),cons(Y,Z))	→	mark#(X)	(37)
    mark#(filter(X1,X2))	→	mark#(X1)	(52)
    mark#(filter(X1,X2))	→	mark#(X2)	(51)
    mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
    a__if#(false,X,Y)	→	mark#(Y)	(35)
    mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
    mark#(tail(X))	→	a__tail#(mark(X))	(48)
    a__tail#(cons(X,Y))	→	mark#(Y)	(33)
    mark#(tail(X))	→	mark#(X)	(47)
    mark#(from(X))	→	a__from#(mark(X))	(44)
    a__from#(X)	→	mark#(X)	(31)
    mark#(from(X))	→	mark#(X)	(43)
    mark#(sieve(X))	→	a__sieve#(mark(X))	(42)
    a__sieve#(cons(X,Y))	→	mark#(X)	(39)
    mark#(sieve(X))	→	mark#(X)	(41)
    mark#(primes)	→	a__primes#	(40)
    a__primes#	→	a__sieve#(a__from(s(s(0))))	(30)
    a__primes#	→	a__from#(s(s(0)))	(29)
    a__if#(true,X,Y)	→	mark#(X)	(34)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the arctic semiring over the integers

    [head(x1)]	=	0 · x1 + -∞
    [a__sieve(x1)]	=	0 · x1 + 2
    [filter(x1, x2)]	=	0 · x1 + 0 · x2 + 2
    [a__head(x1)]	=	0 · x1 + 0
    [0]	=	2
    [a__from(x1)]	=	1 · x1 + 2
    [sieve(x1)]	=	0 · x1 + 2
    [a__primes#]	=	3
    [a__tail#(x1)]	=	0 · x1 + 0
    [tail(x1)]	=	1 · x1 + 4
    [primes]	=	4
    [a__if#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + 0
    [a__from#(x1)]	=	1 · x1 + 2
    [a__filter#(x1, x2)]	=	0 · x1 + 0 · x2 + 2
    [mark(x1)]	=	0 · x1 + 0
    [true]	=	0
    [a__primes]	=	4
    [cons(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
    [divides(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
    [false]	=	0
    [a__sieve#(x1)]	=	0 · x1 + 2
    [mark#(x1)]	=	0 · x1 + 0
    [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
    [a__tail(x1)]	=	1 · x1 + 4
    [a__filter(x1, x2)]	=	0 · x1 + 0 · x2 + 2
    [from(x1)]	=	1 · x1 + 2
    [s(x1)]	=	0 · x1 + -∞

    together with the usable rules

    a__primes	→	a__sieve(a__from(s(s(0))))	(1)
    a__from(X)	→	cons(mark(X),from(s(X)))	(2)
    a__head(cons(X,Y))	→	mark(X)	(3)
    a__tail(cons(X,Y))	→	mark(Y)	(4)
    a__if(true,X,Y)	→	mark(X)	(5)
    a__if(false,X,Y)	→	mark(Y)	(6)
    a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
    a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
    mark(primes)	→	a__primes	(9)
    mark(sieve(X))	→	a__sieve(mark(X))	(10)
    mark(from(X))	→	a__from(mark(X))	(11)
    mark(head(X))	→	a__head(mark(X))	(12)
    mark(tail(X))	→	a__tail(mark(X))	(13)
    mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
    mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
    mark(s(X))	→	s(mark(X))	(16)
    mark(0)	→	0	(17)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
    mark(true)	→	true	(19)
    mark(false)	→	false	(20)
    mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
    a__primes	→	primes	(22)
    a__sieve(X)	→	sieve(X)	(23)
    a__from(X)	→	from(X)	(24)
    a__head(X)	→	head(X)	(25)
    a__tail(X)	→	tail(X)	(26)
    a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
    a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

    mark#(tail(X))	→	a__tail#(mark(X))	(48)
    mark#(tail(X))	→	mark#(X)	(47)
    a__from#(X)	→	mark#(X)	(31)
    mark#(from(X))	→	mark#(X)	(43)
    mark#(primes)	→	a__primes#	(40)

    could be deleted.

    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__filter#(s(s(X)),cons(Y,Z))	→	mark#(Y)	(36)
      mark#(divides(X1,X2))	→	mark#(X1)	(57)
      mark#(divides(X1,X2))	→	mark#(X2)	(56)
      mark#(cons(X1,X2))	→	mark#(X1)	(55)
      mark#(s(X))	→	mark#(X)	(54)
      mark#(filter(X1,X2))	→	a__filter#(mark(X1),mark(X2))	(53)
      a__filter#(s(s(X)),cons(Y,Z))	→	mark#(X)	(37)
      mark#(filter(X1,X2))	→	mark#(X1)	(52)
      mark#(filter(X1,X2))	→	mark#(X2)	(51)
      mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
      a__if#(false,X,Y)	→	mark#(Y)	(35)
      mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
      mark#(sieve(X))	→	a__sieve#(mark(X))	(42)
      a__sieve#(cons(X,Y))	→	mark#(X)	(39)
      mark#(sieve(X))	→	mark#(X)	(41)
      a__if#(true,X,Y)	→	mark#(X)	(34)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the arctic semiring over the integers

      [head(x1)]	=	0 · x1 + -∞
      [a__sieve(x1)]	=	0 · x1 + 0
      [filter(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
      [a__head(x1)]	=	0 · x1 + 0
      [0]	=	1
      [a__from(x1)]	=	1 · x1 + 1
      [sieve(x1)]	=	0 · x1 + -∞
      [tail(x1)]	=	0 · x1 + -∞
      [primes]	=	3
      [a__if#(x1, x2, x3)]	=	2 · x1 + 4 · x2 + 4 · x3 + 0
      [a__filter#(x1, x2)]	=	4 · x1 + 4 · x2 + 0
      [mark(x1)]	=	0 · x1 + 0
      [true]	=	2
      [a__primes]	=	3
      [cons(x1, x2)]	=	1 · x1 + 0 · x2 + 1
      [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + -∞
      [divides(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [false]	=	2
      [a__sieve#(x1)]	=	4 · x1 + 0
      [mark#(x1)]	=	4 · x1 + 4
      [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
      [a__tail(x1)]	=	0 · x1 + 0
      [a__filter(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [from(x1)]	=	1 · x1 + 1
      [s(x1)]	=	0 · x1 + 0

      together with the usable rules

      a__primes	→	a__sieve(a__from(s(s(0))))	(1)
      a__from(X)	→	cons(mark(X),from(s(X)))	(2)
      a__head(cons(X,Y))	→	mark(X)	(3)
      a__tail(cons(X,Y))	→	mark(Y)	(4)
      a__if(true,X,Y)	→	mark(X)	(5)
      a__if(false,X,Y)	→	mark(Y)	(6)
      a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
      a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
      mark(primes)	→	a__primes	(9)
      mark(sieve(X))	→	a__sieve(mark(X))	(10)
      mark(from(X))	→	a__from(mark(X))	(11)
      mark(head(X))	→	a__head(mark(X))	(12)
      mark(tail(X))	→	a__tail(mark(X))	(13)
      mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
      mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
      mark(s(X))	→	s(mark(X))	(16)
      mark(0)	→	0	(17)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
      mark(true)	→	true	(19)
      mark(false)	→	false	(20)
      mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
      a__primes	→	primes	(22)
      a__sieve(X)	→	sieve(X)	(23)
      a__from(X)	→	from(X)	(24)
      a__head(X)	→	head(X)	(25)
      a__tail(X)	→	tail(X)	(26)
      a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
      a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

      a__filter#(s(s(X)),cons(Y,Z))	→	mark#(Y)	(36)
      mark#(cons(X1,X2))	→	mark#(X1)	(55)
      a__sieve#(cons(X,Y))	→	mark#(X)	(39)

      could be deleted.

      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__filter#(s(s(X)),cons(Y,Z))	→	mark#(X)	(37)
        mark#(divides(X1,X2))	→	mark#(X1)	(57)
        mark#(divides(X1,X2))	→	mark#(X2)	(56)
        mark#(s(X))	→	mark#(X)	(54)
        mark#(filter(X1,X2))	→	a__filter#(mark(X1),mark(X2))	(53)
        mark#(filter(X1,X2))	→	mark#(X1)	(52)
        mark#(filter(X1,X2))	→	mark#(X2)	(51)
        mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
        a__if#(false,X,Y)	→	mark#(Y)	(35)
        mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
        mark#(sieve(X))	→	mark#(X)	(41)
        a__if#(true,X,Y)	→	mark#(X)	(34)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the arctic semiring over the integers

        [head(x1)]	=	0 · x1 + -∞
        [a__sieve(x1)]	=	1 · x1 + 1
        [filter(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [a__head(x1)]	=	0 · x1 + 0
        [0]	=	2
        [a__from(x1)]	=	1 · x1 + 4
        [sieve(x1)]	=	1 · x1 + 1
        [tail(x1)]	=	0 · x1 + -∞
        [primes]	=	5
        [a__if#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__filter#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [mark(x1)]	=	0 · x1 + 0
        [true]	=	0
        [a__primes]	=	5
        [cons(x1, x2)]	=	1 · x1 + 0 · x2 + 1
        [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [divides(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [false]	=	0
        [mark#(x1)]	=	0 · x1 + 0
        [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__tail(x1)]	=	0 · x1 + 0
        [a__filter(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [from(x1)]	=	1 · x1 + 4
        [s(x1)]	=	0 · x1 + 0

        together with the usable rules

        a__primes	→	a__sieve(a__from(s(s(0))))	(1)
        a__from(X)	→	cons(mark(X),from(s(X)))	(2)
        a__head(cons(X,Y))	→	mark(X)	(3)
        a__tail(cons(X,Y))	→	mark(Y)	(4)
        a__if(true,X,Y)	→	mark(X)	(5)
        a__if(false,X,Y)	→	mark(Y)	(6)
        a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
        a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
        mark(primes)	→	a__primes	(9)
        mark(sieve(X))	→	a__sieve(mark(X))	(10)
        mark(from(X))	→	a__from(mark(X))	(11)
        mark(head(X))	→	a__head(mark(X))	(12)
        mark(tail(X))	→	a__tail(mark(X))	(13)
        mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
        mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
        mark(s(X))	→	s(mark(X))	(16)
        mark(0)	→	0	(17)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
        mark(true)	→	true	(19)
        mark(false)	→	false	(20)
        mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
        a__primes	→	primes	(22)
        a__sieve(X)	→	sieve(X)	(23)
        a__from(X)	→	from(X)	(24)
        a__head(X)	→	head(X)	(25)
        a__tail(X)	→	tail(X)	(26)
        a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
        a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

        mark#(sieve(X))

        →

        mark#(X)

        (41)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the arctic semiring over the integers

        [head(x1)]	=	1 · x1 + -∞
        [a__sieve(x1)]	=	0 · x1 + 0
        [filter(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [a__head(x1)]	=	1 · x1 + -∞
        [0]	=	4
        [a__from(x1)]	=	2 · x1 + 7
        [sieve(x1)]	=	0 · x1 + 0
        [tail(x1)]	=	3 · x1 + -∞
        [primes]	=	7
        [a__if#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__filter#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [mark(x1)]	=	0 · x1 + -∞
        [true]	=	0
        [a__primes]	=	7
        [cons(x1, x2)]	=	2 · x1 + 0 · x2 + -∞
        [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [divides(x1, x2)]	=	0 · x1 + 1 · x2 + 0
        [false]	=	0
        [mark#(x1)]	=	0 · x1 + -∞
        [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__tail(x1)]	=	3 · x1 + -∞
        [a__filter(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [from(x1)]	=	2 · x1 + 7
        [s(x1)]	=	0 · x1 + -∞

        together with the usable rules

        a__primes	→	a__sieve(a__from(s(s(0))))	(1)
        a__from(X)	→	cons(mark(X),from(s(X)))	(2)
        a__head(cons(X,Y))	→	mark(X)	(3)
        a__tail(cons(X,Y))	→	mark(Y)	(4)
        a__if(true,X,Y)	→	mark(X)	(5)
        a__if(false,X,Y)	→	mark(Y)	(6)
        a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
        a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
        mark(primes)	→	a__primes	(9)
        mark(sieve(X))	→	a__sieve(mark(X))	(10)
        mark(from(X))	→	a__from(mark(X))	(11)
        mark(head(X))	→	a__head(mark(X))	(12)
        mark(tail(X))	→	a__tail(mark(X))	(13)
        mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
        mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
        mark(s(X))	→	s(mark(X))	(16)
        mark(0)	→	0	(17)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
        mark(true)	→	true	(19)
        mark(false)	→	false	(20)
        mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
        a__primes	→	primes	(22)
        a__sieve(X)	→	sieve(X)	(23)
        a__from(X)	→	from(X)	(24)
        a__head(X)	→	head(X)	(25)
        a__tail(X)	→	tail(X)	(26)
        a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
        a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

        mark#(divides(X1,X2))

        →

        mark#(X2)

        (56)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the arctic semiring over the integers

        [head(x1)]	=	3 · x1 + -∞
        [a__sieve(x1)]	=	1 · x1 + 0
        [filter(x1, x2)]	=	1 · x1 + 0 · x2 + 0
        [a__head(x1)]	=	3 · x1 + -∞
        [0]	=	0
        [a__from(x1)]	=	1 · x1 + -∞
        [sieve(x1)]	=	1 · x1 + 0
        [tail(x1)]	=	0 · x1 + 0
        [primes]	=	2
        [a__if#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__filter#(x1, x2)]	=	0 · x1 + -∞ · x2 + -∞
        [mark(x1)]	=	0 · x1 + -∞
        [true]	=	0
        [a__primes]	=	2
        [cons(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
        [if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [divides(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [false]	=	0
        [mark#(x1)]	=	0 · x1 + -∞
        [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
        [a__tail(x1)]	=	0 · x1 + 0
        [a__filter(x1, x2)]	=	1 · x1 + 0 · x2 + 0
        [from(x1)]	=	1 · x1 + -∞
        [s(x1)]	=	0 · x1 + -∞

        together with the usable rules

        a__primes	→	a__sieve(a__from(s(s(0))))	(1)
        a__from(X)	→	cons(mark(X),from(s(X)))	(2)
        a__head(cons(X,Y))	→	mark(X)	(3)
        a__tail(cons(X,Y))	→	mark(Y)	(4)
        a__if(true,X,Y)	→	mark(X)	(5)
        a__if(false,X,Y)	→	mark(Y)	(6)
        a__filter(s(s(X)),cons(Y,Z))	→	a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))	(7)
        a__sieve(cons(X,Y))	→	cons(mark(X),filter(X,sieve(Y)))	(8)
        mark(primes)	→	a__primes	(9)
        mark(sieve(X))	→	a__sieve(mark(X))	(10)
        mark(from(X))	→	a__from(mark(X))	(11)
        mark(head(X))	→	a__head(mark(X))	(12)
        mark(tail(X))	→	a__tail(mark(X))	(13)
        mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(14)
        mark(filter(X1,X2))	→	a__filter(mark(X1),mark(X2))	(15)
        mark(s(X))	→	s(mark(X))	(16)
        mark(0)	→	0	(17)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(18)
        mark(true)	→	true	(19)
        mark(false)	→	false	(20)
        mark(divides(X1,X2))	→	divides(mark(X1),mark(X2))	(21)
        a__primes	→	primes	(22)
        a__sieve(X)	→	sieve(X)	(23)
        a__from(X)	→	from(X)	(24)
        a__head(X)	→	head(X)	(25)
        a__tail(X)	→	tail(X)	(26)
        a__if(X1,X2,X3)	→	if(X1,X2,X3)	(27)
        a__filter(X1,X2)	→	filter(X1,X2)	(28)

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

        mark#(filter(X1,X2))	→	a__filter#(mark(X1),mark(X2))	(53)
        mark#(filter(X1,X2))	→	mark#(X1)	(52)

        could be deleted.

        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#(divides(X1,X2))	→	mark#(X1)	(57)
          mark#(s(X))	→	mark#(X)	(54)
          mark#(filter(X1,X2))	→	mark#(X2)	(51)
          mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
          a__if#(false,X,Y)	→	mark#(Y)	(35)
          mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
          a__if#(true,X,Y)	→	mark#(X)	(34)

          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#(divides(X1,X2))	→	mark#(X1)	(57)
          1	>	1
          mark#(s(X))	→	mark#(X)	(54)
          1	>	1
          mark#(filter(X1,X2))	→	mark#(X2)	(51)
          1	>	1
          mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(50)
          1	>	3
          1	>	2
          a__if#(false,X,Y)	→	mark#(Y)	(35)
          3	≥	1
          mark#(if(X1,X2,X3))	→	mark#(X1)	(49)
          1	>	1
          a__if#(true,X,Y)	→	mark#(X)	(34)
          2	≥	1

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