Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_FR)

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

  sieve#(cons(s(N),Y))	→	activate#(Y)	(33)
  activate#(n__s(X))	→	activate#(X)	(31)
  activate#(n__sieve(X))	→	sieve#(activate(X))	(21)
  activate#(n__filter(X1,X2,X3))	→	filter#(activate(X1),activate(X2),activate(X3))	(30)
  filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(29)
  sieve#(cons(0,Y))	→	activate#(Y)	(27)
  activate#(n__filter(X1,X2,X3))	→	activate#(X3)	(20)
  activate#(n__filter(X1,X2,X3))	→	activate#(X1)	(19)
  activate#(n__sieve(X))	→	activate#(X)	(18)
  filter#(cons(X,Y),0,M)	→	activate#(Y)	(26)
  activate#(n__filter(X1,X2,X3))	→	activate#(X2)	(24)
  activate#(n__nats(X))	→	activate#(X)	(23)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [zprimes]	=	0
  [nats#(x1)]	=	0
  [s(x1)]	=	x1 + 0
  [activate(x1)]	=	x1 + 0
  [filter#(x1, x2, x3)]	=	max(x1 + 1, x2 + 2, x3 + 3, 0)
  [activate#(x1)]	=	x1 + 1
  [zprimes#]	=	0
  [n__nats(x1)]	=	x1 + 40653
  [n__s(x1)]	=	x1 + 0
  [0]	=	0
  [s#(x1)]	=	0
  [n__filter(x1, x2, x3)]	=	max(x1 + 0, x2 + 1, x3 + 2, 0)
  [sieve(x1)]	=	x1 + 10452
  [n__sieve(x1)]	=	x1 + 10452
  [nats(x1)]	=	x1 + 40653
  [cons(x1, x2)]	=	max(x1 + 32288, x2 + 0, 0)
  [filter(x1, x2, x3)]	=	max(x1 + 0, x2 + 1, x3 + 2, 0)
  [sieve#(x1)]	=	x1 + 2

  together with the usable rules

  sieve(cons(s(N),Y))	→	cons(s(N),n__sieve(n__filter(activate(Y),N,N)))	(4)
  activate(X)	→	X	(15)
  sieve(X)	→	n__sieve(X)	(8)
  filter(cons(X,Y),0,M)	→	cons(0,n__filter(activate(Y),M,M))	(1)
  sieve(cons(0,Y))	→	cons(0,n__sieve(activate(Y)))	(3)
  nats(N)	→	cons(N,n__nats(n__s(N)))	(5)
  s(X)	→	n__s(X)	(10)
  filter(X1,X2,X3)	→	n__filter(X1,X2,X3)	(7)
  activate(n__s(X))	→	s(activate(X))	(14)
  activate(n__sieve(X))	→	sieve(activate(X))	(12)
  activate(n__filter(X1,X2,X3))	→	filter(activate(X1),activate(X2),activate(X3))	(11)
  nats(X)	→	n__nats(X)	(9)
  activate(n__nats(X))	→	nats(activate(X))	(13)
  filter(cons(X,Y),s(N),M)	→	cons(X,n__filter(activate(Y),N,M))	(2)

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

  sieve#(cons(s(N),Y))	→	activate#(Y)	(33)
  activate#(n__sieve(X))	→	sieve#(activate(X))	(21)
  sieve#(cons(0,Y))	→	activate#(Y)	(27)
  activate#(n__filter(X1,X2,X3))	→	activate#(X3)	(20)
  activate#(n__sieve(X))	→	activate#(X)	(18)
  activate#(n__filter(X1,X2,X3))	→	activate#(X2)	(24)
  activate#(n__nats(X))	→	activate#(X)	(23)

  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

    filter#(cons(X,Y),0,M)	→	activate#(Y)	(26)
    activate#(n__s(X))	→	activate#(X)	(31)
    activate#(n__filter(X1,X2,X3))	→	activate#(X1)	(19)
    activate#(n__filter(X1,X2,X3))	→	filter#(activate(X1),activate(X2),activate(X3))	(30)
    filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(29)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [zprimes]	=	0
    [nats#(x1)]	=	0
    [s(x1)]	=	x1 + 31892
    [activate(x1)]	=	x1 + 0
    [filter#(x1, x2, x3)]	=	x1 + 25907
    [activate#(x1)]	=	x1 + 0
    [zprimes#]	=	0
    [n__nats(x1)]	=	19781
    [n__s(x1)]	=	x1 + 31892
    [0]	=	0
    [s#(x1)]	=	0
    [n__filter(x1, x2, x3)]	=	x1 + 25908
    [sieve(x1)]	=	50537
    [n__sieve(x1)]	=	50537
    [nats(x1)]	=	19781
    [cons(x1, x2)]	=	x2 + 0
    [filter(x1, x2, x3)]	=	x1 + 25908
    [sieve#(x1)]	=	0

    together with the usable rules

    sieve(cons(s(N),Y))	→	cons(s(N),n__sieve(n__filter(activate(Y),N,N)))	(4)
    activate(X)	→	X	(15)
    sieve(X)	→	n__sieve(X)	(8)
    filter(cons(X,Y),0,M)	→	cons(0,n__filter(activate(Y),M,M))	(1)
    sieve(cons(0,Y))	→	cons(0,n__sieve(activate(Y)))	(3)
    nats(N)	→	cons(N,n__nats(n__s(N)))	(5)
    s(X)	→	n__s(X)	(10)
    filter(X1,X2,X3)	→	n__filter(X1,X2,X3)	(7)
    activate(n__s(X))	→	s(activate(X))	(14)
    activate(n__sieve(X))	→	sieve(activate(X))	(12)
    activate(n__filter(X1,X2,X3))	→	filter(activate(X1),activate(X2),activate(X3))	(11)
    nats(X)	→	n__nats(X)	(9)
    activate(n__nats(X))	→	nats(activate(X))	(13)
    filter(cons(X,Y),s(N),M)	→	cons(X,n__filter(activate(Y),N,M))	(2)

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

    filter#(cons(X,Y),0,M)	→	activate#(Y)	(26)
    activate#(n__s(X))	→	activate#(X)	(31)
    activate#(n__filter(X1,X2,X3))	→	activate#(X1)	(19)
    activate#(n__filter(X1,X2,X3))	→	filter#(activate(X1),activate(X2),activate(X3))	(30)
    filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(29)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.