Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/41843)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

There are 283 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#(0(1(2(x1))))	→	1#(0(2(x1)))	(81)
  1#(0(1(2(x1))))	→	0#(2(x1))	(111)
  0#(2(5(3(5(1(x1))))))	→	1#(5(5(x1)))	(269)
  1#(0(5(5(1(x1)))))	→	5#(1(5(1(x1))))	(196)
  5#(0(0(2(x1))))	→	5#(0(3(0(2(x1)))))	(140)
  5#(5(0(1(2(x1)))))	→	0#(2(1(x1)))	(221)
  0#(2(5(3(5(1(x1))))))	→	5#(5(x1))	(270)
  5#(5(0(1(2(x1)))))	→	1#(x1)	(222)
  1#(2(0(5(x1))))	→	1#(5(x1))	(122)
  1#(0(5(5(1(x1)))))	→	1#(5(1(x1)))	(197)
  1#(5(0(5(0(x1)))))	→	5#(1(0(x1)))	(208)
  1#(5(0(5(0(x1)))))	→	1#(0(x1))	(209)
  1#(4(1(0(0(5(x1))))))	→	1#(x1)	(311)
  1#(2(0(5(x1))))	→	1#(x1)	(125)
  1#(2(1(2(0(0(x1))))))	→	1#(0(1(x1)))	(304)
  1#(2(1(2(0(0(x1))))))	→	0#(1(x1))	(305)
  0#(0(1(2(x1))))	→	0#(2(x1))	(82)
  0#(2(5(3(5(1(x1))))))	→	5#(x1)	(271)
  0#(1(2(4(x1))))	→	1#(4(x1))	(86)
  0#(5(0(5(x1))))	→	0#(5(5(x1)))	(88)
  0#(5(0(5(x1))))	→	5#(5(x1))	(89)
  0#(5(1(2(x1))))	→	1#(5(x1))	(96)
  0#(5(1(2(x1))))	→	5#(x1)	(97)
  0#(1(2(5(0(x1)))))	→	0#(0(1(5(x1))))	(154)
  0#(1(2(5(0(x1)))))	→	0#(1(5(x1)))	(155)
  0#(1(2(5(0(x1)))))	→	1#(5(x1))	(156)
  0#(1(2(5(0(x1)))))	→	5#(x1)	(157)
  0#(5(0(5(1(x1)))))	→	0#(1(0(3(5(5(x1))))))	(171)
  0#(5(0(5(1(x1)))))	→	1#(0(3(5(5(x1)))))	(172)
  0#(5(0(5(1(x1)))))	→	5#(5(x1))	(174)
  0#(5(0(5(1(x1)))))	→	5#(x1)	(175)
  0#(0(0(5(1(2(x1))))))	→	0#(0(1(5(0(2(4(x1)))))))	(223)
  0#(0(0(5(1(2(x1))))))	→	0#(1(5(0(2(4(x1))))))	(224)
  0#(0(5(5(3(4(x1))))))	→	1#(4(1(0(0(3(5(5(x1))))))))	(241)
  0#(0(5(5(3(4(x1))))))	→	1#(0(0(3(5(5(x1))))))	(242)
  0#(0(5(5(3(4(x1))))))	→	0#(0(3(5(5(x1)))))	(243)
  0#(0(5(5(3(4(x1))))))	→	5#(5(x1))	(245)
  0#(0(5(5(3(4(x1))))))	→	5#(x1)	(246)
  0#(1(2(0(1(2(x1))))))	→	1#(1(0(x1)))	(249)
  0#(1(2(0(1(2(x1))))))	→	1#(0(x1))	(250)
  0#(1(2(0(1(2(x1))))))	→	0#(x1)	(251)
  0#(0(2(5(2(x1)))))	→	0#(5(2(x1)))	(153)
  0#(5(2(4(1(x1)))))	→	5#(1(x1))	(187)
  0#(5(2(5(1(3(4(x1)))))))	→	1#(5(x1))	(336)
  0#(5(2(5(1(3(4(x1)))))))	→	5#(x1)	(337)
  0#(4(2(0(5(x1)))))	→	1#(5(x1))	(165)
  0#(0(5(2(3(4(x1))))))	→	1#(2(5(x1)))	(239)
  1#(2(1(2(0(0(x1))))))	→	1#(x1)	(306)
  0#(0(5(2(3(4(x1))))))	→	5#(x1)	(240)
  0#(5(0(0(5(4(x1))))))	→	0#(1(0(1(0(4(5(5(x1))))))))	(272)
  0#(5(0(0(5(4(x1))))))	→	1#(0(1(0(4(5(5(x1)))))))	(273)
  0#(5(0(0(5(4(x1))))))	→	0#(1(0(4(5(5(x1))))))	(274)
  0#(5(0(0(5(4(x1))))))	→	1#(0(4(5(5(x1)))))	(275)
  0#(5(0(0(5(4(x1))))))	→	5#(5(x1))	(277)
  0#(5(0(0(5(4(x1))))))	→	5#(x1)	(278)
  0#(5(1(2(1(4(x1))))))	→	0#(4(x1))	(282)
  0#(0(1(2(3(5(5(x1)))))))	→	5#(1(5(0(3(0(2(1(x1))))))))	(315)
  0#(0(1(2(3(5(5(x1)))))))	→	1#(5(0(3(0(2(1(x1)))))))	(316)
  0#(0(1(2(3(5(5(x1)))))))	→	5#(0(3(0(2(1(x1))))))	(317)
  0#(0(1(2(3(5(5(x1)))))))	→	0#(2(1(x1)))	(319)
  0#(0(1(2(3(5(5(x1)))))))	→	1#(x1)	(320)
  0#(1(0(0(5(3(4(x1)))))))	→	1#(x1)	(328)
  0#(5(5(0(2(5(1(x1)))))))	→	5#(x1)	(343)
  0#(5(5(2(5(3(4(x1)))))))	→	1#(4(5(5(5(x1)))))	(345)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(5(5(x1)))	(346)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(5(x1))	(347)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(x1)	(348)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  1#(0(5(5(1(x1)))))	→	5#(1(5(1(x1))))	(196)
  5#(5(0(1(2(x1)))))	→	0#(2(1(x1)))	(221)
  0#(2(5(3(5(1(x1))))))	→	5#(5(x1))	(270)
  5#(5(0(1(2(x1)))))	→	1#(x1)	(222)
  1#(0(5(5(1(x1)))))	→	1#(5(1(x1)))	(197)
  1#(5(0(5(0(x1)))))	→	5#(1(0(x1)))	(208)
  1#(5(0(5(0(x1)))))	→	1#(0(x1))	(209)
  1#(4(1(0(0(5(x1))))))	→	1#(x1)	(311)
  1#(2(0(5(x1))))	→	1#(x1)	(125)
  0#(2(5(3(5(1(x1))))))	→	5#(x1)	(271)
  0#(5(0(5(x1))))	→	5#(5(x1))	(89)
  0#(5(1(2(x1))))	→	5#(x1)	(97)
  0#(1(2(5(0(x1)))))	→	5#(x1)	(157)
  0#(5(0(5(1(x1)))))	→	5#(5(x1))	(174)
  0#(5(0(5(1(x1)))))	→	5#(x1)	(175)
  0#(0(5(5(3(4(x1))))))	→	5#(5(x1))	(245)
  0#(0(5(5(3(4(x1))))))	→	5#(x1)	(246)
  0#(5(2(4(1(x1)))))	→	5#(1(x1))	(187)
  0#(5(2(5(1(3(4(x1)))))))	→	1#(5(x1))	(336)
  0#(5(2(5(1(3(4(x1)))))))	→	5#(x1)	(337)
  0#(0(5(2(3(4(x1))))))	→	5#(x1)	(240)
  0#(5(0(0(5(4(x1))))))	→	5#(5(x1))	(277)
  0#(5(0(0(5(4(x1))))))	→	5#(x1)	(278)
  0#(5(1(2(1(4(x1))))))	→	0#(4(x1))	(282)
  0#(0(1(2(3(5(5(x1)))))))	→	5#(1(5(0(3(0(2(1(x1))))))))	(315)
  0#(0(1(2(3(5(5(x1)))))))	→	1#(5(0(3(0(2(1(x1)))))))	(316)
  0#(0(1(2(3(5(5(x1)))))))	→	5#(0(3(0(2(1(x1))))))	(317)
  0#(0(1(2(3(5(5(x1)))))))	→	0#(2(1(x1)))	(319)
  0#(0(1(2(3(5(5(x1)))))))	→	1#(x1)	(320)
  0#(1(0(0(5(3(4(x1)))))))	→	1#(x1)	(328)
  0#(5(5(0(2(5(1(x1)))))))	→	5#(x1)	(343)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(5(5(x1)))	(346)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(5(x1))	(347)
  0#(5(5(2(5(3(4(x1)))))))	→	5#(x1)	(348)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 3 components.

  • The 1^st component contains the pair

    0#(5(0(5(x1))))	→	0#(5(5(x1)))	(88)
    0#(1(2(5(0(x1)))))	→	0#(0(1(5(x1))))	(154)
    0#(1(2(5(0(x1)))))	→	0#(1(5(x1)))	(155)
    0#(5(0(5(1(x1)))))	→	0#(1(0(3(5(5(x1))))))	(171)
    0#(0(0(5(1(2(x1))))))	→	0#(0(1(5(0(2(4(x1)))))))	(223)
    0#(0(0(5(1(2(x1))))))	→	0#(1(5(0(2(4(x1))))))	(224)
    0#(0(5(5(3(4(x1))))))	→	0#(0(3(5(5(x1)))))	(243)
    0#(1(2(0(1(2(x1))))))	→	0#(x1)	(251)
    0#(0(5(2(3(4(x1))))))	→	1#(2(5(x1)))	(239)
    1#(2(1(2(0(0(x1))))))	→	0#(1(x1))	(305)
    0#(5(0(0(5(4(x1))))))	→	0#(1(0(1(0(4(5(5(x1))))))))	(272)
    0#(5(0(0(5(4(x1))))))	→	0#(1(0(4(5(5(x1))))))	(274)
    1#(2(1(2(0(0(x1))))))	→	1#(x1)	(306)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    5(0(0(2(x1))))	→	5(0(3(0(2(x1)))))	(20)
    5(0(1(2(x1))))	→	5(1(0(3(2(x1)))))	(21)
    5(0(1(2(x1))))	→	5(1(0(3(2(3(x1))))))	(22)
    5(0(2(0(5(x1)))))	→	5(0(3(3(2(0(5(x1)))))))	(44)
    5(0(2(3(4(x1)))))	→	5(0(3(2(3(4(x1))))))	(45)
    5(5(0(1(2(x1)))))	→	5(5(3(0(2(1(x1))))))	(46)

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

    1#(2(1(2(0(0(x1))))))	→	0#(1(x1))	(305)
    1#(2(1(2(0(0(x1))))))	→	1#(x1)	(306)

    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(2(5(0(x1)))))	→	0#(0(1(5(x1))))	(154)
      0#(5(0(5(x1))))	→	0#(5(5(x1)))	(88)
      0#(1(2(5(0(x1)))))	→	0#(1(5(x1)))	(155)
      0#(5(0(5(1(x1)))))	→	0#(1(0(3(5(5(x1))))))	(171)
      0#(0(0(5(1(2(x1))))))	→	0#(0(1(5(0(2(4(x1)))))))	(223)
      0#(0(0(5(1(2(x1))))))	→	0#(1(5(0(2(4(x1))))))	(224)
      0#(0(5(5(3(4(x1))))))	→	0#(0(3(5(5(x1)))))	(243)
      0#(1(2(0(1(2(x1))))))	→	0#(x1)	(251)
      0#(5(0(0(5(4(x1))))))	→	0#(1(0(1(0(4(5(5(x1))))))))	(272)
      0#(5(0(0(5(4(x1))))))	→	0#(1(0(4(5(5(x1))))))	(274)

      1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

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

      the pairs

      0#(1(2(5(0(x1)))))	→	0#(0(1(5(x1))))	(154)
      0#(1(2(5(0(x1)))))	→	0#(1(5(x1)))	(155)
      0#(1(2(0(1(2(x1))))))	→	0#(x1)	(251)

      could be deleted.

      1.1.1.1.1.1.1.1 Split

      We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD

      0#(0(0(5(1(2(x1))))))	→	0#(1(5(0(2(4(x1))))))	(224)
      0#(0(0(5(1(2(x1))))))	→	0#(0(1(5(0(2(4(x1)))))))	(223)
      0#(5(0(0(5(4(x1))))))	→	0#(1(0(4(5(5(x1))))))	(274)
      0#(5(0(0(5(4(x1))))))	→	0#(1(0(1(0(4(5(5(x1))))))))	(272)
      0#(0(5(5(3(4(x1))))))	→	0#(0(3(5(5(x1)))))	(243)

      and the rules RD

      There are no rules.

      are deleted.

      1.1.1.1.1.1.1.1.1 Semantic Labeling Processor

      The following interpretations form a model of the rules.

      As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

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

      We obtain the set of labeled pairs

      0#0(50(00(50(x1))))	→	0#0(50(50(x1)))	(363)
      0#0(50(00(50(10(x1)))))	→	0#0(10(00(30(50(50(x1))))))	(364)
      0#0(50(00(50(11(x1)))))	→	0#0(10(00(30(50(51(x1))))))	(365)
      0#0(50(00(51(x1))))	→	0#0(50(51(x1)))	(366)
      0#0(00(00(50(11(20(x1))))))	→	0#0(00(10(50(01(20(40(x1)))))))	(367)
      0#0(00(00(50(11(21(x1))))))	→	0#0(00(10(50(01(20(41(x1)))))))	(368)
      0#0(00(00(50(11(20(x1))))))	→	0#0(10(50(01(20(40(x1))))))	(369)
      0#0(00(00(50(11(21(x1))))))	→	0#0(10(50(01(20(41(x1))))))	(370)
      0#0(00(50(50(30(40(x1))))))	→	0#0(00(30(50(50(x1)))))	(371)
      0#0(00(50(50(30(41(x1))))))	→	0#0(00(30(50(51(x1)))))	(372)
      0#0(50(00(00(50(40(x1))))))	→	0#0(10(00(10(00(40(50(50(x1))))))))	(373)
      0#0(50(00(00(50(41(x1))))))	→	0#0(10(00(10(00(40(50(51(x1))))))))	(374)
      0#0(50(00(00(50(40(x1))))))	→	0#0(10(00(40(50(50(x1))))))	(375)
      0#0(50(00(00(50(41(x1))))))	→	0#0(10(00(40(50(51(x1))))))	(376)

      and the set of labeled rules:

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

      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(50(00(50(10(x1)))))	→	0#0(10(00(30(50(50(x1))))))	(364)
        0#0(50(00(50(x1))))	→	0#0(50(50(x1)))	(363)
        0#0(00(00(50(11(20(x1))))))	→	0#0(00(10(50(01(20(40(x1)))))))	(367)
        0#0(00(00(50(11(20(x1))))))	→	0#0(10(50(01(20(40(x1))))))	(369)
        0#0(00(50(50(30(40(x1))))))	→	0#0(00(30(50(50(x1)))))	(371)

        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

        [0#0(x1)]	=	1 · x1
        [50(x1)]	=	1 · x1
        [00(x1)]	=	1 · x1
        [10(x1)]	=	0
        [30(x1)]	=	0
        [11(x1)]	=	1 + 1 · x1
        [20(x1)]	=	1
        [01(x1)]	=	0
        [40(x1)]	=	0
        [21(x1)]	=	1
        [31(x1)]	=	0
        [51(x1)]	=	0
        [41(x1)]	=	1 + 1 · x1

        together with the usable rules

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

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

        0#0(00(00(50(11(20(x1))))))	→	0#0(00(10(50(01(20(40(x1)))))))	(367)
        0#0(00(00(50(11(20(x1))))))	→	0#0(10(50(01(20(40(x1))))))	(369)

        could be deleted.

        1.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

        [0#0(x1)]	=	1 · x1
        [50(x1)]	=	1
        [00(x1)]	=	1 · x1
        [10(x1)]	=	1
        [30(x1)]	=	0
        [40(x1)]	=	0
        [01(x1)]	=	1
        [20(x1)]	=	0
        [21(x1)]	=	0
        [11(x1)]	=	1
        [31(x1)]	=	0
        [51(x1)]	=	1
        [41(x1)]	=	1

        together with the usable rules

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

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

        0#0(00(50(50(30(40(x1))))))

        →

        0#0(00(30(50(50(x1)))))

        (371)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

        There are no pairs anymore.

      1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

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

      together with the usable rules

      5(0(0(2(x1))))	→	5(0(3(0(2(x1)))))	(20)
      5(0(1(2(x1))))	→	5(1(0(3(2(x1)))))	(21)
      5(0(1(2(x1))))	→	5(1(0(3(2(3(x1))))))	(22)
      5(0(2(0(5(x1)))))	→	5(0(3(3(2(0(5(x1)))))))	(44)
      5(0(2(3(4(x1)))))	→	5(0(3(2(3(4(x1))))))	(45)
      5(5(0(1(2(x1)))))	→	5(5(3(0(2(1(x1))))))	(46)
      0(3(5(2(2(x1)))))	→	0(4(5(3(2(2(x1))))))	(27)
      1(0(0(5(x1))))	→	1(1(0(0(1(5(4(x1)))))))	(10)
      1(0(1(2(x1))))	→	1(1(3(0(2(x1)))))	(11)
      1(0(1(2(x1))))	→	1(1(0(3(2(2(x1))))))	(12)
      1(0(1(2(x1))))	→	1(1(0(3(2(3(x1))))))	(13)
      1(0(5(4(x1))))	→	0(1(1(5(4(x1)))))	(14)
      1(2(0(5(x1))))	→	0(3(2(3(1(5(x1))))))	(15)
      1(2(0(5(x1))))	→	5(0(3(3(2(1(x1))))))	(16)
      1(5(0(2(x1))))	→	1(1(0(1(1(5(2(x1)))))))	(17)
      1(5(1(2(x1))))	→	0(1(1(5(2(x1)))))	(18)
      1(5(1(2(x1))))	→	1(0(1(5(3(2(x1))))))	(19)
      1(0(5(5(1(x1)))))	→	0(4(5(1(5(1(x1))))))	(38)
      1(1(2(2(0(x1)))))	→	1(1(3(2(2(0(x1))))))	(39)
      1(1(2(3(4(x1)))))	→	1(1(3(2(2(4(x1))))))	(40)
      1(1(3(5(2(x1)))))	→	1(1(5(3(3(2(x1))))))	(41)
      1(5(0(5(0(x1)))))	→	0(1(5(3(5(1(0(x1)))))))	(42)
      1(5(5(1(2(x1)))))	→	1(5(1(1(5(3(2(2(x1))))))))	(43)
      1(0(0(2(3(4(x1))))))	→	1(4(0(0(3(3(2(x1)))))))	(62)
      1(0(1(3(5(1(x1))))))	→	0(1(1(1(5(3(2(2(x1))))))))	(63)
      1(0(5(4(2(1(x1))))))	→	0(1(1(5(3(4(2(x1)))))))	(64)
      1(1(0(1(2(2(x1))))))	→	1(0(1(1(3(1(2(2(x1))))))))	(65)
      1(2(1(2(0(0(x1))))))	→	0(3(2(2(1(0(1(x1)))))))	(66)
      1(4(1(0(0(5(x1))))))	→	0(0(1(5(4(2(1(x1)))))))	(67)
      1(4(3(5(0(2(x1))))))	→	0(3(3(2(1(5(4(x1)))))))	(68)
      1(0(1(2(3(4(5(x1)))))))	→	3(0(2(1(5(1(3(4(x1))))))))	(76)
      1(1(0(2(0(2(2(x1)))))))	→	1(1(0(2(0(3(2(2(x1))))))))	(77)
      1(2(4(3(5(3(5(x1)))))))	→	5(1(3(2(2(4(3(5(x1))))))))	(78)
      1(4(3(5(2(5(2(x1)))))))	→	5(1(3(2(2(1(5(4(x1))))))))	(79)
      0(2(5(3(5(1(x1))))))	→	0(3(3(2(2(1(5(5(x1))))))))	(58)
      0(4(2(0(5(x1)))))	→	0(4(0(3(2(1(5(x1)))))))	(28)
      0(4(2(5(2(x1)))))	→	0(5(4(3(3(2(2(x1)))))))	(29)

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

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

      →

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

      (171)

      could be deleted.

      1.1.1.1.1.1.1.1.2.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

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

      together with the usable rules

      5(0(0(2(x1))))	→	5(0(3(0(2(x1)))))	(20)
      5(0(1(2(x1))))	→	5(1(0(3(2(x1)))))	(21)
      5(0(1(2(x1))))	→	5(1(0(3(2(3(x1))))))	(22)
      5(0(2(0(5(x1)))))	→	5(0(3(3(2(0(5(x1)))))))	(44)
      5(0(2(3(4(x1)))))	→	5(0(3(2(3(4(x1))))))	(45)
      5(5(0(1(2(x1)))))	→	5(5(3(0(2(1(x1))))))	(46)
      0(3(5(2(2(x1)))))	→	0(4(5(3(2(2(x1))))))	(27)

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

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

      →

      0#(5(5(x1)))

      (88)

      could be deleted.

      1.1.1.1.1.1.1.1.2.1.1 P is empty

      There are no pairs anymore.

  • The 2^nd component contains the pair

    0#(2(5(3(5(1(x1))))))	→	1#(5(5(x1)))	(269)
    1#(0(1(2(x1))))	→	0#(2(x1))	(111)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    5(0(0(2(x1))))	→	5(0(3(0(2(x1)))))	(20)
    5(0(1(2(x1))))	→	5(1(0(3(2(x1)))))	(21)
    5(0(1(2(x1))))	→	5(1(0(3(2(3(x1))))))	(22)
    5(0(2(0(5(x1)))))	→	5(0(3(3(2(0(5(x1)))))))	(44)
    5(0(2(3(4(x1)))))	→	5(0(3(2(3(4(x1))))))	(45)
    5(5(0(1(2(x1)))))	→	5(5(3(0(2(1(x1))))))	(46)

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

    0#(2(5(3(5(1(x1))))))	→	1#(5(5(x1)))	(269)
    1#(0(1(2(x1))))	→	0#(2(x1))	(111)

    could be deleted.

    1.1.1.1.2.1 P is empty

    There are no pairs anymore.

  • The 3^rd component contains the pair

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

    →

    5#(0(3(0(2(x1)))))

    (140)

    1.1.1.1.3 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rule

    0(3(5(2(2(x1)))))

    →

    0(4(5(3(2(2(x1))))))

    (27)

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

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

    →

    5#(0(3(0(2(x1)))))

    (140)

    could be deleted.

    1.1.1.1.3.1 P is empty

    There are no pairs anymore.