Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex8_BLR02_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

  a__fib#(N)	→	mark#(N)	(42)
  a__add#(s(X),Y)	→	mark#(Y)	(27)
  a__sel#(s(N),cons(X,XS))	→	mark#(XS)	(41)
  mark#(add(X1,X2))	→	mark#(X2)	(26)
  a__sel#(0,cons(X,XS))	→	mark#(X)	(40)
  mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
  mark#(fib1(X1,X2))	→	mark#(X2)	(39)
  a__fib1#(X,Y)	→	mark#(X)	(38)
  a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
  a__sel#(s(N),cons(X,XS))	→	mark#(N)	(37)
  a__add#(s(X),Y)	→	mark#(X)	(23)
  a__add#(0,X)	→	mark#(X)	(36)
  mark#(sel(X1,X2))	→	mark#(X1)	(35)
  mark#(fib(X))	→	mark#(X)	(22)
  mark#(s(X))	→	mark#(X)	(21)
  mark#(add(X1,X2))	→	mark#(X1)	(20)
  a__fib#(N)	→	a__fib1#(s(0),s(0))	(34)
  a__fib#(N)	→	a__sel#(mark(N),a__fib1(s(0),s(0)))	(33)
  mark#(fib1(X1,X2))	→	a__fib1#(mark(X1),mark(X2))	(19)
  mark#(sel(X1,X2))	→	mark#(X2)	(32)
  mark#(cons(X1,X2))	→	mark#(X1)	(31)
  mark#(fib(X))	→	a__fib#(mark(X))	(30)
  mark#(fib1(X1,X2))	→	mark#(X1)	(29)
  a__sel#(s(N),cons(X,XS))	→	a__sel#(mark(N),mark(XS))	(18)
  mark#(sel(X1,X2))	→	a__sel#(mark(X1),mark(X2))	(28)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 0
  [a__add#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__fib1#(x1, x2)]	=	max(x1 + 0, 0)
  [fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [fib(x1)]	=	x1 + 2
  [mark#(x1)]	=	x1 + 0
  [0]	=	1
  [sel(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
  [a__sel#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [mark(x1)]	=	x1 + 0
  [a__sel(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
  [a__fib#(x1)]	=	x1 + 1
  [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__fib(x1)]	=	x1 + 2
  [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)

  together with the usable rules

  a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
  a__sel(X1,X2)	→	sel(X1,X2)	(15)
  mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
  a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
  a__add(0,X)	→	mark(X)	(3)
  a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
  a__add(X1,X2)	→	add(X1,X2)	(17)
  a__sel(0,cons(X,XS))	→	mark(X)	(5)
  mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
  mark(fib(X))	→	a__fib(mark(X))	(7)
  a__fib(X)	→	fib(X)	(14)
  mark(0)	→	0	(12)
  mark(s(X))	→	s(mark(X))	(11)
  mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
  a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
  a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

  a__fib#(N)	→	mark#(N)	(42)
  mark#(sel(X1,X2))	→	mark#(X1)	(35)
  mark#(fib(X))	→	mark#(X)	(22)
  mark#(fib(X))	→	a__fib#(mark(X))	(30)

  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__add#(s(X),Y)	→	mark#(Y)	(27)
    a__add#(s(X),Y)	→	mark#(X)	(23)
    a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
    mark#(sel(X1,X2))	→	mark#(X2)	(32)
    mark#(sel(X1,X2))	→	a__sel#(mark(X1),mark(X2))	(28)
    a__add#(0,X)	→	mark#(X)	(36)
    a__sel#(0,cons(X,XS))	→	mark#(X)	(40)
    mark#(add(X1,X2))	→	mark#(X2)	(26)
    mark#(add(X1,X2))	→	mark#(X1)	(20)
    mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
    mark#(s(X))	→	mark#(X)	(21)
    mark#(fib1(X1,X2))	→	mark#(X2)	(39)
    mark#(fib1(X1,X2))	→	mark#(X1)	(29)
    mark#(fib1(X1,X2))	→	a__fib1#(mark(X1),mark(X2))	(19)
    mark#(cons(X1,X2))	→	mark#(X1)	(31)
    a__sel#(s(N),cons(X,XS))	→	mark#(XS)	(41)
    a__sel#(s(N),cons(X,XS))	→	mark#(N)	(37)
    a__sel#(s(N),cons(X,XS))	→	a__sel#(mark(N),mark(XS))	(18)
    a__fib1#(X,Y)	→	mark#(X)	(38)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [s(x1)]	=	x1 + 0
    [a__add#(x1, x2)]	=	max(x1 + 18458, x2 + 18458, 0)
    [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [a__fib1#(x1, x2)]	=	max(x1 + 18458, 0)
    [fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [fib(x1)]	=	x1 + 1325
    [mark#(x1)]	=	x1 + 18458
    [0]	=	1
    [sel(x1, x2)]	=	max(x1 + 1325, x2 + 0, 0)
    [a__sel#(x1, x2)]	=	max(x1 + 18459, x2 + 18458, 0)
    [mark(x1)]	=	x1 + 0
    [a__sel(x1, x2)]	=	max(x1 + 1325, x2 + 0, 0)
    [a__fib#(x1)]	=	x1 + 1
    [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [a__fib(x1)]	=	x1 + 1325
    [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [a__fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)

    together with the usable rules

    a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
    a__sel(X1,X2)	→	sel(X1,X2)	(15)
    mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
    a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
    a__add(0,X)	→	mark(X)	(3)
    a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
    a__add(X1,X2)	→	add(X1,X2)	(17)
    a__sel(0,cons(X,XS))	→	mark(X)	(5)
    mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
    mark(fib(X))	→	a__fib(mark(X))	(7)
    a__fib(X)	→	fib(X)	(14)
    mark(0)	→	0	(12)
    mark(s(X))	→	s(mark(X))	(11)
    mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
    a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
    a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

    a__sel#(s(N),cons(X,XS))

    →

    mark#(N)

    (37)

    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__add#(s(X),Y)	→	mark#(Y)	(27)
      a__add#(s(X),Y)	→	mark#(X)	(23)
      a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
      mark#(sel(X1,X2))	→	mark#(X2)	(32)
      mark#(sel(X1,X2))	→	a__sel#(mark(X1),mark(X2))	(28)
      a__add#(0,X)	→	mark#(X)	(36)
      a__sel#(0,cons(X,XS))	→	mark#(X)	(40)
      mark#(add(X1,X2))	→	mark#(X2)	(26)
      mark#(add(X1,X2))	→	mark#(X1)	(20)
      mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
      mark#(s(X))	→	mark#(X)	(21)
      mark#(fib1(X1,X2))	→	mark#(X2)	(39)
      mark#(fib1(X1,X2))	→	mark#(X1)	(29)
      mark#(fib1(X1,X2))	→	a__fib1#(mark(X1),mark(X2))	(19)
      mark#(cons(X1,X2))	→	mark#(X1)	(31)
      a__sel#(s(N),cons(X,XS))	→	mark#(XS)	(41)
      a__sel#(s(N),cons(X,XS))	→	a__sel#(mark(N),mark(XS))	(18)
      a__fib1#(X,Y)	→	mark#(X)	(38)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [s(x1)]	=	x1 + 0
      [a__add#(x1, x2)]	=	max(x1 + 18588, x2 + 18588, 0)
      [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__fib1#(x1, x2)]	=	max(x1 + 18588, 0)
      [fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [fib(x1)]	=	x1 + 39474
      [mark#(x1)]	=	x1 + 18588
      [0]	=	16908
      [sel(x1, x2)]	=	max(x1 + 21241, x2 + 21240, 0)
      [a__sel#(x1, x2)]	=	max(x1 + 39826, x2 + 39827, 0)
      [mark(x1)]	=	x1 + 0
      [a__sel(x1, x2)]	=	max(x1 + 21241, x2 + 21240, 0)
      [a__fib#(x1)]	=	x1 + 1
      [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__fib(x1)]	=	x1 + 39474
      [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__fib1(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)

      together with the usable rules

      a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
      a__sel(X1,X2)	→	sel(X1,X2)	(15)
      mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
      a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
      a__add(0,X)	→	mark(X)	(3)
      a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
      a__add(X1,X2)	→	add(X1,X2)	(17)
      a__sel(0,cons(X,XS))	→	mark(X)	(5)
      mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
      mark(fib(X))	→	a__fib(mark(X))	(7)
      a__fib(X)	→	fib(X)	(14)
      mark(0)	→	0	(12)
      mark(s(X))	→	s(mark(X))	(11)
      mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
      a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
      a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

      mark#(sel(X1,X2))	→	mark#(X2)	(32)
      mark#(sel(X1,X2))	→	a__sel#(mark(X1),mark(X2))	(28)
      a__sel#(0,cons(X,XS))	→	mark#(X)	(40)
      a__sel#(s(N),cons(X,XS))	→	mark#(XS)	(41)

      could be deleted.

      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

        a__sel#(s(N),cons(X,XS))

        →

        a__sel#(mark(N),mark(XS))

        (18)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the argument filter

        π(a__fib1#)	=	2
        π(a__sel#)	=	1
        π(mark)	=	1

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

        prec(s)	=	4		status(s)	=	[1]		list-extension(s)	=	Lex
        prec(a__add#)	=	0		status(a__add#)	=	[2]		list-extension(a__add#)	=	Lex
        prec(a__add)	=	5		status(a__add)	=	[2, 1]		list-extension(a__add)	=	Lex
        prec(fib1)	=	3		status(fib1)	=	[]		list-extension(fib1)	=	Lex
        prec(fib)	=	1		status(fib)	=	[]		list-extension(fib)	=	Lex
        prec(mark#)	=	0		status(mark#)	=	[]		list-extension(mark#)	=	Lex
        prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
        prec(sel)	=	2		status(sel)	=	[]		list-extension(sel)	=	Lex
        prec(a__sel)	=	2		status(a__sel)	=	[]		list-extension(a__sel)	=	Lex
        prec(a__fib#)	=	0		status(a__fib#)	=	[]		list-extension(a__fib#)	=	Lex
        prec(cons)	=	1		status(cons)	=	[1]		list-extension(cons)	=	Lex
        prec(a__fib)	=	1		status(a__fib)	=	[]		list-extension(a__fib)	=	Lex
        prec(add)	=	5		status(add)	=	[2, 1]		list-extension(add)	=	Lex
        prec(a__fib1)	=	3		status(a__fib1)	=	[]		list-extension(a__fib1)	=	Lex

        and the following Max-polynomial interpretation

        [s(x1)]	=	x1 + 0
        [a__add#(x1, x2)]	=	max(x2 + 1, 0)
        [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [fib1(x1, x2)]	=	max(x1 + 8947, x2 + 8947, 0)
        [fib(x1)]	=	17895
        [mark#(x1)]	=	1
        [0]	=	1
        [sel(x1, x2)]	=	x2 + 8946
        [a__sel(x1, x2)]	=	x2 + 8946
        [a__fib#(x1)]	=	1
        [cons(x1, x2)]	=	max(x1 + 8947, x2 + 0, 0)
        [a__fib(x1)]	=	17895
        [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [a__fib1(x1, x2)]	=	max(x1 + 8947, x2 + 8947, 0)

        together with the usable rules

        a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
        a__sel(X1,X2)	→	sel(X1,X2)	(15)
        mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
        a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
        a__add(0,X)	→	mark(X)	(3)
        a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
        a__add(X1,X2)	→	add(X1,X2)	(17)
        a__sel(0,cons(X,XS))	→	mark(X)	(5)
        mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
        mark(fib(X))	→	a__fib(mark(X))	(7)
        a__fib(X)	→	fib(X)	(14)
        mark(0)	→	0	(12)
        mark(s(X))	→	s(mark(X))	(11)
        mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
        a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
        a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

        a__sel#(s(N),cons(X,XS))

        →

        a__sel#(mark(N),mark(XS))

        (18)

        could be deleted.

        1.1.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__add#(s(X),Y)	→	mark#(Y)	(27)
        a__add#(s(X),Y)	→	mark#(X)	(23)
        a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
        a__add#(0,X)	→	mark#(X)	(36)
        mark#(add(X1,X2))	→	mark#(X2)	(26)
        mark#(add(X1,X2))	→	mark#(X1)	(20)
        mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
        mark#(s(X))	→	mark#(X)	(21)
        mark#(fib1(X1,X2))	→	mark#(X2)	(39)
        mark#(fib1(X1,X2))	→	mark#(X1)	(29)
        mark#(fib1(X1,X2))	→	a__fib1#(mark(X1),mark(X2))	(19)
        mark#(cons(X1,X2))	→	mark#(X1)	(31)
        a__fib1#(X,Y)	→	mark#(X)	(38)

        1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [s(x1)]	=	x1 + 0
        [a__add#(x1, x2)]	=	max(x1 + 13359, x2 + 13359, 0)
        [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [a__fib1#(x1, x2)]	=	max(x1 + 13360, 0)
        [fib1(x1, x2)]	=	max(x1 + 4188, x2 + 4188, 0)
        [fib(x1)]	=	x1 + 35931
        [mark#(x1)]	=	x1 + 13359
        [0]	=	1
        [sel(x1, x2)]	=	max(x1 + 31742, x2 + 31742, 0)
        [a__sel#(x1, x2)]	=	max(0)
        [mark(x1)]	=	x1 + 0
        [a__sel(x1, x2)]	=	max(x1 + 31742, x2 + 31742, 0)
        [a__fib#(x1)]	=	1
        [cons(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
        [a__fib(x1)]	=	x1 + 35931
        [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [a__fib1(x1, x2)]	=	max(x1 + 4188, x2 + 4188, 0)

        together with the usable rules

        a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
        a__sel(X1,X2)	→	sel(X1,X2)	(15)
        mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
        a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
        a__add(0,X)	→	mark(X)	(3)
        a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
        a__add(X1,X2)	→	add(X1,X2)	(17)
        a__sel(0,cons(X,XS))	→	mark(X)	(5)
        mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
        mark(fib(X))	→	a__fib(mark(X))	(7)
        a__fib(X)	→	fib(X)	(14)
        mark(0)	→	0	(12)
        mark(s(X))	→	s(mark(X))	(11)
        mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
        a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
        a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

        mark#(fib1(X1,X2))	→	mark#(X2)	(39)
        mark#(fib1(X1,X2))	→	mark#(X1)	(29)
        mark#(fib1(X1,X2))	→	a__fib1#(mark(X1),mark(X2))	(19)
        mark#(cons(X1,X2))	→	mark#(X1)	(31)
        a__fib1#(X,Y)	→	mark#(X)	(38)

        could be deleted.

        1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          a__add#(s(X),Y)	→	mark#(Y)	(27)
          a__add#(s(X),Y)	→	mark#(X)	(23)
          a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
          a__add#(0,X)	→	mark#(X)	(36)
          mark#(add(X1,X2))	→	mark#(X2)	(26)
          mark#(add(X1,X2))	→	mark#(X1)	(20)
          mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
          mark#(s(X))	→	mark#(X)	(21)

          1.1.1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

          Using the argument filter

          π(a__fib1#)	=	2
          π(a__sel#)	=	1
          π(mark)	=	1

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

          prec(s)	=	4		status(s)	=	[1]		list-extension(s)	=	Lex
          prec(a__add#)	=	6		status(a__add#)	=	[1, 2]		list-extension(a__add#)	=	Lex
          prec(a__add)	=	7		status(a__add)	=	[2, 1]		list-extension(a__add)	=	Lex
          prec(fib1)	=	3		status(fib1)	=	[]		list-extension(fib1)	=	Lex
          prec(fib)	=	1		status(fib)	=	[]		list-extension(fib)	=	Lex
          prec(mark#)	=	5		status(mark#)	=	[1]		list-extension(mark#)	=	Lex
          prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
          prec(sel)	=	2		status(sel)	=	[]		list-extension(sel)	=	Lex
          prec(a__sel)	=	2		status(a__sel)	=	[]		list-extension(a__sel)	=	Lex
          prec(a__fib#)	=	0		status(a__fib#)	=	[]		list-extension(a__fib#)	=	Lex
          prec(cons)	=	1		status(cons)	=	[1]		list-extension(cons)	=	Lex
          prec(a__fib)	=	1		status(a__fib)	=	[]		list-extension(a__fib)	=	Lex
          prec(add)	=	7		status(add)	=	[2, 1]		list-extension(add)	=	Lex
          prec(a__fib1)	=	3		status(a__fib1)	=	[]		list-extension(a__fib1)	=	Lex

          and the following Max-polynomial interpretation

          [s(x1)]	=	x1 + 0
          [a__add#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
          [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
          [fib1(x1, x2)]	=	max(x1 + 2, x2 + 2, 0)
          [fib(x1)]	=	5
          [mark#(x1)]	=	x1 + 0
          [0]	=	1
          [sel(x1, x2)]	=	x2 + 1
          [a__sel(x1, x2)]	=	x2 + 1
          [a__fib#(x1)]	=	1
          [cons(x1, x2)]	=	max(x1 + 2, x2 + 0, 0)
          [a__fib(x1)]	=	5
          [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
          [a__fib1(x1, x2)]	=	max(x1 + 2, x2 + 2, 0)

          together with the usable rules

          a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(4)
          a__sel(X1,X2)	→	sel(X1,X2)	(15)
          mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(8)
          a__fib(N)	→	a__sel(mark(N),a__fib1(s(0),s(0)))	(1)
          a__add(0,X)	→	mark(X)	(3)
          a__fib1(X1,X2)	→	fib1(X1,X2)	(16)
          a__add(X1,X2)	→	add(X1,X2)	(17)
          a__sel(0,cons(X,XS))	→	mark(X)	(5)
          mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(10)
          mark(fib(X))	→	a__fib(mark(X))	(7)
          a__fib(X)	→	fib(X)	(14)
          mark(0)	→	0	(12)
          mark(s(X))	→	s(mark(X))	(11)
          mark(fib1(X1,X2))	→	a__fib1(mark(X1),mark(X2))	(9)
          mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
          a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(6)
          a__fib1(X,Y)	→	cons(mark(X),fib1(Y,add(X,Y)))	(2)

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

          a__add#(s(X),Y)	→	mark#(Y)	(27)
          a__add#(s(X),Y)	→	mark#(X)	(23)
          a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(24)
          a__add#(0,X)	→	mark#(X)	(36)
          mark#(add(X1,X2))	→	mark#(X2)	(26)
          mark#(add(X1,X2))	→	mark#(X1)	(20)
          mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(25)
          mark#(s(X))	→	mark#(X)	(21)

          could be deleted.

          1.1.1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 0 components.