Certification Problem

Input (TPDB TRS_Standard/Beerendonk_07/8)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  cond#(true,x,y)

  →

  cond#(and(gr(x,0),gr(y,0)),p(x),p(y))

  (16)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [cond#(x1, x2, x3)]	=	-6 · x1 + -∞ · x2 + -3 · x3 + 0
  [gr(x1, x2)]	=	-2 · x1 + 5 · x2 + 0
  [p(x1)]	=	-5 · x1 + 1
  [true]	=	7
  [s(x1)]	=	6 · x1 + 9
  [false]	=	0
  [0]	=	1

  together with the usable rules

  p(0)	→	0	(9)
  p(s(x))	→	x	(10)
  gr(0,0)	→	false	(5)
  gr(0,x)	→	false	(6)
  gr(s(x),0)	→	true	(7)
  and(true,true)	→	true	(2)
  and(x,false)	→	false	(3)
  and(false,x)	→	false	(4)

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

  cond#(true,x,y)

  →

  cond#(and(gr(x,0),gr(y,0)),p(x),p(y))

  (16)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  gr#(s(x),s(y))

  →

  gr#(x,y)

  (17)

  1.1.2 Size-Change Termination

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

  gr#(s(x),s(y))	→	gr#(x,y)	(17)
  2	>	2
  1	>	1

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