Certification Problem

Input (TPDB TRS_Standard/AProVE_06/quicksort)

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

• The 1^st component contains the pair

  if_qs#(false,x,n,y)	→	quicksort#(x)	(38)
  quicksort#(x)	→	if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))	(36)
  if_qs#(false,x,n,y)	→	quicksort#(y)	(37)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [false]	=	2
  [low(x1, x2)]	=	-∞ · x1 + 0 · x2 + -2
  [le(x1, x2)]	=	0 · x1 + -∞ · x2 + 2
  [s(x1)]	=	0 · x1 + 0
  [quicksort#(x1)]	=	0 · x1 + 1
  [if_qs#(x1,...,x4)]	=	-1 · x1 + 0 · x2 + -1 · x3 + 0 · x4 + -∞
  [nil]	=	0
  [high(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [0]	=	5
  [add(x1, x2)]	=	0 · x1 + 1 · x2 + 2
  [isempty(x1)]	=	0 · x1 + -∞
  [head(x1)]	=	0 · x1 + -∞
  [if_high(x1, x2, x3)]	=	-2 · x1 + -∞ · x2 + 0 · x3 + 0
  [if_low(x1, x2, x3)]	=	0 · x1 + -∞ · x2 + 0 · x3 + 0
  [tail(x1)]	=	-1 · x1 + 0
  [true]	=	0

  together with the usable rules

  high(n,nil)	→	nil	(10)
  high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(11)
  tail(add(n,x))	→	x	(15)
  head(add(n,x))	→	n	(14)
  if_high(true,n,add(m,x))	→	high(n,x)	(12)
  if_high(false,n,add(m,x))	→	add(m,high(n,x))	(13)
  le(0,y)	→	true	(1)
  le(s(x),0)	→	false	(2)
  le(s(x),s(y))	→	le(x,y)	(3)
  low(n,nil)	→	nil	(6)
  low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(7)
  if_low(true,n,add(m,x))	→	add(m,low(n,x))	(8)
  if_low(false,n,add(m,x))	→	low(n,x)	(9)
  isempty(nil)	→	true	(16)
  isempty(add(n,x))	→	false	(17)

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

  quicksort#(x)

  →

  if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))

  (36)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  app#(add(n,x),y)

  →

  app#(x,y)

  (22)

  1.1.2 Size-Change Termination

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

  app#(add(n,x),y)	→	app#(x,y)	(22)
  2	≥	2
  1	>	1

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

• The 3^rd component contains the pair

  low#(n,add(m,x))	→	if_low#(le(m,n),n,add(m,x))	(24)
  if_low#(true,n,add(m,x))	→	low#(n,x)	(25)
  if_low#(false,n,add(m,x))	→	low#(n,x)	(26)

  1.1.3 Size-Change Termination

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

  low#(n,add(m,x))	→	if_low#(le(m,n),n,add(m,x))	(24)
  2	≥	3
  1	≥	2
  if_low#(true,n,add(m,x))	→	low#(n,x)	(25)
  3	>	2
  2	≥	1
  if_low#(false,n,add(m,x))	→	low#(n,x)	(26)
  3	>	2
  2	≥	1

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

• The 4^th component contains the pair

  high#(n,add(m,x))	→	if_high#(le(m,n),n,add(m,x))	(28)
  if_high#(true,n,add(m,x))	→	high#(n,x)	(29)
  if_high#(false,n,add(m,x))	→	high#(n,x)	(30)

  1.1.4 Size-Change Termination

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

  high#(n,add(m,x))	→	if_high#(le(m,n),n,add(m,x))	(28)
  2	≥	3
  1	≥	2
  if_high#(true,n,add(m,x))	→	high#(n,x)	(29)
  3	>	2
  2	≥	1
  if_high#(false,n,add(m,x))	→	high#(n,x)	(30)
  3	>	2
  2	≥	1

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

• The 5^th component contains the pair

  le#(s(x),s(y))

  →

  le#(x,y)

  (21)

  1.1.5 Size-Change Termination

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

  le#(s(x),s(y))	→	le#(x,y)	(21)
  2	>	2
  1	>	1

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