Certification Problem

Input (TPDB TRS_Standard/Rubio_04/selsort)

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

  ifselsort#(false,cons(N,L))	→	selsort#(replace(min(cons(N,L)),N,L))	(35)
  selsort#(cons(N,L))	→	ifselsort#(eq(N,min(cons(N,L))),cons(N,L))	(32)
  ifselsort#(true,cons(N,L))	→	selsort#(L)	(33)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(ifselsort#)	=	0		stat(ifselsort#)	=	lex
  prec(selsort#)	=	0		stat(selsort#)	=	lex
  prec(ifrepl)	=	0		stat(ifrepl)	=	lex
  prec(replace)	=	0		stat(replace)	=	lex
  prec(ifmin)	=	0		stat(ifmin)	=	lex
  prec(min)	=	0		stat(min)	=	lex
  prec(cons)	=	0		stat(cons)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(le)	=	0		stat(le)	=	lex
  prec(false)	=	0		stat(false)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(true)	=	0		stat(true)	=	lex
  prec(eq)	=	0		stat(eq)	=	lex
  prec(0)	=	0		stat(0)	=	lex

  π(ifselsort#)	=	2
  π(selsort#)	=	1
  π(ifrepl)	=	4
  π(replace)	=	3
  π(ifmin)	=	[]
  π(min)	=	1
  π(cons)	=	[2]
  π(nil)	=	[]
  π(le)	=	2
  π(false)	=	[]
  π(s)	=	1
  π(true)	=	[]
  π(eq)	=	[]
  π(0)	=	[]

  together with the usable rules

  replace(N,M,nil)	→	nil	(13)
  replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
  ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
  ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)

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

  ifselsort#(false,cons(N,L))	→	selsort#(replace(min(cons(N,L)),N,L))	(35)
  ifselsort#(true,cons(N,L))	→	selsort#(L)	(33)

  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

  replace#(N,M,cons(K,L))	→	ifrepl#(eq(N,K),N,M,cons(K,L))	(28)
  ifrepl#(false,N,M,cons(K,L))	→	replace#(N,M,L)	(29)

  1.1.2 Size-Change Termination

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

  replace#(N,M,cons(K,L))	→	ifrepl#(eq(N,K),N,M,cons(K,L))	(28)
  3	≥	4
  2	≥	3
  1	≥	2
  ifrepl#(false,N,M,cons(K,L))	→	replace#(N,M,L)	(29)
  4	>	3
  3	≥	2
  2	≥	1

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

• The 3^rd component contains the pair

  eq#(s(X),s(Y))

  →

  eq#(X,Y)

  (21)

  1.1.3 Size-Change Termination

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

  eq#(s(X),s(Y))	→	eq#(X,Y)	(21)
  2	>	2
  1	>	1

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

• The 4^th component contains the pair

  min#(cons(N,cons(M,L)))	→	ifmin#(le(N,M),cons(N,cons(M,L)))	(24)
  ifmin#(true,cons(N,cons(M,L)))	→	min#(cons(N,L))	(25)
  ifmin#(false,cons(N,cons(M,L)))	→	min#(cons(M,L))	(26)

  1.1.4 Reduction Pair Processor with Usable Rules

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

  [false]	=	2
  [s(x1)]	=	0 · x1 + -∞
  [min#(x1)]	=	0 · x1 + 0
  [ifmin#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [le(x1, x2)]	=	1 · x1 + -∞ · x2 + 2
  [0]	=	3
  [cons(x1, x2)]	=	2 · x1 + 2 · x2 + 0
  [true]	=	3

  together with the usable rules

  le(0,Y)	→	true	(5)
  le(s(X),0)	→	false	(6)
  le(s(X),s(Y))	→	le(X,Y)	(7)

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

  ifmin#(false,cons(N,cons(M,L)))

  →

  min#(cons(M,L))

  (26)

  could be deleted.

  1.1.4.1 Reduction Pair Processor with Usable Rules

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

  [false]	=	1
  [s(x1)]	=	0 · x1 + -∞
  [min#(x1)]	=	2 · x1 + -16
  [ifmin#(x1, x2)]	=	-∞ · x1 + 2 · x2 + 0
  [le(x1, x2)]	=	0 · x1 + 3 · x2 + -∞
  [0]	=	0
  [cons(x1, x2)]	=	-∞ · x1 + 1 · x2 + -2
  [true]	=	3

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

  ifmin#(true,cons(N,cons(M,L)))

  →

  min#(cons(N,L))

  (25)

  could be deleted.

  1.1.4.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 5^th component contains the pair

  le#(s(X),s(Y))

  →

  le#(X,Y)

  (22)

  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)	(22)
  2	>	2
  1	>	1

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