Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/58301)

The rewrite relation of the following TRS is considered.

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

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

There are 236 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(x1)))	→	0#(3(x1))	(147)
  0#(3(0(1(x1))))	→	0#(x1)	(229)
  0#(0(1(x1)))	→	0#(x1)	(142)
  0#(0(1(x1)))	→	0#(4(x1))	(149)
  0#(4(4(1(1(x1)))))	→	0#(4(x1))	(338)
  0#(4(5(5(1(x1)))))	→	5#(x1)	(341)
  5#(0(0(1(x1))))	→	0#(0(x1))	(286)
  0#(0(1(x1)))	→	5#(0(x1))	(153)
  5#(0(0(1(x1))))	→	0#(x1)	(287)
  0#(0(1(x1)))	→	0#(3(0(x1)))	(155)
  0#(3(0(5(1(x1)))))	→	5#(0(0(3(1(x1)))))	(329)
  5#(0(1(0(1(x1)))))	→	0#(0(x1))	(372)
  0#(0(1(x1)))	→	0#(4(0(x1)))	(156)
  0#(0(0(1(x1))))	→	0#(0(1(2(0(2(x1))))))	(170)
  0#(0(0(1(x1))))	→	0#(x1)	(175)
  0#(0(0(1(x1))))	→	0#(0(x1))	(177)
  0#(0(1(1(x1))))	→	0#(x1)	(182)
  0#(0(1(1(x1))))	→	0#(1(x1))	(185)
  0#(1(0(1(x1))))	→	0#(0(1(2(1(x1)))))	(218)
  0#(1(0(1(x1))))	→	0#(0(x1))	(220)
  0#(0(3(1(x1))))	→	0#(x1)	(187)
  0#(0(3(1(x1))))	→	0#(3(x1))	(192)
  0#(3(0(5(1(x1)))))	→	0#(0(3(1(x1))))	(330)
  0#(0(5(1(x1))))	→	0#(x1)	(196)
  0#(0(5(1(x1))))	→	5#(0(0(1(x1))))	(200)
  5#(0(1(0(1(x1)))))	→	0#(x1)	(373)
  0#(0(5(1(x1))))	→	0#(0(1(x1)))	(201)
  0#(0(5(1(x1))))	→	0#(1(x1))	(202)
  0#(1(0(1(x1))))	→	0#(x1)	(221)
  0#(0(5(1(x1))))	→	0#(0(x1))	(204)
  0#(0(5(1(x1))))	→	5#(0(x1))	(208)
  0#(0(5(1(x1))))	→	5#(x1)	(212)
  0#(0(5(1(x1))))	→	0#(5(x1))	(214)
  0#(0(5(1(x1))))	→	0#(4(5(0(x1))))	(215)
  0#(1(0(1(x1))))	→	0#(0(1(x1)))	(222)
  0#(1(0(1(x1))))	→	0#(0(1(1(2(2(x1))))))	(223)
  0#(5(0(1(x1))))	→	5#(0(0(1(x1))))	(230)
  0#(5(0(1(x1))))	→	0#(0(1(x1)))	(231)
  0#(5(0(1(x1))))	→	5#(x1)	(234)
  0#(5(0(1(x1))))	→	5#(0(x1))	(241)
  0#(5(0(1(x1))))	→	0#(x1)	(242)
  0#(5(0(1(x1))))	→	0#(0(1(2(5(x1)))))	(243)
  0#(5(0(1(x1))))	→	5#(0(0(1(2(x1)))))	(248)
  0#(5(0(1(x1))))	→	0#(0(1(2(x1))))	(249)
  0#(5(1(1(x1))))	→	0#(x1)	(254)
  0#(5(1(1(x1))))	→	5#(0(1(1(x1))))	(255)
  0#(5(1(1(x1))))	→	0#(1(1(x1)))	(256)
  0#(1(1(0(1(x1)))))	→	0#(0(1(1(1(3(x1))))))	(323)
  0#(5(1(1(x1))))	→	0#(4(5(x1)))	(257)
  0#(5(1(1(x1))))	→	5#(x1)	(258)
  0#(5(1(1(x1))))	→	5#(0(x1))	(259)
  0#(5(1(1(x1))))	→	0#(1(x1))	(265)
  0#(1(0(1(1(x1)))))	→	0#(0(1(1(1(3(x1))))))	(319)
  0#(1(0(3(1(x1)))))	→	0#(x1)	(322)
  0#(5(5(1(x1))))	→	0#(x1)	(270)
  0#(5(5(1(x1))))	→	5#(x1)	(273)
  0#(5(5(1(x1))))	→	5#(5(x1))	(275)
  0#(5(5(1(x1))))	→	5#(0(5(1(x1))))	(278)
  0#(5(5(1(x1))))	→	0#(5(1(x1)))	(279)
  0#(5(1(0(1(x1)))))	→	0#(1(5(0(x1))))	(348)
  0#(1(4(1(1(x1)))))	→	0#(1(x1))	(325)
  0#(1(5(0(1(x1)))))	→	0#(0(x1))	(327)
  0#(5(5(1(x1))))	→	5#(0(1(x1)))	(283)
  0#(5(5(1(x1))))	→	0#(1(x1))	(284)
  0#(1(5(0(1(x1)))))	→	0#(x1)	(328)
  0#(0(0(3(1(x1)))))	→	0#(3(0(0(1(x1)))))	(293)
  0#(3(0(5(1(x1)))))	→	0#(3(1(x1)))	(331)
  0#(3(1(0(1(x1)))))	→	0#(0(1(x1)))	(332)
  0#(0(0(3(1(x1)))))	→	0#(0(1(x1)))	(294)
  0#(0(0(3(1(x1)))))	→	0#(1(x1))	(295)
  0#(0(0(5(1(x1)))))	→	0#(0(0(x1)))	(297)
  0#(0(0(5(1(x1)))))	→	0#(0(x1))	(298)
  0#(0(0(5(1(x1)))))	→	0#(x1)	(299)
  0#(0(1(4(0(x1)))))	→	0#(4(0(x1)))	(301)
  0#(0(1(5(0(x1)))))	→	0#(0(x1))	(304)
  0#(0(5(1(1(x1)))))	→	0#(5(0(1(x1))))	(310)
  0#(0(5(1(1(x1)))))	→	5#(0(1(x1)))	(311)
  0#(0(5(1(1(x1)))))	→	0#(1(x1))	(312)
  0#(0(5(3(1(x1)))))	→	0#(0(x1))	(317)
  0#(0(5(3(1(x1)))))	→	0#(x1)	(318)
  0#(3(5(1(1(x1)))))	→	0#(3(x1))	(337)
  0#(5(0(0(1(x1)))))	→	5#(0(0(0(1(x1)))))	(342)
  0#(5(0(0(1(x1)))))	→	0#(0(0(1(x1))))	(343)
  0#(5(0(1(0(x1)))))	→	0#(5(x1))	(346)
  0#(5(0(1(0(x1)))))	→	5#(x1)	(347)
  0#(5(1(0(1(x1)))))	→	5#(0(x1))	(349)
  0#(5(1(0(1(x1)))))	→	0#(x1)	(350)
  0#(5(3(0(1(x1)))))	→	0#(3(0(5(1(x1)))))	(363)
  0#(5(3(0(1(x1)))))	→	0#(5(1(x1)))	(364)
  0#(5(3(1(1(x1)))))	→	5#(x1)	(366)
  0#(5(3(1(1(x1)))))	→	0#(x1)	(368)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  0#(0(1(x1)))	→	0#(3(x1))	(147)
  0#(3(0(1(x1))))	→	0#(x1)	(229)
  0#(0(1(x1)))	→	0#(x1)	(142)
  0#(0(1(x1)))	→	0#(4(x1))	(149)
  0#(4(4(1(1(x1)))))	→	0#(4(x1))	(338)
  0#(4(5(5(1(x1)))))	→	5#(x1)	(341)
  5#(0(0(1(x1))))	→	0#(0(x1))	(286)
  0#(0(1(x1)))	→	5#(0(x1))	(153)
  5#(0(0(1(x1))))	→	0#(x1)	(287)
  0#(0(1(x1)))	→	0#(3(0(x1)))	(155)
  5#(0(1(0(1(x1)))))	→	0#(0(x1))	(372)
  0#(0(1(x1)))	→	0#(4(0(x1)))	(156)
  0#(0(0(1(x1))))	→	0#(0(1(2(0(2(x1))))))	(170)
  0#(0(0(1(x1))))	→	0#(x1)	(175)
  0#(0(0(1(x1))))	→	0#(0(x1))	(177)
  0#(0(1(1(x1))))	→	0#(x1)	(182)
  0#(0(1(1(x1))))	→	0#(1(x1))	(185)
  0#(1(0(1(x1))))	→	0#(0(1(2(1(x1)))))	(218)
  0#(1(0(1(x1))))	→	0#(0(x1))	(220)
  0#(0(3(1(x1))))	→	0#(x1)	(187)
  0#(0(3(1(x1))))	→	0#(3(x1))	(192)
  0#(3(0(5(1(x1)))))	→	0#(0(3(1(x1))))	(330)
  0#(0(5(1(x1))))	→	0#(x1)	(196)
  5#(0(1(0(1(x1)))))	→	0#(x1)	(373)
  0#(0(5(1(x1))))	→	0#(0(1(x1)))	(201)
  0#(0(5(1(x1))))	→	0#(1(x1))	(202)
  0#(1(0(1(x1))))	→	0#(x1)	(221)
  0#(0(5(1(x1))))	→	0#(0(x1))	(204)
  0#(0(5(1(x1))))	→	5#(0(x1))	(208)
  0#(0(5(1(x1))))	→	5#(x1)	(212)
  0#(0(5(1(x1))))	→	0#(5(x1))	(214)
  0#(0(5(1(x1))))	→	0#(4(5(0(x1))))	(215)
  0#(1(0(1(x1))))	→	0#(0(1(x1)))	(222)
  0#(5(0(1(x1))))	→	0#(0(1(x1)))	(231)
  0#(5(0(1(x1))))	→	5#(x1)	(234)
  0#(5(0(1(x1))))	→	5#(0(x1))	(241)
  0#(5(0(1(x1))))	→	0#(x1)	(242)
  0#(5(0(1(x1))))	→	0#(0(1(2(5(x1)))))	(243)
  0#(5(0(1(x1))))	→	0#(0(1(2(x1))))	(249)
  0#(5(1(1(x1))))	→	0#(x1)	(254)
  0#(5(1(1(x1))))	→	0#(1(1(x1)))	(256)
  0#(5(1(1(x1))))	→	0#(4(5(x1)))	(257)
  0#(5(1(1(x1))))	→	5#(x1)	(258)
  0#(5(1(1(x1))))	→	5#(0(x1))	(259)
  0#(5(1(1(x1))))	→	0#(1(x1))	(265)
  0#(1(0(3(1(x1)))))	→	0#(x1)	(322)
  0#(5(5(1(x1))))	→	0#(x1)	(270)
  0#(5(5(1(x1))))	→	5#(x1)	(273)
  0#(5(5(1(x1))))	→	5#(5(x1))	(275)
  0#(5(5(1(x1))))	→	0#(5(1(x1)))	(279)
  0#(5(1(0(1(x1)))))	→	0#(1(5(0(x1))))	(348)
  0#(1(4(1(1(x1)))))	→	0#(1(x1))	(325)
  0#(1(5(0(1(x1)))))	→	0#(0(x1))	(327)
  0#(5(5(1(x1))))	→	5#(0(1(x1)))	(283)
  0#(5(5(1(x1))))	→	0#(1(x1))	(284)
  0#(1(5(0(1(x1)))))	→	0#(x1)	(328)
  0#(3(0(5(1(x1)))))	→	0#(3(1(x1)))	(331)
  0#(3(1(0(1(x1)))))	→	0#(0(1(x1)))	(332)
  0#(0(0(3(1(x1)))))	→	0#(0(1(x1)))	(294)
  0#(0(0(3(1(x1)))))	→	0#(1(x1))	(295)
  0#(0(0(5(1(x1)))))	→	0#(0(0(x1)))	(297)
  0#(0(0(5(1(x1)))))	→	0#(0(x1))	(298)
  0#(0(0(5(1(x1)))))	→	0#(x1)	(299)
  0#(0(1(4(0(x1)))))	→	0#(4(0(x1)))	(301)
  0#(0(1(5(0(x1)))))	→	0#(0(x1))	(304)
  0#(0(5(1(1(x1)))))	→	0#(5(0(1(x1))))	(310)
  0#(0(5(1(1(x1)))))	→	5#(0(1(x1)))	(311)
  0#(0(5(1(1(x1)))))	→	0#(1(x1))	(312)
  0#(0(5(3(1(x1)))))	→	0#(0(x1))	(317)
  0#(0(5(3(1(x1)))))	→	0#(x1)	(318)
  0#(3(5(1(1(x1)))))	→	0#(3(x1))	(337)
  0#(5(0(0(1(x1)))))	→	0#(0(0(1(x1))))	(343)
  0#(5(0(1(0(x1)))))	→	0#(5(x1))	(346)
  0#(5(0(1(0(x1)))))	→	5#(x1)	(347)
  0#(5(1(0(1(x1)))))	→	5#(0(x1))	(349)
  0#(5(1(0(1(x1)))))	→	0#(x1)	(350)
  0#(5(3(0(1(x1)))))	→	0#(5(1(x1)))	(364)
  0#(5(3(1(1(x1)))))	→	5#(x1)	(366)
  0#(5(3(1(1(x1)))))	→	0#(x1)	(368)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.