Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212026)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

There are 132 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#(3(2(x1)))	→	3#(0(x1))	(54)
  3#(2(0(x1)))	→	3#(x1)	(62)
  3#(2(0(x1)))	→	4#(x1)	(68)
  4#(0(4(2(x1))))	→	3#(0(x1))	(132)
  3#(2(4(x1)))	→	3#(3(4(x1)))	(69)
  3#(2(4(x1)))	→	3#(4(x1))	(70)
  3#(2(4(x1)))	→	3#(x1)	(72)
  3#(2(5(x1)))	→	3#(5(2(x1)))	(73)
  3#(2(5(x1)))	→	5#(2(x1))	(74)
  5#(2(4(x1)))	→	3#(4(x1))	(91)
  3#(2(5(x1)))	→	4#(5(2(x1)))	(76)
  4#(0(4(2(x1))))	→	0#(x1)	(133)
  0#(3(2(x1)))	→	0#(x1)	(55)
  0#(3(1(2(x1))))	→	3#(0(2(x1)))	(98)
  3#(2(5(x1)))	→	3#(3(5(2(x1))))	(77)
  3#(2(5(x1)))	→	3#(4(5(4(2(x1)))))	(78)
  3#(2(5(x1)))	→	4#(5(4(2(x1))))	(79)
  4#(3(2(0(x1))))	→	3#(4(x1))	(135)
  3#(2(5(x1)))	→	5#(4(2(x1)))	(80)
  5#(4(2(0(2(x1)))))	→	5#(0(4(2(1(2(x1))))))	(178)
  5#(0(2(x1)))	→	5#(x1)	(86)
  5#(5(0(0(x1))))	→	0#(5(5(0(x1))))	(140)
  0#(3(2(4(x1))))	→	3#(0(4(4(x1))))	(100)
  3#(0(2(4(x1))))	→	3#(0(4(2(1(1(x1))))))	(106)
  3#(0(5(4(x1))))	→	3#(4(0(5(1(3(x1))))))	(109)
  3#(0(5(4(x1))))	→	4#(0(5(1(3(x1)))))	(110)
  4#(3(2(0(x1))))	→	4#(x1)	(136)
  3#(0(5(4(x1))))	→	0#(5(1(3(x1))))	(111)
  0#(3(2(4(x1))))	→	0#(4(4(x1)))	(101)
  0#(3(2(4(x1))))	→	4#(4(x1))	(102)
  0#(5(3(1(2(x1)))))	→	0#(x1)	(149)
  3#(0(5(4(x1))))	→	5#(1(3(x1)))	(112)
  5#(1(0(2(4(x1)))))	→	5#(4(0(3(x1))))	(171)
  5#(5(0(0(x1))))	→	5#(5(0(x1)))	(141)
  5#(5(0(0(x1))))	→	5#(0(x1))	(142)
  5#(1(0(2(4(x1)))))	→	4#(0(3(x1)))	(172)
  5#(1(0(2(4(x1)))))	→	0#(3(x1))	(173)
  5#(1(0(2(4(x1)))))	→	3#(x1)	(174)
  3#(0(5(4(x1))))	→	3#(x1)	(113)
  3#(2(5(4(x1))))	→	3#(4(3(5(2(x1)))))	(122)
  3#(2(5(4(x1))))	→	4#(3(5(2(x1))))	(123)
  3#(2(5(4(x1))))	→	3#(5(2(x1)))	(124)
  3#(2(5(4(x1))))	→	5#(2(x1))	(125)
  3#(5(3(2(x1))))	→	3#(3(0(2(5(x1)))))	(126)
  3#(5(3(2(x1))))	→	3#(0(2(5(x1))))	(127)
  3#(5(3(2(x1))))	→	5#(x1)	(129)
  3#(0(3(1(2(x1)))))	→	3#(3(x1))	(159)
  3#(0(3(1(2(x1)))))	→	3#(x1)	(160)
  3#(5(1(4(0(x1)))))	→	3#(3(4(5(0(x1)))))	(163)
  3#(5(1(4(0(x1)))))	→	3#(4(5(0(x1))))	(164)
  3#(5(1(4(0(x1)))))	→	4#(5(0(x1)))	(165)
  3#(5(1(4(0(x1)))))	→	5#(0(x1))	(166)
  3#(5(3(0(4(x1)))))	→	5#(3(4(x1)))	(169)
  3#(5(3(0(4(x1)))))	→	3#(4(x1))	(170)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  5#(2(4(x1)))	→	3#(4(x1))	(91)
  0#(5(3(1(2(x1)))))	→	0#(x1)	(149)
  5#(5(0(0(x1))))	→	5#(0(x1))	(142)
  5#(1(0(2(4(x1)))))	→	4#(0(3(x1)))	(172)
  5#(1(0(2(4(x1)))))	→	0#(3(x1))	(173)
  5#(1(0(2(4(x1)))))	→	3#(x1)	(174)
  3#(0(5(4(x1))))	→	3#(x1)	(113)
  3#(5(3(0(4(x1)))))	→	3#(4(x1))	(170)

  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

    3#(2(0(x1)))	→	3#(x1)	(62)
    3#(2(0(x1)))	→	4#(x1)	(68)
    4#(0(4(2(x1))))	→	3#(0(x1))	(132)
    3#(2(4(x1)))	→	3#(3(4(x1)))	(69)
    3#(2(4(x1)))	→	3#(4(x1))	(70)
    3#(2(4(x1)))	→	3#(x1)	(72)
    3#(2(5(x1)))	→	3#(5(2(x1)))	(73)
    3#(2(5(x1)))	→	4#(5(2(x1)))	(76)
    4#(0(4(2(x1))))	→	0#(x1)	(133)
    0#(3(2(x1)))	→	3#(0(x1))	(54)
    3#(2(5(x1)))	→	3#(3(5(2(x1))))	(77)
    3#(2(5(x1)))	→	3#(4(5(4(2(x1)))))	(78)
    3#(2(5(x1)))	→	4#(5(4(2(x1))))	(79)
    4#(3(2(0(x1))))	→	3#(4(x1))	(135)
    3#(2(5(x1)))	→	5#(4(2(x1)))	(80)
    5#(4(2(0(2(x1)))))	→	5#(0(4(2(1(2(x1))))))	(178)
    5#(0(2(x1)))	→	5#(x1)	(86)
    5#(5(0(0(x1))))	→	0#(5(5(0(x1))))	(140)
    0#(3(2(x1)))	→	0#(x1)	(55)
    0#(3(1(2(x1))))	→	3#(0(2(x1)))	(98)
    3#(0(2(4(x1))))	→	3#(0(4(2(1(1(x1))))))	(106)
    3#(0(5(4(x1))))	→	3#(4(0(5(1(3(x1))))))	(109)
    3#(0(5(4(x1))))	→	4#(0(5(1(3(x1)))))	(110)
    4#(3(2(0(x1))))	→	4#(x1)	(136)
    3#(0(5(4(x1))))	→	0#(5(1(3(x1))))	(111)
    0#(3(2(4(x1))))	→	3#(0(4(4(x1))))	(100)
    3#(0(5(4(x1))))	→	5#(1(3(x1)))	(112)
    5#(1(0(2(4(x1)))))	→	5#(4(0(3(x1))))	(171)
    5#(5(0(0(x1))))	→	5#(5(0(x1)))	(141)
    3#(2(5(4(x1))))	→	3#(4(3(5(2(x1)))))	(122)
    3#(2(5(4(x1))))	→	4#(3(5(2(x1))))	(123)
    3#(2(5(4(x1))))	→	3#(5(2(x1)))	(124)
    3#(5(3(2(x1))))	→	3#(3(0(2(5(x1)))))	(126)
    3#(5(3(2(x1))))	→	3#(0(2(5(x1))))	(127)
    3#(5(3(2(x1))))	→	5#(x1)	(129)
    3#(0(3(1(2(x1)))))	→	3#(3(x1))	(159)
    3#(0(3(1(2(x1)))))	→	3#(x1)	(160)
    3#(5(1(4(0(x1)))))	→	3#(3(4(5(0(x1)))))	(163)
    3#(5(1(4(0(x1)))))	→	3#(4(5(0(x1))))	(164)
    3#(5(1(4(0(x1)))))	→	4#(5(0(x1)))	(165)
    3#(5(1(4(0(x1)))))	→	5#(0(x1))	(166)
    3#(5(3(0(4(x1)))))	→	5#(3(4(x1)))	(169)
    0#(3(2(4(x1))))	→	0#(4(4(x1)))	(101)
    0#(3(2(4(x1))))	→	4#(4(x1))	(102)

    1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pairs

    3#(2(0(x1)))	→	3#(x1)	(62)
    3#(2(0(x1)))	→	4#(x1)	(68)
    3#(2(4(x1)))	→	3#(3(4(x1)))	(69)
    3#(2(4(x1)))	→	3#(4(x1))	(70)
    3#(2(4(x1)))	→	3#(x1)	(72)
    3#(2(5(x1)))	→	4#(5(2(x1)))	(76)
    0#(3(2(x1)))	→	3#(0(x1))	(54)
    3#(2(5(x1)))	→	4#(5(4(2(x1))))	(79)
    5#(0(2(x1)))	→	5#(x1)	(86)
    0#(3(2(x1)))	→	0#(x1)	(55)
    3#(0(5(4(x1))))	→	4#(0(5(1(3(x1)))))	(110)
    4#(3(2(0(x1))))	→	4#(x1)	(136)
    0#(3(2(4(x1))))	→	3#(0(4(4(x1))))	(100)
    5#(1(0(2(4(x1)))))	→	5#(4(0(3(x1))))	(171)
    3#(2(5(4(x1))))	→	4#(3(5(2(x1))))	(123)
    3#(5(3(2(x1))))	→	5#(x1)	(129)
    3#(0(3(1(2(x1)))))	→	3#(3(x1))	(159)
    3#(0(3(1(2(x1)))))	→	3#(x1)	(160)
    3#(5(1(4(0(x1)))))	→	4#(5(0(x1)))	(165)
    0#(3(2(4(x1))))	→	0#(4(4(x1)))	(101)
    0#(3(2(4(x1))))	→	4#(4(x1))	(102)

    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

      3#(2(5(x1)))	→	3#(3(5(2(x1))))	(77)
      3#(2(5(x1)))	→	3#(5(2(x1)))	(73)
      3#(2(5(x1)))	→	3#(4(5(4(2(x1)))))	(78)
      3#(2(5(x1)))	→	5#(4(2(x1)))	(80)
      5#(4(2(0(2(x1)))))	→	5#(0(4(2(1(2(x1))))))	(178)
      5#(5(0(0(x1))))	→	0#(5(5(0(x1))))	(140)
      0#(3(1(2(x1))))	→	3#(0(2(x1)))	(98)
      3#(0(2(4(x1))))	→	3#(0(4(2(1(1(x1))))))	(106)
      3#(0(5(4(x1))))	→	3#(4(0(5(1(3(x1))))))	(109)
      3#(0(5(4(x1))))	→	0#(5(1(3(x1))))	(111)
      3#(2(5(4(x1))))	→	3#(4(3(5(2(x1)))))	(122)
      3#(2(5(4(x1))))	→	3#(5(2(x1)))	(124)
      3#(5(3(2(x1))))	→	3#(3(0(2(5(x1)))))	(126)
      3#(5(3(2(x1))))	→	3#(0(2(5(x1))))	(127)
      3#(5(1(4(0(x1)))))	→	3#(3(4(5(0(x1)))))	(163)
      3#(5(1(4(0(x1)))))	→	3#(4(5(0(x1))))	(164)
      3#(5(1(4(0(x1)))))	→	5#(0(x1))	(166)
      5#(5(0(0(x1))))	→	5#(5(0(x1)))	(141)
      3#(5(3(0(4(x1)))))	→	5#(3(4(x1)))	(169)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

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

      together with the usable rules

      5(2(4(x1)))	→	5(2(1(1(3(4(x1))))))	(19)
      5(4(2(0(2(x1)))))	→	5(0(4(2(1(2(x1))))))	(48)
      5(0(2(x1)))	→	1(1(0(2(5(x1)))))	(17)
      5(0(4(x1)))	→	0(5(4(1(1(x1)))))	(18)
      5(3(2(x1)))	→	1(1(3(5(1(2(x1))))))	(20)
      5(5(0(x1)))	→	5(1(1(5(0(x1)))))	(21)
      5(4(1(0(x1))))	→	5(1(1(4(0(1(x1))))))	(35)
      5(5(0(0(x1))))	→	1(1(0(5(5(0(x1))))))	(36)
      5(5(2(2(x1))))	→	5(5(1(1(2(2(x1))))))	(37)
      5(1(0(2(4(x1)))))	→	2(1(5(4(0(3(x1))))))	(46)
      5(1(3(2(0(x1)))))	→	2(3(5(0(1(1(x1))))))	(47)

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

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

      →

      3#(0(2(x1)))

      (98)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 2 components.

      • The 1^st component contains the pair

        3#(2(5(x1)))	→	3#(5(2(x1)))	(73)
        3#(2(5(x1)))	→	3#(3(5(2(x1))))	(77)
        3#(2(5(x1)))	→	3#(4(5(4(2(x1)))))	(78)
        3#(0(2(4(x1))))	→	3#(0(4(2(1(1(x1))))))	(106)
        3#(0(5(4(x1))))	→	3#(4(0(5(1(3(x1))))))	(109)
        3#(2(5(4(x1))))	→	3#(4(3(5(2(x1)))))	(122)
        3#(2(5(4(x1))))	→	3#(5(2(x1)))	(124)
        3#(5(3(2(x1))))	→	3#(3(0(2(5(x1)))))	(126)
        3#(5(3(2(x1))))	→	3#(0(2(5(x1))))	(127)
        3#(5(1(4(0(x1)))))	→	3#(3(4(5(0(x1)))))	(163)
        3#(5(1(4(0(x1)))))	→	3#(4(5(0(x1))))	(164)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

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

        together with the usable rules

        5(2(4(x1)))	→	5(2(1(1(3(4(x1))))))	(19)
        3(0(4(x1)))	→	0(1(3(4(1(x1)))))	(5)
        3(2(0(x1)))	→	0(2(1(3(x1))))	(6)
        3(2(0(x1)))	→	3(0(2(1(x1))))	(7)
        3(2(0(x1)))	→	0(1(2(1(3(x1)))))	(8)
        3(2(0(x1)))	→	3(0(1(2(1(4(x1))))))	(9)
        3(2(4(x1)))	→	1(2(1(3(3(4(x1))))))	(10)
        3(2(4(x1)))	→	4(1(2(1(1(3(x1))))))	(11)
        3(2(5(x1)))	→	1(3(5(2(x1))))	(12)
        3(2(5(x1)))	→	3(1(4(5(2(x1)))))	(13)
        3(2(5(x1)))	→	1(1(3(3(5(2(x1))))))	(14)
        3(2(5(x1)))	→	1(3(4(5(4(2(x1))))))	(15)
        3(5(0(x1)))	→	3(1(0(5(1(1(x1))))))	(16)
        3(0(5(4(x1))))	→	3(4(0(5(1(3(x1))))))	(27)
        3(0(2(4(x1))))	→	3(0(4(2(1(1(x1))))))	(26)
        3(2(5(4(x1))))	→	3(4(3(5(2(x1)))))	(31)
        3(5(3(2(x1))))	→	3(3(0(2(5(x1)))))	(32)
        3(1(0(0(x1))))	→	0(1(1(3(0(1(x1))))))	(28)
        3(2(4(0(x1))))	→	3(1(0(4(2(x1)))))	(29)
        3(2(4(5(x1))))	→	3(1(4(2(1(5(x1))))))	(30)
        3(0(1(4(5(x1)))))	→	3(4(0(5(1(1(x1))))))	(41)
        3(0(3(1(2(x1)))))	→	0(2(1(1(3(3(x1))))))	(42)
        3(2(2(0(4(x1)))))	→	3(2(2(0(1(4(x1))))))	(43)
        3(5(1(4(0(x1)))))	→	1(3(3(4(5(0(x1))))))	(44)
        3(5(3(0(4(x1)))))	→	3(0(1(5(3(4(x1))))))	(45)
        4(0(4(2(x1))))	→	4(4(2(1(3(0(x1))))))	(33)
        4(3(2(0(x1))))	→	0(2(1(3(4(x1)))))	(34)
        0(4(2(x1)))	→	4(1(1(1(0(2(x1))))))	(4)
        0(2(0(x1)))	→	0(0(2(1(1(x1)))))	(2)

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

        3#(2(5(x1)))	→	3#(5(2(x1)))	(73)
        3#(2(5(x1)))	→	3#(3(5(2(x1))))	(77)
        3#(2(5(x1)))	→	3#(4(5(4(2(x1)))))	(78)
        3#(2(5(4(x1))))	→	3#(4(3(5(2(x1)))))	(122)
        3#(2(5(4(x1))))	→	3#(5(2(x1)))	(124)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

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

        together with the usable rules

        0(4(2(x1)))	→	4(1(1(1(0(2(x1))))))	(4)
        3(0(4(x1)))	→	0(1(3(4(1(x1)))))	(5)
        3(2(0(x1)))	→	0(2(1(3(x1))))	(6)
        3(2(0(x1)))	→	3(0(2(1(x1))))	(7)
        3(2(0(x1)))	→	0(1(2(1(3(x1)))))	(8)
        3(2(0(x1)))	→	3(0(1(2(1(4(x1))))))	(9)
        3(2(4(x1)))	→	1(2(1(3(3(4(x1))))))	(10)
        3(2(4(x1)))	→	4(1(2(1(1(3(x1))))))	(11)
        3(2(5(x1)))	→	1(3(5(2(x1))))	(12)
        3(2(5(x1)))	→	3(1(4(5(2(x1)))))	(13)
        3(2(5(x1)))	→	1(1(3(3(5(2(x1))))))	(14)
        3(2(5(x1)))	→	1(3(4(5(4(2(x1))))))	(15)
        3(5(0(x1)))	→	3(1(0(5(1(1(x1))))))	(16)
        3(0(5(4(x1))))	→	3(4(0(5(1(3(x1))))))	(27)
        3(0(2(4(x1))))	→	3(0(4(2(1(1(x1))))))	(26)
        3(2(5(4(x1))))	→	3(4(3(5(2(x1)))))	(31)
        3(5(3(2(x1))))	→	3(3(0(2(5(x1)))))	(32)
        3(1(0(0(x1))))	→	0(1(1(3(0(1(x1))))))	(28)
        3(2(4(0(x1))))	→	3(1(0(4(2(x1)))))	(29)
        3(2(4(5(x1))))	→	3(1(4(2(1(5(x1))))))	(30)
        3(0(1(4(5(x1)))))	→	3(4(0(5(1(1(x1))))))	(41)
        3(0(3(1(2(x1)))))	→	0(2(1(1(3(3(x1))))))	(42)
        3(2(2(0(4(x1)))))	→	3(2(2(0(1(4(x1))))))	(43)
        3(5(1(4(0(x1)))))	→	1(3(3(4(5(0(x1))))))	(44)
        3(5(3(0(4(x1)))))	→	3(0(1(5(3(4(x1))))))	(45)
        0(2(0(x1)))	→	0(0(2(1(1(x1)))))	(2)
        4(0(4(2(x1))))	→	4(4(2(1(3(0(x1))))))	(33)
        4(3(2(0(x1))))	→	0(2(1(3(4(x1)))))	(34)

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

        3#(5(3(2(x1))))	→	3#(3(0(2(5(x1)))))	(126)
        3#(5(3(2(x1))))	→	3#(0(2(5(x1))))	(127)
        3#(5(1(4(0(x1)))))	→	3#(3(4(5(0(x1)))))	(163)
        3#(5(1(4(0(x1)))))	→	3#(4(5(0(x1))))	(164)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

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

        together with the usable rules

        0(4(2(x1)))	→	4(1(1(1(0(2(x1))))))	(4)
        4(0(4(2(x1))))	→	4(4(2(1(3(0(x1))))))	(33)
        4(3(2(0(x1))))	→	0(2(1(3(4(x1)))))	(34)

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

        3#(0(2(4(x1))))	→	3#(0(4(2(1(1(x1))))))	(106)
        3#(0(5(4(x1))))	→	3#(4(0(5(1(3(x1))))))	(109)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1 P is empty

        There are no pairs anymore.

      • The 2^nd component contains the pair

        5#(5(0(0(x1))))	→	5#(5(0(x1)))	(141)
        5#(4(2(0(2(x1)))))	→	5#(0(4(2(1(2(x1))))))	(178)

        1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

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

        together with the usable rules

        0(4(2(x1)))	→	4(1(1(1(0(2(x1))))))	(4)
        5(0(2(x1)))	→	1(1(0(2(5(x1)))))	(17)
        5(0(4(x1)))	→	0(5(4(1(1(x1)))))	(18)
        5(2(4(x1)))	→	5(2(1(1(3(4(x1))))))	(19)
        5(3(2(x1)))	→	1(1(3(5(1(2(x1))))))	(20)
        5(5(0(x1)))	→	5(1(1(5(0(x1)))))	(21)
        5(4(1(0(x1))))	→	5(1(1(4(0(1(x1))))))	(35)
        5(5(0(0(x1))))	→	1(1(0(5(5(0(x1))))))	(36)
        5(5(2(2(x1))))	→	5(5(1(1(2(2(x1))))))	(37)
        5(1(0(2(4(x1)))))	→	2(1(5(4(0(3(x1))))))	(46)
        5(1(3(2(0(x1)))))	→	2(3(5(0(1(1(x1))))))	(47)
        5(4(2(0(2(x1)))))	→	5(0(4(2(1(2(x1))))))	(48)
        3(5(0(x1)))	→	3(1(0(5(1(1(x1))))))	(16)

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

        5#(4(2(0(2(x1)))))

        →

        5#(0(4(2(1(2(x1))))))

        (178)

        could be deleted.

        1.1.1.1.1.1.1.1.2.1 Reduction Pair Processor with Usable Rules

        Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

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

        together with the usable rules

        0(0(0(x1)))	→	0(0(1(0(1(x1)))))	(1)
        0(2(0(x1)))	→	0(0(2(1(1(x1)))))	(2)
        0(3(2(x1)))	→	2(1(3(0(x1))))	(3)
        0(4(2(x1)))	→	4(1(1(1(0(2(x1))))))	(4)
        0(0(2(4(x1))))	→	0(4(0(2(1(1(x1))))))	(22)
        0(3(1(2(x1))))	→	1(1(3(0(2(x1)))))	(23)
        0(3(2(4(x1))))	→	2(1(3(0(4(4(x1))))))	(24)
        0(4(3(2(x1))))	→	2(3(4(0(1(x1)))))	(25)
        0(0(1(2(4(x1)))))	→	0(0(2(1(1(4(x1))))))	(38)
        0(5(3(1(2(x1)))))	→	5(2(1(3(1(0(x1))))))	(39)
        0(5(5(1(0(x1)))))	→	5(0(0(5(1(1(x1))))))	(40)
        5(0(2(x1)))	→	1(1(0(2(5(x1)))))	(17)
        5(0(4(x1)))	→	0(5(4(1(1(x1)))))	(18)
        5(2(4(x1)))	→	5(2(1(1(3(4(x1))))))	(19)
        5(3(2(x1)))	→	1(1(3(5(1(2(x1))))))	(20)
        5(5(0(x1)))	→	5(1(1(5(0(x1)))))	(21)
        5(4(1(0(x1))))	→	5(1(1(4(0(1(x1))))))	(35)
        5(5(0(0(x1))))	→	1(1(0(5(5(0(x1))))))	(36)
        5(5(2(2(x1))))	→	5(5(1(1(2(2(x1))))))	(37)
        5(1(0(2(4(x1)))))	→	2(1(5(4(0(3(x1))))))	(46)
        5(1(3(2(0(x1)))))	→	2(3(5(0(1(1(x1))))))	(47)
        5(4(2(0(2(x1)))))	→	5(0(4(2(1(2(x1))))))	(48)
        3(5(0(x1)))	→	3(1(0(5(1(1(x1))))))	(16)

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

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

        →

        5#(5(0(x1)))

        (141)

        could be deleted.

        1.1.1.1.1.1.1.1.2.1.1 P is empty

        There are no pairs anymore.