Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_C)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(92)
  top#(mark(X))	→	top#(proper(X))	(90)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [proper(x1)]	=	1 · x1
  [filter(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [cons(x1, x2)]	=	2 · x1 + 1 · x2
  [0]	=	0
  [ok(x1)]	=	2 · x1
  [s(x1)]	=	1 · x1
  [sieve(x1)]	=	2 · x1
  [nats(x1)]	=	2 · x1
  [zprimes]	=	0
  [mark(x1)]	=	1 · x1
  [active(x1)]	=	2 · x1
  [top#(x1)]	=	2 · x1

  together with the usable rules

  proper(filter(X1,X2,X3))	→	filter(proper(X1),proper(X2),proper(X3))	(21)
  proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(22)
  proper(0)	→	ok(0)	(23)
  proper(s(X))	→	s(proper(X))	(24)
  proper(sieve(X))	→	sieve(proper(X))	(25)
  proper(nats(X))	→	nats(proper(X))	(26)
  proper(zprimes)	→	ok(zprimes)	(27)
  nats(mark(X))	→	mark(nats(X))	(20)
  nats(ok(X))	→	ok(nats(X))	(32)
  sieve(mark(X))	→	mark(sieve(X))	(19)
  sieve(ok(X))	→	ok(sieve(X))	(31)
  s(mark(X))	→	mark(s(X))	(18)
  s(ok(X))	→	ok(s(X))	(30)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)
  filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
  filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
  filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
  filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
  active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
  active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)
  active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
  active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
  active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
  active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
  active(filter(X1,X2,X3))	→	filter(active(X1),X2,X3)	(7)
  active(filter(X1,X2,X3))	→	filter(X1,active(X2),X3)	(8)
  active(filter(X1,X2,X3))	→	filter(X1,X2,active(X3))	(9)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
  active(s(X))	→	s(active(X))	(11)
  active(sieve(X))	→	sieve(active(X))	(12)
  active(nats(X))	→	nats(active(X))	(13)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1 Reduction Pair Processor

  Using the

  prec(top#)	=	0		stat(top#)	=	lex
  prec(mark)	=	2		stat(mark)	=	lex
  prec(filter)	=	3		stat(filter)	=	lex
  prec(0)	=	1		stat(0)	=	lex
  prec(s)	=	2		stat(s)	=	lex
  prec(sieve)	=	2		stat(sieve)	=	lex
  prec(nats)	=	2		stat(nats)	=	lex
  prec(zprimes)	=	4		stat(zprimes)	=	lex

  π(top#)	=	[1]
  π(ok)	=	1
  π(active)	=	1
  π(mark)	=	[1]
  π(proper)	=	1
  π(filter)	=	[1,3,2]
  π(cons)	=	1
  π(0)	=	[]
  π(s)	=	[1]
  π(sieve)	=	[1]
  π(nats)	=	[1]
  π(zprimes)	=	[]

  the pair

  top#(mark(X))

  →

  top#(proper(X))

  (90)

  could be deleted.

  1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	2 · x1
  [filter(x1, x2, x3)]	=	2 · x1 + 1 · x2 + 2 · x3
  [cons(x1, x2)]	=	2 · x1 + 1 · x2
  [0]	=	0
  [mark(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [sieve(x1)]	=	2 · x1
  [nats(x1)]	=	2 · x1
  [zprimes]	=	0
  [ok(x1)]	=	2 · x1
  [top#(x1)]	=	2 · x1

  together with the usable rules

  active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
  active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)
  active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
  active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
  active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
  active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
  active(filter(X1,X2,X3))	→	filter(active(X1),X2,X3)	(7)
  active(filter(X1,X2,X3))	→	filter(X1,active(X2),X3)	(8)
  active(filter(X1,X2,X3))	→	filter(X1,X2,active(X3))	(9)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
  active(s(X))	→	s(active(X))	(11)
  active(sieve(X))	→	sieve(active(X))	(12)
  active(nats(X))	→	nats(active(X))	(13)
  nats(mark(X))	→	mark(nats(X))	(20)
  nats(ok(X))	→	ok(nats(X))	(32)
  sieve(mark(X))	→	mark(sieve(X))	(19)
  sieve(ok(X))	→	ok(sieve(X))	(31)
  s(mark(X))	→	mark(s(X))	(18)
  s(ok(X))	→	ok(s(X))	(30)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)
  filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
  filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
  filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
  filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)

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

  active(zprimes)

  →

  mark(sieve(nats(s(s(0)))))

  (6)

  could be deleted.

  1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 + 2 · x1
  [filter(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [cons(x1, x2)]	=	1 + 2 · x1 + 1 · x2
  [0]	=	0
  [mark(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [sieve(x1)]	=	1 + 2 · x1
  [nats(x1)]	=	1 + 2 · x1
  [ok(x1)]	=	2 + 2 · x1
  [top#(x1)]	=	1 · x1

  the pair

  top#(ok(X))

  →

  top#(active(X))

  (92)

  and the rules

  active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
  active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)
  active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
  active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
  active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
  nats(ok(X))	→	ok(nats(X))	(32)
  sieve(ok(X))	→	ok(sieve(X))	(31)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)
  filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)

  could be deleted.

  1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  active#(filter(X1,X2,X3))	→	active#(X2)	(54)
  active#(filter(X1,X2,X3))	→	active#(X1)	(52)
  active#(filter(X1,X2,X3))	→	active#(X3)	(56)
  active#(cons(X1,X2))	→	active#(X1)	(58)
  active#(s(X))	→	active#(X)	(60)
  active#(sieve(X))	→	active#(X)	(62)
  active#(nats(X))	→	active#(X)	(64)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [filter(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	1 · x1
  [sieve(x1)]	=	1 · x1
  [nats(x1)]	=	1 · x1
  [active#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.2.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  active#(filter(X1,X2,X3))	→	active#(X2)	(54)
  1	>	1
  active#(filter(X1,X2,X3))	→	active#(X1)	(52)
  1	>	1
  active#(filter(X1,X2,X3))	→	active#(X3)	(56)
  1	>	1
  active#(cons(X1,X2))	→	active#(X1)	(58)
  1	>	1
  active#(s(X))	→	active#(X)	(60)
  1	>	1
  active#(sieve(X))	→	active#(X)	(62)
  1	>	1
  active#(nats(X))	→	active#(X)	(64)
  1	>	1

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

• The 3^rd component contains the pair

  proper#(filter(X1,X2,X3))	→	proper#(X2)	(74)
  proper#(filter(X1,X2,X3))	→	proper#(X1)	(73)
  proper#(filter(X1,X2,X3))	→	proper#(X3)	(75)
  proper#(cons(X1,X2))	→	proper#(X1)	(77)
  proper#(cons(X1,X2))	→	proper#(X2)	(78)
  proper#(s(X))	→	proper#(X)	(80)
  proper#(sieve(X))	→	proper#(X)	(82)
  proper#(nats(X))	→	proper#(X)	(84)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [filter(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	1 · x1
  [sieve(x1)]	=	1 · x1
  [nats(x1)]	=	1 · x1
  [proper#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.3.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  proper#(filter(X1,X2,X3))	→	proper#(X2)	(74)
  1	>	1
  proper#(filter(X1,X2,X3))	→	proper#(X1)	(73)
  1	>	1
  proper#(filter(X1,X2,X3))	→	proper#(X3)	(75)
  1	>	1
  proper#(cons(X1,X2))	→	proper#(X1)	(77)
  1	>	1
  proper#(cons(X1,X2))	→	proper#(X2)	(78)
  1	>	1
  proper#(s(X))	→	proper#(X)	(80)
  1	>	1
  proper#(sieve(X))	→	proper#(X)	(82)
  1	>	1
  proper#(nats(X))	→	proper#(X)	(84)
  1	>	1

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

• The 4^th component contains the pair

  filter#(X1,mark(X2),X3)	→	filter#(X1,X2,X3)	(66)
  filter#(mark(X1),X2,X3)	→	filter#(X1,X2,X3)	(65)
  filter#(X1,X2,mark(X3))	→	filter#(X1,X2,X3)	(67)
  filter#(ok(X1),ok(X2),ok(X3))	→	filter#(X1,X2,X3)	(85)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [ok(x1)]	=	1 · x1
  [filter#(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.4.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  filter#(X1,mark(X2),X3)	→	filter#(X1,X2,X3)	(66)
  1	≥	1
  2	>	2
  3	≥	3
  filter#(mark(X1),X2,X3)	→	filter#(X1,X2,X3)	(65)
  1	>	1
  2	≥	2
  3	≥	3
  filter#(X1,X2,mark(X3))	→	filter#(X1,X2,X3)	(67)
  1	≥	1
  2	≥	2
  3	>	3
  filter#(ok(X1),ok(X2),ok(X3))	→	filter#(X1,X2,X3)	(85)
  1	>	1
  2	>	2
  3	>	3

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

• The 5^th component contains the pair

  cons#(ok(X1),ok(X2))	→	cons#(X1,X2)	(86)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(68)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [cons#(x1, x2)]	=	1 · x1 + 1 · x2

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.5.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  cons#(ok(X1),ok(X2))	→	cons#(X1,X2)	(86)
  1	>	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(68)
  1	>	1
  2	≥	2

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

• The 6^th component contains the pair

  s#(ok(X))	→	s#(X)	(87)
  s#(mark(X))	→	s#(X)	(69)

  1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [s#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.6.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  s#(ok(X))	→	s#(X)	(87)
  1	>	1
  s#(mark(X))	→	s#(X)	(69)
  1	>	1

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

• The 7^th component contains the pair

  sieve#(ok(X))	→	sieve#(X)	(88)
  sieve#(mark(X))	→	sieve#(X)	(70)

  1.1.7 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [sieve#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.7.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  sieve#(ok(X))	→	sieve#(X)	(88)
  1	>	1
  sieve#(mark(X))	→	sieve#(X)	(70)
  1	>	1

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

• The 8^th component contains the pair

  nats#(ok(X))	→	nats#(X)	(89)
  nats#(mark(X))	→	nats#(X)	(71)

  1.1.8 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [nats#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.8.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  nats#(ok(X))	→	nats#(X)	(89)
  1	>	1
  nats#(mark(X))	→	nats#(X)	(71)
  1	>	1

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