Certification Problem

Input (TPDB TRS_Standard/SK90/4.61)

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

• The 1^st component contains the pair

  bsort#(.(x,y))

  →

  bsort#(butlast(bubble(.(x,y))))

  (13)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [butlast(x1)]	=	-1 · x1 + 0
  [bubble(x1)]	=	-∞ · x1 + 1
  [nil]	=	0
  [if(x1, x2, x3)]	=	-∞ · x1 + -∞ · x2 + -5 · x3 + 0
  [bsort#(x1)]	=	0 · x1 + 0
  [<=(x1, x2)]	=	0 · x1 + 1 · x2 + 2
  [.(x1, x2)]	=	-∞ · x1 + 1 · x2 + 1

  together with the usable rules

  bubble(.(x,nil))	→	.(x,nil)	(4)
  bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)
  butlast(nil)	→	nil	(9)
  butlast(.(x,nil))	→	nil	(10)
  butlast(.(x,.(y,z)))	→	.(x,butlast(.(y,z)))	(11)

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

  bsort#(.(x,y))

  →

  bsort#(butlast(bubble(.(x,y))))

  (13)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  butlast#(.(x,.(y,z)))

  →

  butlast#(.(y,z))

  (19)

  1.1.2 Size-Change Termination

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

  butlast#(.(x,.(y,z)))	→	butlast#(.(y,z))	(19)
  1	>	1

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

• The 3^rd component contains the pair

  bubble#(.(x,.(y,z)))	→	bubble#(.(y,z))	(16)
  bubble#(.(x,.(y,z)))	→	bubble#(.(x,z))	(17)

  1.1.3 Reduction Pair Processor with Usable Rules

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

  [bubble#(x1)]	=	0 · x1 + -∞
  [.(x1, x2)]	=	-∞ · x1 + 2 · x2 + -3

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

  bubble#(.(x,.(y,z)))

  →

  bubble#(.(y,z))

  (16)

  could be deleted.

  1.1.3.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(bubble#)	=	0		stat(bubble#)	=	lex
  prec(.)	=	0		stat(.)	=	lex

  π(bubble#)	=	[1]
  π(.)	=	[2]

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

  bubble#(.(x,.(y,z)))

  →

  bubble#(.(x,z))

  (17)

  could be deleted.

  1.1.3.1.1 P is empty

  There are no pairs anymore.

• The 4^th component contains the pair

  last#(.(x,.(y,z)))

  →

  last#(.(y,z))

  (18)

  1.1.4 Size-Change Termination

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

  last#(.(x,.(y,z)))	→	last#(.(y,z))	(18)
  1	>	1

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