Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_Luc02a_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#(half(X))	→	mark#(X)	(63)
  a__sqr#(s(X))	→	mark#(X)	(43)
  a__half#(s(s(X)))	→	a__half#(mark(X))	(62)
  mark#(sqr(X))	→	a__sqr#(mark(X))	(42)
  mark#(s(X))	→	mark#(X)	(41)
  mark#(dbl(X))	→	a__dbl#(mark(X))	(61)
  mark#(sqr(X))	→	mark#(X)	(40)
  a__dbl#(s(X))	→	a__dbl#(mark(X))	(39)
  mark#(cons(X1,X2))	→	mark#(X1)	(60)
  a__add#(0,X)	→	mark#(X)	(59)
  a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
  a__first#(s(X),cons(Y,Z))	→	mark#(Y)	(58)
  a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
  mark#(dbl(X))	→	mark#(X)	(57)
  mark#(add(X1,X2))	→	mark#(X1)	(56)
  a__sqr#(s(X))	→	a__dbl#(mark(X))	(55)
  a__add#(s(X),Y)	→	mark#(Y)	(36)
  a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)
  a__dbl#(s(X))	→	mark#(X)	(34)
  mark#(first(X1,X2))	→	a__first#(mark(X1),mark(X2))	(53)
  mark#(recip(X))	→	mark#(X)	(54)
  mark#(half(X))	→	a__half#(mark(X))	(52)
  mark#(terms(X))	→	a__terms#(mark(X))	(33)
  a__sqr#(s(X))	→	mark#(X)	(43)
  mark#(first(X1,X2))	→	mark#(X2)	(51)
  mark#(add(X1,X2))	→	mark#(X2)	(50)
  a__terms#(N)	→	a__sqr#(mark(N))	(49)
  a__half#(s(s(X)))	→	mark#(X)	(48)
  mark#(first(X1,X2))	→	mark#(X1)	(47)
  a__add#(s(X),Y)	→	mark#(X)	(46)
  mark#(terms(X))	→	mark#(X)	(45)
  a__terms#(N)	→	mark#(N)	(32)
  a__half#(dbl(X))	→	mark#(X)	(31)
  mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 0
  [a__first#(x1, x2)]	=	max(x1 + 20205, x2 + 20203, 0)
  [recip(x1)]	=	x1 + 1
  [dbl(x1)]	=	x1 + 0
  [a__half(x1)]	=	x1 + 0
  [a__add#(x1, x2)]	=	max(x1 + 19335, x2 + 19335, 0)
  [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__dbl(x1)]	=	x1 + 0
  [a__half#(x1)]	=	x1 + 19335
  [a__sqr(x1)]	=	x1 + 0
  [half(x1)]	=	x1 + 0
  [a__terms#(x1)]	=	x1 + 19336
  [mark#(x1)]	=	x1 + 19335
  [0]	=	0
  [nil]	=	0
  [a__dbl#(x1)]	=	x1 + 19335
  [mark(x1)]	=	x1 + 0
  [first(x1, x2)]	=	max(x1 + 870, x2 + 869, 0)
  [a__first(x1, x2)]	=	max(x1 + 870, x2 + 869, 0)
  [cons(x1, x2)]	=	max(x1 + 1, 0)
  [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [sqr(x1)]	=	x1 + 0
  [a__terms(x1)]	=	x1 + 29535
  [a__sqr#(x1)]	=	x1 + 19335
  [terms(x1)]	=	x1 + 29535

  together with the usable rules

  mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
  a__dbl(0)	→	0	(4)
  mark(sqr(X))	→	a__sqr(mark(X))	(15)
  a__first(0,X)	→	nil	(8)
  a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
  a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
  mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
  mark(recip(X))	→	recip(mark(X))	(21)
  a__sqr(X)	→	sqr(X)	(26)
  mark(half(X))	→	a__half(mark(X))	(19)
  mark(dbl(X))	→	a__dbl(mark(X))	(17)
  a__add(X1,X2)	→	add(X1,X2)	(27)
  mark(s(X))	→	s(mark(X))	(22)
  a__dbl(X)	→	dbl(X)	(28)
  a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
  a__half(0)	→	0	(10)
  a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
  a__terms(X)	→	terms(X)	(25)
  a__half(X)	→	half(X)	(30)
  mark(terms(X))	→	a__terms(mark(X))	(14)
  a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
  mark(0)	→	0	(23)
  mark(nil)	→	nil	(24)
  a__half(s(0))	→	0	(11)
  a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
  a__half(dbl(X))	→	mark(X)	(13)
  a__add(0,X)	→	mark(X)	(6)
  a__first(X1,X2)	→	first(X1,X2)	(29)
  a__sqr(0)	→	0	(2)

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

  mark#(cons(X1,X2))	→	mark#(X1)	(60)
  a__first#(s(X),cons(Y,Z))	→	mark#(Y)	(58)
  mark#(recip(X))	→	mark#(X)	(54)
  mark#(terms(X))	→	a__terms#(mark(X))	(33)
  mark#(first(X1,X2))	→	mark#(X2)	(51)
  a__terms#(N)	→	a__sqr#(mark(N))	(49)
  mark#(first(X1,X2))	→	mark#(X1)	(47)
  mark#(terms(X))	→	mark#(X)	(45)
  a__terms#(N)	→	mark#(N)	(32)

  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

    mark#(sqr(X))	→	mark#(X)	(40)
    mark#(sqr(X))	→	a__sqr#(mark(X))	(42)
    a__sqr#(s(X))	→	mark#(X)	(43)
    a__sqr#(s(X))	→	a__dbl#(mark(X))	(55)
    a__sqr#(s(X))	→	mark#(X)	(43)
    a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
    a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
    mark#(add(X1,X2))	→	mark#(X2)	(50)
    mark#(add(X1,X2))	→	mark#(X1)	(56)
    mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)
    mark#(half(X))	→	mark#(X)	(63)
    mark#(half(X))	→	a__half#(mark(X))	(52)
    mark#(dbl(X))	→	mark#(X)	(57)
    mark#(dbl(X))	→	a__dbl#(mark(X))	(61)
    mark#(s(X))	→	mark#(X)	(41)
    a__dbl#(s(X))	→	mark#(X)	(34)
    a__dbl#(s(X))	→	a__dbl#(mark(X))	(39)
    a__add#(s(X),Y)	→	mark#(Y)	(36)
    a__add#(s(X),Y)	→	mark#(X)	(46)
    a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)
    a__half#(s(s(X)))	→	mark#(X)	(48)
    a__half#(s(s(X)))	→	a__half#(mark(X))	(62)
    a__half#(dbl(X))	→	mark#(X)	(31)
    a__add#(0,X)	→	mark#(X)	(59)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [s(x1)]	=	x1 + 0
    [a__first#(x1, x2)]	=	max(x1 + 20205, x2 + 20203, 0)
    [recip(x1)]	=	x1 + 31112
    [dbl(x1)]	=	x1 + 0
    [a__half(x1)]	=	x1 + 1
    [a__add#(x1, x2)]	=	max(x1 + 28163, x2 + 28163, 0)
    [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [a__dbl(x1)]	=	x1 + 0
    [a__half#(x1)]	=	x1 + 28163
    [a__sqr(x1)]	=	x1 + 0
    [half(x1)]	=	x1 + 1
    [a__terms#(x1)]	=	x1 + 19336
    [mark#(x1)]	=	x1 + 28163
    [0]	=	0
    [nil]	=	0
    [a__dbl#(x1)]	=	x1 + 28163
    [mark(x1)]	=	x1 + 0
    [first(x1, x2)]	=	max(x1 + 2, x2 + 1, 0)
    [a__first(x1, x2)]	=	max(x1 + 2, x2 + 1, 0)
    [cons(x1, x2)]	=	max(x1 + 1, 0)
    [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [sqr(x1)]	=	x1 + 0
    [a__terms(x1)]	=	x1 + 43325
    [a__sqr#(x1)]	=	x1 + 28163
    [terms(x1)]	=	x1 + 43325

    together with the usable rules

    mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
    a__dbl(0)	→	0	(4)
    mark(sqr(X))	→	a__sqr(mark(X))	(15)
    a__first(0,X)	→	nil	(8)
    a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
    a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
    mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
    mark(recip(X))	→	recip(mark(X))	(21)
    a__sqr(X)	→	sqr(X)	(26)
    mark(half(X))	→	a__half(mark(X))	(19)
    mark(dbl(X))	→	a__dbl(mark(X))	(17)
    a__add(X1,X2)	→	add(X1,X2)	(27)
    mark(s(X))	→	s(mark(X))	(22)
    a__dbl(X)	→	dbl(X)	(28)
    a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
    a__half(0)	→	0	(10)
    a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
    a__terms(X)	→	terms(X)	(25)
    a__half(X)	→	half(X)	(30)
    mark(terms(X))	→	a__terms(mark(X))	(14)
    a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
    mark(0)	→	0	(23)
    mark(nil)	→	nil	(24)
    a__half(s(0))	→	0	(11)
    a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
    a__half(dbl(X))	→	mark(X)	(13)
    a__add(0,X)	→	mark(X)	(6)
    a__first(X1,X2)	→	first(X1,X2)	(29)
    a__sqr(0)	→	0	(2)

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

    mark#(half(X))	→	mark#(X)	(63)
    mark#(half(X))	→	a__half#(mark(X))	(52)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 2 components.

    • The 1^st component contains the pair

      a__half#(s(s(X)))

      →

      a__half#(mark(X))

      (62)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the argument filter

      π(a__first#)	=	2
      π(a__half)	=	1
      π(a__half#)	=	1
      π(half)	=	1
      π(mark)	=	1

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

      prec(s)	=	0		status(s)	=	[1]		list-extension(s)	=	Lex
      prec(recip)	=	2		status(recip)	=	[]		list-extension(recip)	=	Lex
      prec(dbl)	=	2		status(dbl)	=	[1]		list-extension(dbl)	=	Lex
      prec(a__add#)	=	0		status(a__add#)	=	[1, 2]		list-extension(a__add#)	=	Lex
      prec(a__add)	=	1		status(a__add)	=	[2, 1]		list-extension(a__add)	=	Lex
      prec(a__dbl)	=	2		status(a__dbl)	=	[1]		list-extension(a__dbl)	=	Lex
      prec(a__sqr)	=	2		status(a__sqr)	=	[1]		list-extension(a__sqr)	=	Lex
      prec(a__terms#)	=	0		status(a__terms#)	=	[]		list-extension(a__terms#)	=	Lex
      prec(mark#)	=	0		status(mark#)	=	[]		list-extension(mark#)	=	Lex
      prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
      prec(nil)	=	0		status(nil)	=	[]		list-extension(nil)	=	Lex
      prec(a__dbl#)	=	0		status(a__dbl#)	=	[]		list-extension(a__dbl#)	=	Lex
      prec(first)	=	0		status(first)	=	[]		list-extension(first)	=	Lex
      prec(a__first)	=	0		status(a__first)	=	[]		list-extension(a__first)	=	Lex
      prec(cons)	=	0		status(cons)	=	[]		list-extension(cons)	=	Lex
      prec(add)	=	1		status(add)	=	[2, 1]		list-extension(add)	=	Lex
      prec(sqr)	=	2		status(sqr)	=	[1]		list-extension(sqr)	=	Lex
      prec(a__terms)	=	2		status(a__terms)	=	[1]		list-extension(a__terms)	=	Lex
      prec(a__sqr#)	=	0		status(a__sqr#)	=	[]		list-extension(a__sqr#)	=	Lex
      prec(terms)	=	2		status(terms)	=	[1]		list-extension(terms)	=	Lex

      and the following Max-polynomial interpretation

      [s(x1)]	=	x1 + 0
      [recip(x1)]	=	0
      [dbl(x1)]	=	x1 + 0
      [a__add#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__dbl(x1)]	=	x1 + 0
      [a__sqr(x1)]	=	x1 + 0
      [a__terms#(x1)]	=	0
      [mark#(x1)]	=	0
      [0]	=	0
      [nil]	=	0
      [a__dbl#(x1)]	=	0
      [first(x1, x2)]	=	max(0)
      [a__first(x1, x2)]	=	max(0)
      [cons(x1, x2)]	=	max(0)
      [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [sqr(x1)]	=	x1 + 0
      [a__terms(x1)]	=	x1 + 0
      [a__sqr#(x1)]	=	0
      [terms(x1)]	=	x1 + 0

      together with the usable rules

      mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
      a__dbl(0)	→	0	(4)
      mark(sqr(X))	→	a__sqr(mark(X))	(15)
      a__first(0,X)	→	nil	(8)
      a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
      a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
      mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
      mark(recip(X))	→	recip(mark(X))	(21)
      a__sqr(X)	→	sqr(X)	(26)
      mark(half(X))	→	a__half(mark(X))	(19)
      mark(dbl(X))	→	a__dbl(mark(X))	(17)
      a__add(X1,X2)	→	add(X1,X2)	(27)
      mark(s(X))	→	s(mark(X))	(22)
      a__dbl(X)	→	dbl(X)	(28)
      a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
      a__half(0)	→	0	(10)
      a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
      a__terms(X)	→	terms(X)	(25)
      a__half(X)	→	half(X)	(30)
      mark(terms(X))	→	a__terms(mark(X))	(14)
      a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
      mark(0)	→	0	(23)
      mark(nil)	→	nil	(24)
      a__half(s(0))	→	0	(11)
      a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
      a__half(dbl(X))	→	mark(X)	(13)
      a__add(0,X)	→	mark(X)	(6)
      a__first(X1,X2)	→	first(X1,X2)	(29)
      a__sqr(0)	→	0	(2)

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

      a__half#(s(s(X)))

      →

      a__half#(mark(X))

      (62)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.

    • The 2^nd component contains the pair

      mark#(sqr(X))	→	mark#(X)	(40)
      mark#(sqr(X))	→	a__sqr#(mark(X))	(42)
      a__sqr#(s(X))	→	mark#(X)	(43)
      a__sqr#(s(X))	→	a__dbl#(mark(X))	(55)
      a__sqr#(s(X))	→	mark#(X)	(43)
      a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
      a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
      mark#(add(X1,X2))	→	mark#(X2)	(50)
      mark#(add(X1,X2))	→	mark#(X1)	(56)
      mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)
      mark#(dbl(X))	→	mark#(X)	(57)
      mark#(dbl(X))	→	a__dbl#(mark(X))	(61)
      mark#(s(X))	→	mark#(X)	(41)
      a__dbl#(s(X))	→	mark#(X)	(34)
      a__dbl#(s(X))	→	a__dbl#(mark(X))	(39)
      a__add#(s(X),Y)	→	mark#(Y)	(36)
      a__add#(s(X),Y)	→	mark#(X)	(46)
      a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)
      a__add#(0,X)	→	mark#(X)	(59)

      1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [s(x1)]	=	x1 + 0
      [a__first#(x1, x2)]	=	max(0)
      [recip(x1)]	=	1
      [dbl(x1)]	=	x1 + 1
      [a__half(x1)]	=	x1 + 1
      [a__add#(x1, x2)]	=	max(x1 + 48491, x2 + 48491, 0)
      [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [a__dbl(x1)]	=	x1 + 1
      [a__half#(x1)]	=	28163
      [a__sqr(x1)]	=	x1 + 1
      [half(x1)]	=	x1 + 1
      [a__terms#(x1)]	=	19336
      [mark#(x1)]	=	x1 + 48491
      [0]	=	1
      [nil]	=	12701
      [a__dbl#(x1)]	=	x1 + 48492
      [mark(x1)]	=	x1 + 0
      [first(x1, x2)]	=	max(x1 + 46869, 0)
      [a__first(x1, x2)]	=	max(x1 + 46869, 0)
      [cons(x1, x2)]	=	max(0)
      [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
      [sqr(x1)]	=	x1 + 1
      [a__terms(x1)]	=	49364
      [a__sqr#(x1)]	=	x1 + 48492
      [terms(x1)]	=	49364

      together with the usable rules

      mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
      a__dbl(0)	→	0	(4)
      mark(sqr(X))	→	a__sqr(mark(X))	(15)
      a__first(0,X)	→	nil	(8)
      a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
      a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
      mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
      mark(recip(X))	→	recip(mark(X))	(21)
      a__sqr(X)	→	sqr(X)	(26)
      mark(half(X))	→	a__half(mark(X))	(19)
      mark(dbl(X))	→	a__dbl(mark(X))	(17)
      a__add(X1,X2)	→	add(X1,X2)	(27)
      mark(s(X))	→	s(mark(X))	(22)
      a__dbl(X)	→	dbl(X)	(28)
      a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
      a__half(0)	→	0	(10)
      a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
      a__terms(X)	→	terms(X)	(25)
      a__half(X)	→	half(X)	(30)
      mark(terms(X))	→	a__terms(mark(X))	(14)
      a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
      mark(0)	→	0	(23)
      mark(nil)	→	nil	(24)
      a__half(s(0))	→	0	(11)
      a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
      a__half(dbl(X))	→	mark(X)	(13)
      a__add(0,X)	→	mark(X)	(6)
      a__first(X1,X2)	→	first(X1,X2)	(29)
      a__sqr(0)	→	0	(2)

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

      mark#(sqr(X))	→	mark#(X)	(40)
      a__sqr#(s(X))	→	mark#(X)	(43)
      a__sqr#(s(X))	→	mark#(X)	(43)
      mark#(dbl(X))	→	mark#(X)	(57)
      a__dbl#(s(X))	→	mark#(X)	(34)

      could be deleted.

      1.1.1.1.1.1.2.1 Dependency Graph Processor

      The dependency pairs are split into 2 components.

      • The 1^st component contains the pair

        mark#(sqr(X))	→	a__sqr#(mark(X))	(42)
        a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
        a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
        mark#(add(X1,X2))	→	mark#(X2)	(50)
        mark#(add(X1,X2))	→	mark#(X1)	(56)
        mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)
        mark#(s(X))	→	mark#(X)	(41)
        a__add#(s(X),Y)	→	mark#(Y)	(36)
        a__add#(s(X),Y)	→	mark#(X)	(46)
        a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)
        a__add#(0,X)	→	mark#(X)	(59)

        1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [s(x1)]	=	x1 + 0
        [a__first#(x1, x2)]	=	max(0)
        [recip(x1)]	=	1
        [dbl(x1)]	=	x1 + 1
        [a__half(x1)]	=	x1 + 1
        [a__add#(x1, x2)]	=	max(x1 + 35955, x2 + 35956, 0)
        [a__add(x1, x2)]	=	max(x1 + 0, x2 + 1, 0)
        [a__dbl(x1)]	=	x1 + 1
        [a__half#(x1)]	=	28163
        [a__sqr(x1)]	=	x1 + 3
        [half(x1)]	=	x1 + 1
        [a__terms#(x1)]	=	19336
        [mark#(x1)]	=	x1 + 35955
        [0]	=	1
        [nil]	=	2
        [a__dbl#(x1)]	=	x1 + 48492
        [mark(x1)]	=	x1 + 0
        [first(x1, x2)]	=	max(x1 + 1, 0)
        [a__first(x1, x2)]	=	max(x1 + 1, 0)
        [cons(x1, x2)]	=	max(0)
        [add(x1, x2)]	=	max(x1 + 0, x2 + 1, 0)
        [sqr(x1)]	=	x1 + 3
        [a__terms(x1)]	=	44798
        [a__sqr#(x1)]	=	x1 + 35958
        [terms(x1)]	=	44798

        together with the usable rules

        mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
        a__dbl(0)	→	0	(4)
        mark(sqr(X))	→	a__sqr(mark(X))	(15)
        a__first(0,X)	→	nil	(8)
        a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
        a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
        mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
        mark(recip(X))	→	recip(mark(X))	(21)
        a__sqr(X)	→	sqr(X)	(26)
        mark(half(X))	→	a__half(mark(X))	(19)
        mark(dbl(X))	→	a__dbl(mark(X))	(17)
        a__add(X1,X2)	→	add(X1,X2)	(27)
        mark(s(X))	→	s(mark(X))	(22)
        a__dbl(X)	→	dbl(X)	(28)
        a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
        a__half(0)	→	0	(10)
        a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
        a__terms(X)	→	terms(X)	(25)
        a__half(X)	→	half(X)	(30)
        mark(terms(X))	→	a__terms(mark(X))	(14)
        a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
        mark(0)	→	0	(23)
        mark(nil)	→	nil	(24)
        a__half(s(0))	→	0	(11)
        a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
        a__half(dbl(X))	→	mark(X)	(13)
        a__add(0,X)	→	mark(X)	(6)
        a__first(X1,X2)	→	first(X1,X2)	(29)
        a__sqr(0)	→	0	(2)

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

        mark#(add(X1,X2))	→	mark#(X2)	(50)
        a__add#(s(X),Y)	→	mark#(Y)	(36)
        a__add#(0,X)	→	mark#(X)	(59)

        could be deleted.

        1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          mark#(sqr(X))	→	a__sqr#(mark(X))	(42)
          a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
          a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
          mark#(add(X1,X2))	→	mark#(X1)	(56)
          mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)
          mark#(s(X))	→	mark#(X)	(41)
          a__add#(s(X),Y)	→	mark#(X)	(46)
          a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)

          1.1.1.1.1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the argument filter

          π(a__first#)	=	2
          π(a__half)	=	1
          π(a__add#)	=	1
          π(half)	=	1
          π(mark#)	=	1
          π(mark)	=	1

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

          prec(s)	=	1		status(s)	=	[1]		list-extension(s)	=	Lex
          prec(recip)	=	4		status(recip)	=	[]		list-extension(recip)	=	Lex
          prec(dbl)	=	3		status(dbl)	=	[1]		list-extension(dbl)	=	Lex
          prec(a__add)	=	2		status(a__add)	=	[1, 2]		list-extension(a__add)	=	Lex
          prec(a__dbl)	=	3		status(a__dbl)	=	[1]		list-extension(a__dbl)	=	Lex
          prec(a__half#)	=	0		status(a__half#)	=	[]		list-extension(a__half#)	=	Lex
          prec(a__sqr)	=	4		status(a__sqr)	=	[1]		list-extension(a__sqr)	=	Lex
          prec(a__terms#)	=	0		status(a__terms#)	=	[]		list-extension(a__terms#)	=	Lex
          prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
          prec(nil)	=	0		status(nil)	=	[]		list-extension(nil)	=	Lex
          prec(a__dbl#)	=	0		status(a__dbl#)	=	[]		list-extension(a__dbl#)	=	Lex
          prec(first)	=	0		status(first)	=	[]		list-extension(first)	=	Lex
          prec(a__first)	=	0		status(a__first)	=	[]		list-extension(a__first)	=	Lex
          prec(cons)	=	0		status(cons)	=	[]		list-extension(cons)	=	Lex
          prec(add)	=	2		status(add)	=	[1, 2]		list-extension(add)	=	Lex
          prec(sqr)	=	4		status(sqr)	=	[1]		list-extension(sqr)	=	Lex
          prec(a__terms)	=	4		status(a__terms)	=	[1]		list-extension(a__terms)	=	Lex
          prec(a__sqr#)	=	4		status(a__sqr#)	=	[1]		list-extension(a__sqr#)	=	Lex
          prec(terms)	=	4		status(terms)	=	[1]		list-extension(terms)	=	Lex

          and the following Max-polynomial interpretation

          [s(x1)]	=	x1 + 0
          [recip(x1)]	=	0
          [dbl(x1)]	=	x1 + 0
          [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
          [a__dbl(x1)]	=	x1 + 0
          [a__half#(x1)]	=	0
          [a__sqr(x1)]	=	x1 + 0
          [a__terms#(x1)]	=	0
          [0]	=	0
          [nil]	=	0
          [a__dbl#(x1)]	=	0
          [first(x1, x2)]	=	max(0)
          [a__first(x1, x2)]	=	max(0)
          [cons(x1, x2)]	=	max(0)
          [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
          [sqr(x1)]	=	x1 + 0
          [a__terms(x1)]	=	x1 + 0
          [a__sqr#(x1)]	=	x1 + 0
          [terms(x1)]	=	x1 + 0

          together with the usable rules

          mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
          a__dbl(0)	→	0	(4)
          mark(sqr(X))	→	a__sqr(mark(X))	(15)
          a__first(0,X)	→	nil	(8)
          a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
          a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
          mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
          mark(recip(X))	→	recip(mark(X))	(21)
          a__sqr(X)	→	sqr(X)	(26)
          mark(half(X))	→	a__half(mark(X))	(19)
          mark(dbl(X))	→	a__dbl(mark(X))	(17)
          a__add(X1,X2)	→	add(X1,X2)	(27)
          mark(s(X))	→	s(mark(X))	(22)
          a__dbl(X)	→	dbl(X)	(28)
          a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
          a__half(0)	→	0	(10)
          a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
          mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
          a__terms(X)	→	terms(X)	(25)
          a__half(X)	→	half(X)	(30)
          mark(terms(X))	→	a__terms(mark(X))	(14)
          a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
          mark(0)	→	0	(23)
          mark(nil)	→	nil	(24)
          a__half(s(0))	→	0	(11)
          a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
          a__half(dbl(X))	→	mark(X)	(13)
          a__add(0,X)	→	mark(X)	(6)
          a__first(X1,X2)	→	first(X1,X2)	(29)
          a__sqr(0)	→	0	(2)

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

          a__sqr#(s(X))	→	a__sqr#(mark(X))	(37)
          a__sqr#(s(X))	→	a__add#(a__sqr(mark(X)),a__dbl(mark(X)))	(38)
          mark#(add(X1,X2))	→	mark#(X1)	(56)
          mark#(add(X1,X2))	→	a__add#(mark(X1),mark(X2))	(44)
          mark#(s(X))	→	mark#(X)	(41)
          a__add#(s(X),Y)	→	mark#(X)	(46)
          a__add#(s(X),Y)	→	a__add#(mark(X),mark(Y))	(35)

          could be deleted.

          1.1.1.1.1.1.2.1.1.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 0 components.

      • The 2^nd component contains the pair

        a__dbl#(s(X))

        →

        a__dbl#(mark(X))

        (39)

        1.1.1.1.1.1.2.1.2 Reduction Pair Processor with Usable Rules

        Using the argument filter

        π(a__first#)	=	2
        π(a__half)	=	1
        π(a__add#)	=	1
        π(half)	=	1
        π(mark#)	=	1
        π(mark)	=	1

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

        prec(s)	=	1		status(s)	=	[1]		list-extension(s)	=	Lex
        prec(recip)	=	4		status(recip)	=	[]		list-extension(recip)	=	Lex
        prec(dbl)	=	3		status(dbl)	=	[1]		list-extension(dbl)	=	Lex
        prec(a__add)	=	2		status(a__add)	=	[1, 2]		list-extension(a__add)	=	Lex
        prec(a__dbl)	=	3		status(a__dbl)	=	[1]		list-extension(a__dbl)	=	Lex
        prec(a__half#)	=	0		status(a__half#)	=	[]		list-extension(a__half#)	=	Lex
        prec(a__sqr)	=	4		status(a__sqr)	=	[1]		list-extension(a__sqr)	=	Lex
        prec(a__terms#)	=	0		status(a__terms#)	=	[]		list-extension(a__terms#)	=	Lex
        prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
        prec(nil)	=	0		status(nil)	=	[]		list-extension(nil)	=	Lex
        prec(a__dbl#)	=	0		status(a__dbl#)	=	[1]		list-extension(a__dbl#)	=	Lex
        prec(first)	=	0		status(first)	=	[]		list-extension(first)	=	Lex
        prec(a__first)	=	0		status(a__first)	=	[]		list-extension(a__first)	=	Lex
        prec(cons)	=	0		status(cons)	=	[]		list-extension(cons)	=	Lex
        prec(add)	=	2		status(add)	=	[1, 2]		list-extension(add)	=	Lex
        prec(sqr)	=	4		status(sqr)	=	[1]		list-extension(sqr)	=	Lex
        prec(a__terms)	=	4		status(a__terms)	=	[1]		list-extension(a__terms)	=	Lex
        prec(a__sqr#)	=	4		status(a__sqr#)	=	[1]		list-extension(a__sqr#)	=	Lex
        prec(terms)	=	4		status(terms)	=	[1]		list-extension(terms)	=	Lex

        and the following Max-polynomial interpretation

        [s(x1)]	=	x1 + 0
        [recip(x1)]	=	0
        [dbl(x1)]	=	x1 + 0
        [a__add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [a__dbl(x1)]	=	x1 + 0
        [a__half#(x1)]	=	0
        [a__sqr(x1)]	=	x1 + 0
        [a__terms#(x1)]	=	0
        [0]	=	0
        [nil]	=	0
        [a__dbl#(x1)]	=	x1 + 0
        [first(x1, x2)]	=	max(0)
        [a__first(x1, x2)]	=	max(0)
        [cons(x1, x2)]	=	max(0)
        [add(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
        [sqr(x1)]	=	x1 + 0
        [a__terms(x1)]	=	x1 + 0
        [a__sqr#(x1)]	=	x1 + 0
        [terms(x1)]	=	x1 + 0

        together with the usable rules

        mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
        a__dbl(0)	→	0	(4)
        mark(sqr(X))	→	a__sqr(mark(X))	(15)
        a__first(0,X)	→	nil	(8)
        a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
        a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
        mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
        mark(recip(X))	→	recip(mark(X))	(21)
        a__sqr(X)	→	sqr(X)	(26)
        mark(half(X))	→	a__half(mark(X))	(19)
        mark(dbl(X))	→	a__dbl(mark(X))	(17)
        a__add(X1,X2)	→	add(X1,X2)	(27)
        mark(s(X))	→	s(mark(X))	(22)
        a__dbl(X)	→	dbl(X)	(28)
        a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
        a__half(0)	→	0	(10)
        a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
        mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
        a__terms(X)	→	terms(X)	(25)
        a__half(X)	→	half(X)	(30)
        mark(terms(X))	→	a__terms(mark(X))	(14)
        a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
        mark(0)	→	0	(23)
        mark(nil)	→	nil	(24)
        a__half(s(0))	→	0	(11)
        a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
        a__half(dbl(X))	→	mark(X)	(13)
        a__add(0,X)	→	mark(X)	(6)
        a__first(X1,X2)	→	first(X1,X2)	(29)
        a__sqr(0)	→	0	(2)

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

        a__dbl#(s(X))

        →

        a__dbl#(mark(X))

        (39)

        could be deleted.

        1.1.1.1.1.1.2.1.2.1 Dependency Graph Processor

        The dependency pairs are split into 0 components.