Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_Z)

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

  activate#(n__sieve(X))	→	sieve#(X)	(23)
  filter#(cons(X,Y),0,M)	→	activate#(Y)	(22)
  filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(21)
  sieve#(cons(s(N),Y))	→	filter#(activate(Y),N,N)	(16)
  activate#(n__filter(X1,X2,X3))	→	filter#(X1,X2,X3)	(15)
  sieve#(cons(s(N),Y))	→	activate#(Y)	(18)
  sieve#(cons(0,Y))	→	activate#(Y)	(17)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [zprimes]	=	0
  [nats#(x1)]	=	0
  [s(x1)]	=	1
  [activate(x1)]	=	x1 + 0
  [filter#(x1, x2, x3)]	=	x1 + 0
  [activate#(x1)]	=	x1 + 0
  [zprimes#]	=	0
  [n__nats(x1)]	=	41063
  [0]	=	1
  [n__filter(x1, x2, x3)]	=	x1 + 0
  [sieve(x1)]	=	x1 + 32287
  [n__sieve(x1)]	=	x1 + 32287
  [nats(x1)]	=	41063
  [cons(x1, x2)]	=	x2 + 0
  [filter(x1, x2, x3)]	=	x1 + 0
  [sieve#(x1)]	=	x1 + 1

  together with the usable rules

  sieve(cons(s(N),Y))	→	cons(s(N),n__sieve(filter(activate(Y),N,N)))	(4)
  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(s(N)))	(5)
  activate(n__filter(X1,X2,X3))	→	filter(X1,X2,X3)	(10)
  filter(X1,X2,X3)	→	n__filter(X1,X2,X3)	(7)
  activate(n__nats(X))	→	nats(X)	(12)
  activate(n__sieve(X))	→	sieve(X)	(11)
  nats(X)	→	n__nats(X)	(9)
  activate(X)	→	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

  activate#(n__sieve(X))	→	sieve#(X)	(23)
  sieve#(cons(s(N),Y))	→	filter#(activate(Y),N,N)	(16)
  sieve#(cons(s(N),Y))	→	activate#(Y)	(18)
  sieve#(cons(0,Y))	→	activate#(Y)	(17)

  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)	(22)
    activate#(n__filter(X1,X2,X3))	→	filter#(X1,X2,X3)	(15)
    filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(21)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [zprimes]	=	0
    [nats#(x1)]	=	0
    [s(x1)]	=	1
    [activate(x1)]	=	x1 + 1
    [filter#(x1, x2, x3)]	=	x1 + 0
    [activate#(x1)]	=	x1 + 0
    [zprimes#]	=	0
    [n__nats(x1)]	=	24653
    [0]	=	2
    [n__filter(x1, x2, x3)]	=	x1 + x3 + 14681
    [sieve(x1)]	=	52869
    [n__sieve(x1)]	=	52868
    [nats(x1)]	=	24654
    [cons(x1, x2)]	=	x2 + 1
    [filter(x1, x2, x3)]	=	x1 + x3 + 14682
    [sieve#(x1)]	=	1

    together with the usable rules

    sieve(cons(s(N),Y))	→	cons(s(N),n__sieve(filter(activate(Y),N,N)))	(4)
    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(s(N)))	(5)
    activate(n__filter(X1,X2,X3))	→	filter(X1,X2,X3)	(10)
    filter(X1,X2,X3)	→	n__filter(X1,X2,X3)	(7)
    activate(n__nats(X))	→	nats(X)	(12)
    activate(n__sieve(X))	→	sieve(X)	(11)
    nats(X)	→	n__nats(X)	(9)
    activate(X)	→	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)	(22)
    activate#(n__filter(X1,X2,X3))	→	filter#(X1,X2,X3)	(15)
    filter#(cons(X,Y),s(N),M)	→	activate#(Y)	(21)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.