Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/57799)

The rewrite relation of the following TRS is considered.

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

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

There are 239 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

  0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
  0#(5(1(0(x1))))	→	0#(0(x1))	(287)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(4(4(x1)))))	→	0#(x1)	(254)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(4(4(x1)))))	→	0#(x1)	(254)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
  0#(0(0(0(x1))))	→	0#(2(0(x1)))	(316)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(1(0(x1))))	→	0#(1(x1))	(225)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(4(x1))))	→	0#(x1)	(223)
  0#(1(0(4(x1))))	→	0#(x1)	(223)
  0#(5(1(0(x1))))	→	0#(0(x1))	(287)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(5(4(4(0(x1)))))	→	0#(2(x1))	(216)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(5(1(0(x1))))	→	0#(0(x1))	(287)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(0(x1))))	→	0#(0(4(x1)))	(213)
  0#(1(0(x1)))	→	0#(2(0(x1)))	(282)
  0#(1(1(0(x1))))	→	0#(0(x1))	(202)
  0#(1(1(0(x1))))	→	0#(1(0(5(3(1(x1))))))	(212)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(4(x1))))	→	0#(0(4(x1)))	(207)
  0#(1(1(0(x1))))	→	0#(0(1(x1)))	(206)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(4(x1))))	→	0#(2(0(x1)))	(204)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(1(0(x1))))	→	0#(0(x1))	(202)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(1(0(x1))))	→	0#(0(x1))	(202)
  0#(0(0(0(x1))))	→	0#(0(0(2(0(x1)))))	(290)
  0#(0(0(0(x1))))	→	0#(0(2(0(x1))))	(199)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(5(1(0(x1))))	→	0#(0(x1))	(287)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(2(0(x1)))	(282)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(4(4(x1)))))	→	0#(0(x1))	(276)
  0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(2(0(1(0(x1)))))	→	0#(0(x1))	(269)
  0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(1(0(x1))))	→	0#(1(0(x1)))	(166)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(x1)))	→	0#(0(x1))	(167)
  0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
  0#(1(0(x1)))	→	0#(5(0(x1)))	(159)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

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

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

  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(4(4(x1)))))	→	0#(x1)	(254)
  0#(1(0(4(4(x1)))))	→	0#(x1)	(254)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(0(0(0(x1))))	→	0#(2(0(x1)))	(316)
  0#(1(1(0(x1))))	→	0#(1(x1))	(225)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(1(0(4(x1))))	→	0#(x1)	(223)
  0#(1(0(4(x1))))	→	0#(x1)	(223)
  0#(5(4(4(0(x1)))))	→	0#(2(x1))	(216)
  0#(1(0(0(x1))))	→	0#(0(4(x1)))	(213)
  0#(1(0(x1)))	→	0#(2(x1))	(268)
  0#(0(0(0(x1))))	→	0#(0(2(0(x1))))	(199)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(0(1(0(x1))))	→	0#(0(x1))	(171)
  0#(2(0(1(0(x1)))))	→	0#(0(x1))	(269)
  0#(1(0(x1)))	→	0#(2(x1))	(268)

  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

    0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(1(0(x1))))	→	0#(0(x1))	(202)
    0#(5(1(0(x1))))	→	0#(0(x1))	(287)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
    0#(1(1(0(x1))))	→	0#(0(1(x1)))	(206)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(5(1(0(x1))))	→	0#(0(x1))	(287)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(4(4(x1)))))	→	0#(0(x1))	(276)
    0#(5(1(0(x1))))	→	0#(0(x1))	(287)
    0#(5(1(0(x1))))	→	0#(0(x1))	(287)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
    0#(0(0(0(x1))))	→	0#(0(0(2(0(x1)))))	(290)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(1(0(x1))))	→	0#(0(x1))	(202)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(1(0(x1))))	→	0#(0(x1))	(202)
    0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
    0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(1(0(x1))))	→	0#(1(0(x1)))	(166)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(4(x1))))	→	0#(0(4(x1)))	(207)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
    0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
    0#(1(1(0(x1))))	→	0#(1(0(5(3(1(x1))))))	(212)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(0(x1))	(167)
    0#(1(0(x1)))	→	0#(5(0(x1)))	(159)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

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

    together with the usable rules

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

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

    0#(0(0(0(x1))))

    →

    0#(0(0(2(0(x1)))))

    (290)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(5(1(0(x1))))	→	0#(0(x1))	(287)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
      0#(1(1(0(x1))))	→	0#(0(1(x1)))	(206)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(5(1(0(x1))))	→	0#(0(x1))	(287)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(4(4(x1)))))	→	0#(0(x1))	(276)
      0#(5(1(0(x1))))	→	0#(0(x1))	(287)
      0#(5(1(0(x1))))	→	0#(0(x1))	(287)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(1(0(x1)))	(166)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(4(x1))))	→	0#(0(4(x1)))	(207)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
      0#(1(1(0(x1))))	→	0#(1(0(5(3(1(x1))))))	(212)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

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

      together with the usable rules

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

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

      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
      0#(1(1(0(x1))))	→	0#(0(1(x1)))	(206)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(4(4(x1)))))	→	0#(0(x1))	(276)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(0(x1))	(202)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(2(x1)))	(260)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(1(0(x1))))	→	0#(1(0(x1)))	(166)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(4(x1))))	→	0#(0(4(x1)))	(207)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)
      0#(1(0(0(x1))))	→	0#(0(0(x1)))	(161)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(0(x1))	(167)
      0#(1(0(x1)))	→	0#(5(0(x1)))	(159)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

        [0#(x1)]	=	1 0 0 0 · x1 + 0 0
        [1(x1)]	=	0 1 0 0 · x1 + 6727 11316
        [4(x1)]	=	1 8950
        [5(x1)]	=	1 0 0 0 · x1 + 0 2358
        [3(x1)]	=	1 0 0 0 · x1 + 0 1
        [0(x1)]	=	18043 11317
        [2(x1)]	=	0 5177

        together with the usable rules

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

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

        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)
        0#(5(1(0(x1))))	→	0#(0(x1))	(287)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 0 components.