Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_Luc02a_FR)

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

• The 1^st component contains the pair

  activate#(n__terms(X))	→	activate#(X)	(35)
  activate#(n__s(X))	→	activate#(X)	(37)
  activate#(n__first(X1,X2))	→	first#(activate(X1),activate(X2))	(38)
  first#(s(X),cons(Y,Z))	→	activate#(Z)	(31)
  activate#(n__first(X1,X2))	→	activate#(X1)	(39)
  activate#(n__first(X1,X2))	→	activate#(X2)	(40)

  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(n__first)	=	0		weight(n__first)	=	2
  prec(activate)	=	4		weight(activate)	=	0
  prec(first)	=	2		weight(first)	=	2
  prec(0)	=	1		weight(0)	=	2
  prec(nil)	=	3		weight(nil)	=	4

  in combination with the following argument filter

  π(activate#)	=	1
  π(n__terms)	=	1
  π(n__s)	=	1
  π(n__first)	=	[1,2]
  π(first#)	=	2
  π(activate)	=	[1]
  π(cons)	=	2
  π(terms)	=	1
  π(s)	=	1
  π(first)	=	[1,2]
  π(0)	=	[]
  π(nil)	=	[]

  together with the usable rules

  activate(n__terms(X))	→	terms(activate(X))	(17)
  activate(n__s(X))	→	s(activate(X))	(18)
  activate(n__first(X1,X2))	→	first(activate(X1),activate(X2))	(19)
  activate(X)	→	X	(20)
  first(s(X),cons(Y,Z))	→	cons(Y,n__first(X,activate(Z)))	(9)
  s(X)	→	n__s(X)	(15)
  terms(N)	→	cons(recip(sqr(N)),n__terms(n__s(N)))	(1)
  terms(X)	→	n__terms(X)	(14)
  first(0,X)	→	nil	(8)
  first(X1,X2)	→	n__first(X1,X2)	(16)

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

  activate#(n__first(X1,X2))	→	first#(activate(X1),activate(X2))	(38)
  activate#(n__first(X1,X2))	→	activate#(X1)	(39)
  activate#(n__first(X1,X2))	→	activate#(X2)	(40)

  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

    activate#(n__s(X))	→	activate#(X)	(37)
    activate#(n__terms(X))	→	activate#(X)	(35)

    1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [n__s(x1)]	=	1 · x1
    [n__terms(x1)]	=	1 · x1
    [activate#(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.

    activate#(n__s(X))	→	activate#(X)	(37)
    1	>	1
    activate#(n__terms(X))	→	activate#(X)	(35)
    1	>	1

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

• The 2^nd component contains the pair

  sqr#(s(X))

  →

  sqr#(X)

  (24)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [sqr#(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.

  sqr#(s(X))	→	sqr#(X)	(24)
  1	>	1

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

• The 3^rd component contains the pair

  dbl#(s(X))

  →

  dbl#(X)

  (28)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [dbl#(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.

  dbl#(s(X))	→	dbl#(X)	(28)
  1	>	1

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

• The 4^th component contains the pair

  add#(s(X),Y)

  →

  add#(X,Y)

  (30)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [add#(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.

  add#(s(X),Y)	→	add#(X,Y)	(30)
  1	>	1
  2	≥	2

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

• The 5^th component contains the pair

  half#(s(s(X)))

  →

  half#(X)

  (33)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [half#(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.5.1 Size-Change Termination

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

  half#(s(s(X)))	→	half#(X)	(33)
  1	>	1

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