Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/58301)

The rewrite relation of the following TRS is considered.

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

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

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

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [0#(x1)]	=	x1 + 1
  [1(x1)]	=	x1 + 1
  [4(x1)]	=	x1 + 0
  [5(x1)]	=	x1 + 1
  [3(x1)]	=	x1 + 0
  [0(x1)]	=	x1 + 1
  [5#(x1)]	=	x1 + 0
  [2(x1)]	=	0

  together with the usable rules

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

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

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

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.