Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/213218)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

There are 151 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  2#(0(1(3(1(x1)))))

  →

  2#(x1)

  (151)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  2#(0(1(3(1(x1)))))	→	2#(x1)	(151)
  1	>	1

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

• The 2^nd component contains the pair

  4#(5(3(2(x1))))

  →

  4#(x1)

  (112)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [5(x1)]	=	1 · x1
  [3(x1)]	=	1 · x1
  [2(x1)]	=	1 · x1
  [4#(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.

  4#(5(3(2(x1))))	→	4#(x1)	(112)
  1	>	1

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