Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z065)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Rule Removal

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  $#(#(x1))

  →

  $#(*(x1))

  (19)

  1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [*(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [1(x1)]	=	1 · x1
  [#(x1)]	=	1 · x1
  [$#(x1)]	=	1 · x1

  together with the usable rules

  *(0(x1))	→	1(*(x1))	(8)
  *(1(x1))	→	#(0(x1))	(9)
  0(#(x1))	→	#(0(x1))	(10)
  1(#(x1))	→	#(1(x1))	(11)

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

  1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [*(x1)]	=	2 · x1
  [0(x1)]	=	1 + 3 · x1
  [1(x1)]	=	2 + 3 · x1
  [#(x1)]	=	1 + 2 · x1
  [$#(x1)]	=	3 · x1

  the pair

  $#(#(x1))

  →

  $#(*(x1))

  (19)

  and the rules

  *(1(x1))	→	#(0(x1))	(9)
  0(#(x1))	→	#(0(x1))	(10)

  could be deleted.

  1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  *#(0(x1))

  →

  *#(x1)

  (15)

  1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [0(x1)]	=	1 · x1
  [*#(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.2.1 Size-Change Termination

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

  *#(0(x1))	→	*#(x1)	(15)
  1	>	1

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

• The 3^rd component contains the pair

  0#(#(x1))

  →

  0#(x1)

  (17)

  1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  0#(#(x1))	→	0#(x1)	(17)
  1	>	1

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

• The 4^th component contains the pair

  1#(#(x1))

  →

  1#(x1)

  (18)

  1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  1#(#(x1))	→	1#(x1)	(18)
  1	>	1

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