Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret5)

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

• The 1^st component contains the pair

  a#(nt(X))	→	a#(X)	(31)
  a#(ns(X))	→	a#(X)	(33)
  a#(nf(X1,X2))	→	f#(a(X1),a(X2))	(34)
  f#(s(X),cs(Y,Z))	→	a#(Z)	(29)
  a#(nf(X1,X2))	→	a#(X1)	(35)
  a#(nf(X1,X2))	→	a#(X2)	(36)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  prec(nf)	=	0		weight(nf)	=	2
  prec(a)	=	4		weight(a)	=	0
  prec(f)	=	1		weight(f)	=	2
  prec(0)	=	2		weight(0)	=	2
  prec(nil)	=	3		weight(nil)	=	4

  in combination with the following argument filter

  π(a#)	=	1
  π(nt)	=	1
  π(ns)	=	1
  π(nf)	=	[1,2]
  π(f#)	=	2
  π(a)	=	[1]
  π(cs)	=	2
  π(t)	=	1
  π(s)	=	1
  π(f)	=	[1,2]
  π(0)	=	[]
  π(nil)	=	[]

  together with the usable rules

  a(nt(X))	→	t(a(X))	(14)
  a(ns(X))	→	s(a(X))	(15)
  a(nf(X1,X2))	→	f(a(X1),a(X2))	(16)
  a(X)	→	X	(17)
  f(s(X),cs(Y,Z))	→	cs(Y,nf(X,a(Z)))	(10)
  s(X)	→	ns(X)	(12)
  t(N)	→	cs(r(q(N)),nt(ns(N)))	(1)
  t(X)	→	nt(X)	(11)
  f(0,X)	→	nil	(9)
  f(X1,X2)	→	nf(X1,X2)	(13)

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

  a#(nf(X1,X2))	→	f#(a(X1),a(X2))	(34)
  a#(nf(X1,X2))	→	a#(X1)	(35)
  a#(nf(X1,X2))	→	a#(X2)	(36)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    a#(ns(X))	→	a#(X)	(33)
    a#(nt(X))	→	a#(X)	(31)

    1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [ns(x1)]	=	1 · x1
    [nt(x1)]	=	1 · x1
    [a#(x1)]	=	1 · x1

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

    1.1.1.1.1.1 Size-Change Termination

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

    a#(ns(X))	→	a#(X)	(33)
    1	>	1
    a#(nt(X))	→	a#(X)	(31)
    1	>	1

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

• The 2^nd component contains the pair

  q#(s(X))

  →

  q#(X)

  (21)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [q#(x1)]	=	1 · x1

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

  1.1.2.1 Size-Change Termination

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

  q#(s(X))	→	q#(X)	(21)
  1	>	1

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

• The 3^rd component contains the pair

  d#(s(X))

  →

  d#(X)

  (25)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [d#(x1)]	=	1 · x1

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

  1.1.3.1 Size-Change Termination

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

  d#(s(X))	→	d#(X)	(25)
  1	>	1

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

• The 4^th component contains the pair

  p#(s(X),s(Y))

  →

  p#(X,Y)

  (28)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [p#(x1, x2)]	=	1 · x1 + 1 · x2

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

  1.1.4.1 Size-Change Termination

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

  p#(s(X),s(Y))	→	p#(X,Y)	(28)
  1	>	1
  2	>	2

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