Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/157388)

The rewrite relation of the following TRS is considered.

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

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

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

  0#(1(0(1(x1))))	→	0#(0(x1))	(392)
  4#(5(5(1(1(x1)))))	→	4#(x1)	(393)
  4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
  4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
  0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)
  4#(4(3(0(1(x1)))))	→	4#(x1)	(356)
  0#(1(0(1(x1))))	→	0#(x1)	(349)
  4#(3(0(1(1(x1)))))	→	0#(x1)	(344)
  0#(4(3(0(1(x1)))))	→	4#(0(x1))	(340)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  4#(3(5(0(1(x1)))))	→	4#(x1)	(280)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  4#(3(5(0(1(x1)))))	→	4#(x1)	(280)
  0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  0#(4(3(0(1(x1)))))	→	0#(x1)	(267)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
  0#(0(3(1(1(x1)))))	→	0#(x1)	(238)
  4#(5(3(0(1(x1)))))	→	4#(4(1(x1)))	(235)
  0#(4(1(0(1(x1)))))	→	4#(0(1(x1)))	(226)
  0#(4(3(0(1(x1)))))	→	0#(4(0(x1)))	(225)
  4#(5(3(0(1(x1)))))	→	4#(0(x1))	(224)
  4#(5(3(0(1(x1)))))	→	4#(5(x1))	(218)
  0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)
  0#(4(3(0(1(x1)))))	→	4#(x1)	(210)
  4#(3(0(1(1(x1)))))	→	4#(x1)	(209)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  0#(4(5(1(1(x1)))))	→	4#(0(1(x1)))	(189)
  4#(3(0(1(x1))))	→	4#(3(x1))	(177)
  4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
  4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
  4#(5(3(0(1(x1)))))	→	0#(x1)	(169)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

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

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

  4#(4(3(0(1(x1)))))	→	4#(x1)	(356)
  0#(1(0(1(x1))))	→	0#(x1)	(349)
  0#(4(3(0(1(x1)))))	→	4#(0(x1))	(340)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  4#(3(5(0(1(x1)))))	→	4#(x1)	(280)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  4#(3(5(0(1(x1)))))	→	4#(x1)	(280)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  0#(4(3(0(1(x1)))))	→	0#(x1)	(267)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  0#(0(3(1(1(x1)))))	→	0#(x1)	(238)
  4#(5(3(0(1(x1)))))	→	4#(4(1(x1)))	(235)
  0#(4(1(0(1(x1)))))	→	4#(0(1(x1)))	(226)
  4#(5(3(0(1(x1)))))	→	4#(5(x1))	(218)
  0#(4(3(0(1(x1)))))	→	4#(x1)	(210)
  4#(3(0(1(1(x1)))))	→	4#(x1)	(209)
  4#(3(0(1(x1))))	→	4#(x1)	(203)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  4#(5(3(0(1(x1)))))	→	4#(x1)	(192)
  4#(3(0(1(x1))))	→	4#(3(x1))	(177)

  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#(4(3(0(1(x1)))))	→	0#(4(0(x1)))	(225)
    4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
    0#(1(0(1(x1))))	→	0#(0(x1))	(392)
    4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
    4#(5(5(1(1(x1)))))	→	4#(x1)	(393)
    4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
    0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)
    4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
    0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
    0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
    0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)
    0#(4(5(1(1(x1)))))	→	4#(0(1(x1)))	(189)
    4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
    4#(5(3(0(1(x1)))))	→	4#(0(x1))	(224)
    4#(3(0(1(1(x1)))))	→	0#(x1)	(344)

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

    together with the usable rules

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

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

    4#(5(5(1(1(x1)))))

    →

    4#(x1)

    (393)

    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#(4(3(0(1(x1)))))	→	0#(4(0(x1)))	(225)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      0#(1(0(1(x1))))	→	0#(0(x1))	(392)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
      0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
      0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)
      0#(4(5(1(1(x1)))))	→	4#(0(1(x1)))	(189)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	4#(0(x1))	(224)
      4#(3(0(1(1(x1)))))	→	0#(x1)	(344)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

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

      together with the usable rules

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

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

      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      0#(4(5(1(1(x1)))))	→	4#(0(1(x1)))	(189)
      4#(5(3(0(1(x1)))))	→	0#(x1)	(169)
      4#(5(3(0(1(x1)))))	→	4#(0(x1))	(224)
      4#(3(0(1(1(x1)))))	→	0#(x1)	(344)

      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#(4(3(0(1(x1)))))	→	0#(4(0(x1)))	(225)
        0#(1(0(1(x1))))	→	0#(0(x1))	(392)
        0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)
        0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
        0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
        0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)

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

        together with the usable rules

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

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

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

        →

        0#(4(0(x1)))

        (225)

        could be deleted.

        1.1.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#(1(0(1(x1))))	→	0#(0(x1))	(392)
          0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)
          0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
          0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
          0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)

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

          together with the usable rules

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

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

          0#(4(1(0(1(x1)))))	→	0#(4(0(1(x1))))	(270)
          0#(4(3(1(1(x1)))))	→	0#(x1)	(257)
          0#(4(5(1(1(x1)))))	→	0#(1(x1))	(375)

          could be deleted.

          1.1.1.1.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#(1(0(1(x1))))	→	0#(0(x1))	(392)
            0#(0(3(1(1(x1)))))	→	0#(0(x1))	(212)

            1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

            Using the Max-polynomial interpretation

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

            together with the usable rules

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

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

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

            →

            0#(0(x1))

            (392)

            could be deleted.

            1.1.1.1.1.1.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#(0(3(1(1(x1)))))

              →

              0#(0(x1))

              (212)

              1.1.1.1.1.1.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)]	=	0 1 0 0 · x1 + 0 0
              [1(x1)]	=	1 0 0 0 · x1 + 1 31253
              [4(x1)]	=	0 1 0 1 · x1 + 17153 2213
              [5(x1)]	=	0 0 0 1 · x1 + 8286 21354
              [3(x1)]	=	1 0 0 0 · x1 + 0 64718
              [4#(x1)]	=	0 0
              [0(x1)]	=	0 1 1 0 · x1 + 14940 16312
              [2(x1)]	=	1 1

              together with the usable rules

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

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

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

              →

              0#(0(x1))

              (212)

              could be deleted.

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

              The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  4#(1(0(1(x1))))

  →

  4#(1(x1))

  (362)

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

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

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

  4#(1(0(1(x1))))

  →

  4#(1(x1))

  (362)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.