Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/85675)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

There are 332 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 332 ruless (increase limit for explicit display).

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

  2(5(2(4(1(5(3(3(1(0(2(5(3(x1)))))))))))))	→	2(3(1(3(3(5(1(2(0(3(2(3(0(x1)))))))))))))	(18)
  0(0(1(2(2(3(x1))))))	→	4(0(2(2(3(x1)))))	(4)
  3(0(2(4(5(2(1(2(0(2(5(1(x1))))))))))))	→	3(1(3(0(5(0(2(2(4(0(4(x1)))))))))))	(15)
  2(1(4(0(4(1(5(0(2(x1)))))))))	→	3(3(2(2(3(0(3(3(4(x1)))))))))	(8)
  0(1(0(2(x1))))	→	3(4(4(x1)))	(1)
  5(3(5(0(1(x1)))))	→	5(2(3(0(x1))))	(3)
  3(3(3(4(3(0(0(4(4(5(0(5(x1))))))))))))	→	3(1(5(5(0(3(1(0(5(2(5(x1)))))))))))	(16)
  2(0(3(0(2(3(1(0(0(3(0(3(5(3(x1))))))))))))))	→	3(4(0(2(1(4(4(4(0(5(5(5(2(x1)))))))))))))	(21)
  0(3(0(2(2(2(5(5(2(4(4(3(5(1(0(0(0(3(3(x1)))))))))))))))))))	→	3(3(1(3(4(5(5(2(0(4(2(3(1(1(5(1(2(3(x1))))))))))))))))))	(26)
  2(5(5(3(5(3(1(3(1(2(5(0(0(x1)))))))))))))	→	2(5(5(5(0(4(5(5(1(1(3(2(2(x1)))))))))))))	(19)
  0(5(3(5(1(0(5(1(2(4(4(5(0(x1)))))))))))))	→	0(3(1(0(4(5(5(2(5(5(2(4(0(x1)))))))))))))	(17)
  3(3(4(3(3(4(3(0(2(5(3(1(4(5(2(5(2(4(3(5(x1))))))))))))))))))))	→	5(2(5(0(5(0(1(1(1(3(2(4(4(0(3(2(4(1(5(x1)))))))))))))))))))	(27)
  3(5(3(3(1(2(4(0(4(3(5(4(2(1(x1))))))))))))))	→	5(2(0(1(4(4(3(3(3(5(3(4(1(2(x1))))))))))))))	(22)
  2(1(5(5(3(0(1(3(3(3(1(2(0(5(2(0(3(5(2(2(2(x1)))))))))))))))))))))	→	3(0(3(3(4(0(1(4(5(1(3(3(3(4(1(2(1(3(2(1(x1))))))))))))))))))))	(28)
  0(5(3(1(4(3(x1))))))	→	1(4(0(5(2(x1)))))	(5)
  5(3(5(4(4(2(2(2(1(x1)))))))))	→	5(0(3(0(0(4(5(2(1(x1)))))))))	(10)
  2(4(0(2(3(0(0(2(x1))))))))	→	2(4(0(3(4(4(2(x1)))))))	(7)
  3(5(3(3(3(2(3(0(2(4(2(1(3(x1)))))))))))))	→	5(1(3(1(4(0(0(1(5(0(4(5(x1))))))))))))	(20)
  2(2(1(3(4(0(1(1(4(2(2(2(0(4(4(2(4(4(x1))))))))))))))))))	→	4(3(4(4(5(5(0(1(0(1(3(2(5(5(1(1(4(4(x1))))))))))))))))))	(25)
  5(4(0(0(3(2(5(3(0(3(0(4(5(0(4(4(5(1(1(1(3(x1)))))))))))))))))))))	→	5(2(5(1(0(3(5(3(2(1(0(0(5(5(4(5(4(4(2(2(2(x1)))))))))))))))))))))	(30)
  2(5(5(0(1(1(5(1(4(2(3(3(x1))))))))))))	→	4(2(3(0(3(0(0(2(3(2(3(x1)))))))))))	(14)
  4(4(3(2(0(1(1(4(0(2(x1))))))))))	→	2(3(4(0(0(1(2(1(3(4(x1))))))))))	(12)
  3(5(5(0(2(2(0(0(3(5(1(3(3(5(3(5(x1))))))))))))))))	→	3(1(4(2(0(3(4(0(4(1(5(4(2(5(x1))))))))))))))	(23)
  5(5(3(5(0(5(3(5(2(3(1(3(3(4(0(2(x1))))))))))))))))	→	5(2(4(2(4(4(0(5(5(1(3(4(0(4(0(x1)))))))))))))))	(24)
  2(0(4(2(3(3(3(5(4(2(x1))))))))))	→	3(4(4(2(0(2(3(3(5(2(x1))))))))))	(11)
  5(0(4(0(0(1(3(5(0(x1)))))))))	→	5(0(0(0(3(5(5(3(2(x1)))))))))	(9)
  1(5(5(2(4(2(4(0(3(3(0(x1)))))))))))	→	1(3(5(4(5(5(5(3(2(4(2(x1)))))))))))	(13)
  2(0(4(3(5(3(3(1(x1))))))))	→	2(1(2(2(2(0(3(1(x1))))))))	(6)
  5(1(3(4(0(3(0(2(5(3(0(2(2(0(1(2(3(3(4(1(1(x1)))))))))))))))))))))	→	5(0(1(1(4(2(0(1(1(2(1(4(0(4(3(1(2(0(0(2(x1))))))))))))))))))))	(29)
  2(0(0(3(x1))))	→	3(4(1(x1)))	(2)

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

  5#(1(3(4(0(3(0(2(5(3(0(2(2(0(1(2(3(3(4(1(1(x1)))))))))))))))))))))	→	3#(1(2(0(0(2(x1))))))	(359)
  3#(0(2(4(5(2(1(2(0(2(5(1(x1))))))))))))	→	3#(1(3(0(5(0(2(2(4(0(4(x1)))))))))))	(296)
  0#(5(3(5(1(0(5(1(2(4(4(5(0(x1)))))))))))))	→	3#(1(0(4(5(5(2(5(5(2(4(0(x1))))))))))))	(282)
  0#(3(0(2(2(2(5(5(2(4(4(3(5(1(0(0(0(3(3(x1)))))))))))))))))))	→	3#(1(1(5(1(2(3(x1)))))))	(261)
  3#(3(3(4(3(0(0(4(4(5(0(5(x1))))))))))))	→	3#(1(5(5(0(3(1(0(5(2(5(x1)))))))))))	(243)
  3#(3(3(4(3(0(0(4(4(5(0(5(x1))))))))))))	→	3#(1(0(5(2(5(x1))))))	(237)
  3#(5(3(3(3(2(3(0(2(4(2(1(3(x1)))))))))))))	→	3#(1(4(0(0(1(5(0(4(5(x1))))))))))	(125)
  2#(5(2(4(1(5(3(3(1(0(2(5(3(x1)))))))))))))	→	3#(1(3(3(5(1(2(0(3(2(3(0(x1))))))))))))	(108)
  3#(5(5(0(2(2(0(0(3(5(1(3(3(5(3(5(x1))))))))))))))))	→	3#(1(4(2(0(3(4(0(4(1(5(4(2(5(x1))))))))))))))	(88)
  0#(3(0(2(2(2(5(5(2(4(4(3(5(1(0(0(0(3(3(x1)))))))))))))))))))	→	3#(1(3(4(5(5(2(0(4(2(3(1(1(5(1(2(3(x1)))))))))))))))))	(58)

  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

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

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [0#(x1)]	=	42737
    [1(x1)]	=	8405
    [4(x1)]	=	9508
    [5(x1)]	=	9508
    [3(x1)]	=	x1 + 0
    [2#(x1)]	=	42737
    [4#(x1)]	=	42737
    [0(x1)]	=	9508
    [3#(x1)]	=	x1 + 33229
    [5#(x1)]	=	42737
    [2(x1)]	=	9508
    [1#(x1)]	=	42737

    together with the usable rules

    2(5(2(4(1(5(3(3(1(0(2(5(3(x1)))))))))))))	→	2(3(1(3(3(5(1(2(0(3(2(3(0(x1)))))))))))))	(18)
    0(0(1(2(2(3(x1))))))	→	4(0(2(2(3(x1)))))	(4)
    3(0(2(4(5(2(1(2(0(2(5(1(x1))))))))))))	→	3(1(3(0(5(0(2(2(4(0(4(x1)))))))))))	(15)
    2(1(4(0(4(1(5(0(2(x1)))))))))	→	3(3(2(2(3(0(3(3(4(x1)))))))))	(8)
    0(1(0(2(x1))))	→	3(4(4(x1)))	(1)
    5(3(5(0(1(x1)))))	→	5(2(3(0(x1))))	(3)
    3(3(3(4(3(0(0(4(4(5(0(5(x1))))))))))))	→	3(1(5(5(0(3(1(0(5(2(5(x1)))))))))))	(16)
    2(0(3(0(2(3(1(0(0(3(0(3(5(3(x1))))))))))))))	→	3(4(0(2(1(4(4(4(0(5(5(5(2(x1)))))))))))))	(21)
    0(3(0(2(2(2(5(5(2(4(4(3(5(1(0(0(0(3(3(x1)))))))))))))))))))	→	3(3(1(3(4(5(5(2(0(4(2(3(1(1(5(1(2(3(x1))))))))))))))))))	(26)
    2(5(5(3(5(3(1(3(1(2(5(0(0(x1)))))))))))))	→	2(5(5(5(0(4(5(5(1(1(3(2(2(x1)))))))))))))	(19)
    0(5(3(5(1(0(5(1(2(4(4(5(0(x1)))))))))))))	→	0(3(1(0(4(5(5(2(5(5(2(4(0(x1)))))))))))))	(17)
    3(3(4(3(3(4(3(0(2(5(3(1(4(5(2(5(2(4(3(5(x1))))))))))))))))))))	→	5(2(5(0(5(0(1(1(1(3(2(4(4(0(3(2(4(1(5(x1)))))))))))))))))))	(27)
    3(5(3(3(1(2(4(0(4(3(5(4(2(1(x1))))))))))))))	→	5(2(0(1(4(4(3(3(3(5(3(4(1(2(x1))))))))))))))	(22)
    2(1(5(5(3(0(1(3(3(3(1(2(0(5(2(0(3(5(2(2(2(x1)))))))))))))))))))))	→	3(0(3(3(4(0(1(4(5(1(3(3(3(4(1(2(1(3(2(1(x1))))))))))))))))))))	(28)
    0(5(3(1(4(3(x1))))))	→	1(4(0(5(2(x1)))))	(5)
    5(3(5(4(4(2(2(2(1(x1)))))))))	→	5(0(3(0(0(4(5(2(1(x1)))))))))	(10)
    2(4(0(2(3(0(0(2(x1))))))))	→	2(4(0(3(4(4(2(x1)))))))	(7)
    3(5(3(3(3(2(3(0(2(4(2(1(3(x1)))))))))))))	→	5(1(3(1(4(0(0(1(5(0(4(5(x1))))))))))))	(20)
    2(2(1(3(4(0(1(1(4(2(2(2(0(4(4(2(4(4(x1))))))))))))))))))	→	4(3(4(4(5(5(0(1(0(1(3(2(5(5(1(1(4(4(x1))))))))))))))))))	(25)
    5(4(0(0(3(2(5(3(0(3(0(4(5(0(4(4(5(1(1(1(3(x1)))))))))))))))))))))	→	5(2(5(1(0(3(5(3(2(1(0(0(5(5(4(5(4(4(2(2(2(x1)))))))))))))))))))))	(30)
    2(5(5(0(1(1(5(1(4(2(3(3(x1))))))))))))	→	4(2(3(0(3(0(0(2(3(2(3(x1)))))))))))	(14)
    4(4(3(2(0(1(1(4(0(2(x1))))))))))	→	2(3(4(0(0(1(2(1(3(4(x1))))))))))	(12)
    3(5(5(0(2(2(0(0(3(5(1(3(3(5(3(5(x1))))))))))))))))	→	3(1(4(2(0(3(4(0(4(1(5(4(2(5(x1))))))))))))))	(23)
    5(5(3(5(0(5(3(5(2(3(1(3(3(4(0(2(x1))))))))))))))))	→	5(2(4(2(4(4(0(5(5(1(3(4(0(4(0(x1)))))))))))))))	(24)
    2(0(4(2(3(3(3(5(4(2(x1))))))))))	→	3(4(4(2(0(2(3(3(5(2(x1))))))))))	(11)
    5(0(4(0(0(1(3(5(0(x1)))))))))	→	5(0(0(0(3(5(5(3(2(x1)))))))))	(9)
    1(5(5(2(4(2(4(0(3(3(0(x1)))))))))))	→	1(3(5(4(5(5(5(3(2(4(2(x1)))))))))))	(13)
    2(0(4(3(5(3(3(1(x1))))))))	→	2(1(2(2(2(0(3(1(x1))))))))	(6)
    5(1(3(4(0(3(0(2(5(3(0(2(2(0(1(2(3(3(4(1(1(x1)))))))))))))))))))))	→	5(0(1(1(4(2(0(1(1(2(1(4(0(4(3(1(2(0(0(2(x1))))))))))))))))))))	(29)
    2(0(0(3(x1))))	→	3(4(1(x1)))	(2)

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

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

    →

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

    (246)

    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

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

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [0#(x1)]	=	x1 + 183
      [1(x1)]	=	x1 + 166
      [4(x1)]	=	x1 + 194
      [5(x1)]	=	x1 + 157
      [3(x1)]	=	x1 + 170
      [2#(x1)]	=	x1 + 331
      [4#(x1)]	=	x1 + 348
      [0(x1)]	=	x1 + 167
      [3#(x1)]	=	x1 + 190
      [5#(x1)]	=	x1 + 177
      [2(x1)]	=	x1 + 154
      [1#(x1)]	=	x1 + 0

      together with the usable rules

      2(5(2(4(1(5(3(3(1(0(2(5(3(x1)))))))))))))	→	2(3(1(3(3(5(1(2(0(3(2(3(0(x1)))))))))))))	(18)
      0(0(1(2(2(3(x1))))))	→	4(0(2(2(3(x1)))))	(4)
      3(0(2(4(5(2(1(2(0(2(5(1(x1))))))))))))	→	3(1(3(0(5(0(2(2(4(0(4(x1)))))))))))	(15)
      2(1(4(0(4(1(5(0(2(x1)))))))))	→	3(3(2(2(3(0(3(3(4(x1)))))))))	(8)
      0(1(0(2(x1))))	→	3(4(4(x1)))	(1)
      5(3(5(0(1(x1)))))	→	5(2(3(0(x1))))	(3)
      3(3(3(4(3(0(0(4(4(5(0(5(x1))))))))))))	→	3(1(5(5(0(3(1(0(5(2(5(x1)))))))))))	(16)
      2(0(3(0(2(3(1(0(0(3(0(3(5(3(x1))))))))))))))	→	3(4(0(2(1(4(4(4(0(5(5(5(2(x1)))))))))))))	(21)
      0(3(0(2(2(2(5(5(2(4(4(3(5(1(0(0(0(3(3(x1)))))))))))))))))))	→	3(3(1(3(4(5(5(2(0(4(2(3(1(1(5(1(2(3(x1))))))))))))))))))	(26)
      2(5(5(3(5(3(1(3(1(2(5(0(0(x1)))))))))))))	→	2(5(5(5(0(4(5(5(1(1(3(2(2(x1)))))))))))))	(19)
      0(5(3(5(1(0(5(1(2(4(4(5(0(x1)))))))))))))	→	0(3(1(0(4(5(5(2(5(5(2(4(0(x1)))))))))))))	(17)
      3(3(4(3(3(4(3(0(2(5(3(1(4(5(2(5(2(4(3(5(x1))))))))))))))))))))	→	5(2(5(0(5(0(1(1(1(3(2(4(4(0(3(2(4(1(5(x1)))))))))))))))))))	(27)
      3(5(3(3(1(2(4(0(4(3(5(4(2(1(x1))))))))))))))	→	5(2(0(1(4(4(3(3(3(5(3(4(1(2(x1))))))))))))))	(22)
      2(1(5(5(3(0(1(3(3(3(1(2(0(5(2(0(3(5(2(2(2(x1)))))))))))))))))))))	→	3(0(3(3(4(0(1(4(5(1(3(3(3(4(1(2(1(3(2(1(x1))))))))))))))))))))	(28)
      0(5(3(1(4(3(x1))))))	→	1(4(0(5(2(x1)))))	(5)
      5(3(5(4(4(2(2(2(1(x1)))))))))	→	5(0(3(0(0(4(5(2(1(x1)))))))))	(10)
      2(4(0(2(3(0(0(2(x1))))))))	→	2(4(0(3(4(4(2(x1)))))))	(7)
      3(5(3(3(3(2(3(0(2(4(2(1(3(x1)))))))))))))	→	5(1(3(1(4(0(0(1(5(0(4(5(x1))))))))))))	(20)
      2(2(1(3(4(0(1(1(4(2(2(2(0(4(4(2(4(4(x1))))))))))))))))))	→	4(3(4(4(5(5(0(1(0(1(3(2(5(5(1(1(4(4(x1))))))))))))))))))	(25)
      5(4(0(0(3(2(5(3(0(3(0(4(5(0(4(4(5(1(1(1(3(x1)))))))))))))))))))))	→	5(2(5(1(0(3(5(3(2(1(0(0(5(5(4(5(4(4(2(2(2(x1)))))))))))))))))))))	(30)
      2(5(5(0(1(1(5(1(4(2(3(3(x1))))))))))))	→	4(2(3(0(3(0(0(2(3(2(3(x1)))))))))))	(14)
      4(4(3(2(0(1(1(4(0(2(x1))))))))))	→	2(3(4(0(0(1(2(1(3(4(x1))))))))))	(12)
      3(5(5(0(2(2(0(0(3(5(1(3(3(5(3(5(x1))))))))))))))))	→	3(1(4(2(0(3(4(0(4(1(5(4(2(5(x1))))))))))))))	(23)
      5(5(3(5(0(5(3(5(2(3(1(3(3(4(0(2(x1))))))))))))))))	→	5(2(4(2(4(4(0(5(5(1(3(4(0(4(0(x1)))))))))))))))	(24)
      2(0(4(2(3(3(3(5(4(2(x1))))))))))	→	3(4(4(2(0(2(3(3(5(2(x1))))))))))	(11)
      5(0(4(0(0(1(3(5(0(x1)))))))))	→	5(0(0(0(3(5(5(3(2(x1)))))))))	(9)
      1(5(5(2(4(2(4(0(3(3(0(x1)))))))))))	→	1(3(5(4(5(5(5(3(2(4(2(x1)))))))))))	(13)
      2(0(4(3(5(3(3(1(x1))))))))	→	2(1(2(2(2(0(3(1(x1))))))))	(6)
      5(1(3(4(0(3(0(2(5(3(0(2(2(0(1(2(3(3(4(1(1(x1)))))))))))))))))))))	→	5(0(1(1(4(2(0(1(1(2(1(4(0(4(3(1(2(0(0(2(x1))))))))))))))))))))	(29)
      2(0(0(3(x1))))	→	3(4(1(x1)))	(2)

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

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

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.