Certification Problem

Input (TPDB TRS_Standard/Hydras/worm_wrong)

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 4 components.

• The 1^st component contains the pair

  c#(b(x))

  →

  c#(a(x))

  (32)

  1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  c#(b(f(x0)))	→	c#(f(a(x0)))	(35)
  c#(b(.(x0,x1)))	→	c#(.(a(x0),x1))	(36)
  c#(b(b1(x0)))	→	c#(b1(a(x0)))	(37)
  c#(b(f(.(0,x0))))	→	c#(b1(.(f(.(0,x0)),.(0,f(x0)))))	(38)
  c#(b(f(0)))	→	c#(b1(.(f(0),0)))	(39)
  c#(b(b(x0)))	→	c#(b(a(x0)))	(40)

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

  prec(f)	=	2		weight(f)	=	1
  prec(.)	=	1		weight(.)	=	1
  prec(0)	=	0		weight(0)	=	1

  in combination with the following argument filter

  π(c#)	=	1
  π(b)	=	1
  π(f)	=	[]
  π(.)	=	[]
  π(b1)	=	1
  π(a)	=	1
  π(0)	=	[]

  together with the usable rules

  a(f(x))	→	f(a(x))	(2)
  a(.(x,y))	→	.(a(x),y)	(3)
  a(b1(x))	→	b1(a(x))	(4)
  a(f(.(0,x)))	→	b1(.(f(.(0,x)),.(0,f(x))))	(8)
  a(f(0))	→	b1(.(f(0),0))	(9)
  a(b(x))	→	b(a(x))	(13)
  f(b(x))	→	b(f(x))	(5)
  f(.(0,x))	→	b(.(0,f(x)))	(10)
  f(0)	→	b(0)	(11)
  .(.(x,y),z)	→	.(x,.(y,z))	(1)
  .(b(x),y)	→	b(.(x,y))	(6)
  b1(b(x))	→	b(b(x))	(7)

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

  c#(b(f(.(0,x0))))	→	c#(b1(.(f(.(0,x0)),.(0,f(x0)))))	(38)
  c#(b(f(0)))	→	c#(b1(.(f(0),0)))	(39)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

  [c#(x1)]	=	0 0 + 1 0 0 0 · x1
  [b(x1)]	=	0 0 + 1 1 0 0 · x1
  [f(x1)]	=	1 0 + 1 0 0 1 · x1
  [a(x1)]	=	0 0 + 1 0 0 1 · x1
  [.(x1, x2)]	=	0 0 + 1 0 0 1 · x1 + 0 0 0 0 · x2
  [b1(x1)]	=	0 1 + 1 0 0 0 · x1
  [0]	=	0 1

  together with the usable rules

  a(f(x))	→	f(a(x))	(2)
  a(.(x,y))	→	.(a(x),y)	(3)
  a(b1(x))	→	b1(a(x))	(4)
  a(f(.(0,x)))	→	b1(.(f(.(0,x)),.(0,f(x))))	(8)
  a(f(0))	→	b1(.(f(0),0))	(9)
  a(b(x))	→	b(a(x))	(13)
  f(b(x))	→	b(f(x))	(5)
  f(.(0,x))	→	b(.(0,f(x)))	(10)
  f(0)	→	b(0)	(11)
  .(.(x,y),z)	→	.(x,.(y,z))	(1)
  .(b(x),y)	→	b(.(x,y))	(6)
  b1(b(x))	→	b(b(x))	(7)

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

  c#(b(b1(x0)))

  →

  c#(b1(a(x0)))

  (37)

  could be deleted.

  1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

  [c#(x1)]	=	0 0 + 0 1 0 0 · x1
  [b(x1)]	=	0 1 + 0 1 0 2 · x1
  [f(x1)]	=	0 0 + 1 1 0 3 · x1
  [a(x1)]	=	1 0 + 2 0 0 2 · x1
  [.(x1, x2)]	=	0 0 + 1 0 0 1 · x1 + 0 0 0 0 · x2
  [b1(x1)]	=	1 2 + 2 0 2 1 · x1
  [0]	=	0 3

  together with the usable rules

  a(f(x))	→	f(a(x))	(2)
  a(.(x,y))	→	.(a(x),y)	(3)
  a(b1(x))	→	b1(a(x))	(4)
  a(f(.(0,x)))	→	b1(.(f(.(0,x)),.(0,f(x))))	(8)
  a(f(0))	→	b1(.(f(0),0))	(9)
  a(b(x))	→	b(a(x))	(13)
  f(b(x))	→	b(f(x))	(5)
  f(.(0,x))	→	b(.(0,f(x)))	(10)
  f(0)	→	b(0)	(11)
  .(.(x,y),z)	→	.(x,.(y,z))	(1)
  .(b(x),y)	→	b(.(x,y))	(6)
  b1(b(x))	→	b(b(x))	(7)

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

  c#(b(f(x0)))	→	c#(f(a(x0)))	(35)
  c#(b(.(x0,x1)))	→	c#(.(a(x0),x1))	(36)
  c#(b(b(x0)))	→	c#(b(a(x0)))	(40)

  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

  a#(.(x,y))	→	a#(x)	(19)
  a#(f(x))	→	a#(x)	(17)
  a#(b1(x))	→	a#(x)	(21)
  a#(b(x))	→	a#(x)	(34)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [.(x1, x2)]	=	1 · x1 + 1 · x2
  [f(x1)]	=	1 · x1
  [b1(x1)]	=	1 · x1
  [b(x1)]	=	1 · x1
  [a#(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.

  a#(.(x,y))	→	a#(x)	(19)
  1	>	1
  a#(f(x))	→	a#(x)	(17)
  1	>	1
  a#(b1(x))	→	a#(x)	(21)
  1	>	1
  a#(b(x))	→	a#(x)	(34)
  1	>	1

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

• The 3^rd component contains the pair

  f#(.(0,x))	→	f#(x)	(31)
  f#(b(x))	→	f#(x)	(22)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [.(x1, x2)]	=	1 · x1 + 1 · x2
  [0]	=	0
  [b(x1)]	=	1 · x1
  [f#(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.

  f#(.(0,x))	→	f#(x)	(31)
  1	>	1
  f#(b(x))	→	f#(x)	(22)
  1	>	1

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

• The 4^th component contains the pair

  .#(.(x,y),z)	→	.#(y,z)	(15)
  .#(.(x,y),z)	→	.#(x,.(y,z))	(14)
  .#(b(x),y)	→	.#(x,y)	(23)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [.(x1, x2)]	=	1 · x1 + 1 · x2
  [b(x1)]	=	1 · x1
  [.#(x1, x2)]	=	1 · x1 + 1 · x2

  together with the usable rules

  .(.(x,y),z)	→	.(x,.(y,z))	(1)
  .(b(x),y)	→	b(.(x,y))	(6)

  (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.

  .#(.(x,y),z)	→	.#(y,z)	(15)
  1	>	1
  2	≥	2
  .#(.(x,y),z)	→	.#(x,.(y,z))	(14)
  1	>	1
  .#(b(x),y)	→	.#(x,y)	(23)
  1	>	1
  2	≥	2

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