Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/214320)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

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

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

• The 1^st component contains the pair

  0#(1(1(3(x1))))	→	0#(x1)	(113)
  0#(1(0(3(x1))))	→	0#(x1)	(109)
  0#(3(1(0(x1))))	→	0#(5(0(x1)))	(137)

  1.1.1 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 + 1 · x1
  [0(x1)]	=	1 · x1
  [5(x1)]	=	0
  [2(x1)]	=	0
  [4(x1)]	=	0

  together with the usable rules

  5(0(1(0(x1))))	→	1(4(0(0(5(1(x1))))))	(41)
  5(0(1(0(x1))))	→	2(1(0(0(4(5(x1))))))	(42)
  5(0(1(2(0(x1)))))	→	0(0(5(2(1(0(x1))))))	(50)

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

  0#(1(1(3(x1))))	→	0#(x1)	(113)
  0#(1(0(3(x1))))	→	0#(x1)	(109)
  0#(3(1(0(x1))))	→	0#(5(0(x1)))	(137)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

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

  →

  3#(0(x1))

  (166)

  1.1.2 Size-Change Termination

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

  3#(0(3(1(0(x1)))))	→	3#(0(x1))	(166)
  1	>	1

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

• The 3^rd component contains the pair

  5#(0(1(0(x1))))

  →

  5#(x1)

  (144)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  5#(0(1(0(x1))))	→	5#(x1)	(144)
  1	>	1

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