Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwttt)

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 1 component.

• The 1^st component contains the pair

  f#(x,f(a,y))	→	f#(f(a,h(f(a,x))),y)	(3)
  f#(x,f(a,y))	→	f#(a,f(f(a,h(f(a,x))),y))	(2)
  f#(x,f(a,y))	→	f#(a,x)	(5)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [f#(x1, x2)]	=	1 + x1 + x2
  [f(x1, x2)]	=	1 + 2 · x2
  [h(x1)]	=	-2
  [a]	=	0

  the pair

  f#(x,f(a,y))

  →

  f#(a,x)

  (5)

  could be deleted.

  1.1.1.1 Reduction Pair Processor

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

  prec(f)

  =

  1

  weight(f)

  =

  1

  in combination with the following argument filter

  π(f#)	=	2
  π(f)	=	[2]

  the pair

  f#(x,f(a,y))

  →

  f#(f(a,h(f(a,x))),y)

  (3)

  could be deleted.

  1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(a,f(a,x1))

  →

  f#(a,f(f(a,h(f(a,a))),x1))

  (6)

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [f#(x1, x2)]	=	-2 + 2 · x1 + x2
  [f(x1, x2)]	=	-1 + x1 + 2 · x2
  [a]	=	2
  [h(x1)]	=	-2

  the pair

  f#(a,f(a,x1))

  →

  f#(a,f(f(a,h(f(a,a))),x1))

  (6)

  could be deleted.

  1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.