Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3336)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

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

  2#(5(x1))	→	1#(x1)	(42)
  1#(2(5(x1)))	→	5#(4(x1))	(62)
  5#(5(3(x1)))	→	1#(2(2(x1)))	(166)
  1#(2(5(x1)))	→	4#(x1)	(63)
  4#(5(x1))	→	2#(2(1(3(2(1(x1))))))	(51)
  2#(5(1(x1)))	→	2#(2(2(1(2(3(x1))))))	(78)
  2#(5(1(x1)))	→	2#(2(1(2(3(x1)))))	(79)
  2#(5(1(x1)))	→	2#(1(2(3(x1))))	(80)
  2#(5(1(x1)))	→	1#(2(3(x1)))	(81)
  1#(2(5(x1)))	→	1#(x1)	(68)
  1#(4(5(x1)))	→	2#(1(x1))	(76)
  2#(5(1(x1)))	→	2#(3(x1))	(82)
  2#(5(1(x1)))	→	3#(x1)	(83)
  3#(5(x1))	→	1#(x1)	(46)
  1#(4(5(x1)))	→	1#(x1)	(77)
  3#(4(2(x1)))	→	2#(2(2(x1)))	(102)
  2#(5(2(x1)))	→	2#(2(3(3(x1))))	(85)
  2#(5(2(x1)))	→	2#(3(3(x1)))	(86)
  2#(5(2(x1)))	→	3#(3(x1))	(87)
  3#(4(2(x1)))	→	2#(2(x1))	(103)
  2#(5(2(x1)))	→	3#(x1)	(88)
  3#(5(1(x1)))	→	5#(x1)	(106)
  5#(5(3(x1)))	→	2#(2(x1))	(167)
  2#(5(3(x1)))	→	4#(1(3(3(x1))))	(90)
  4#(5(x1))	→	2#(1(3(2(1(x1)))))	(52)
  2#(5(3(x1)))	→	1#(3(3(x1)))	(91)
  2#(5(3(x1)))	→	3#(3(x1))	(92)
  3#(5(1(x1)))	→	4#(2(2(3(4(x1)))))	(107)
  4#(5(x1))	→	1#(3(2(1(x1))))	(53)
  4#(5(x1))	→	3#(2(1(x1)))	(54)
  3#(5(1(x1)))	→	2#(2(3(4(x1))))	(108)
  2#(5(4(x1)))	→	1#(x1)	(96)
  3#(5(1(x1)))	→	2#(3(4(x1)))	(109)
  3#(5(1(x1)))	→	3#(4(x1))	(110)
  3#(5(1(x1)))	→	4#(x1)	(111)
  4#(5(x1))	→	2#(1(x1))	(55)
  4#(5(x1))	→	1#(x1)	(56)
  4#(5(1(x1)))	→	5#(3(3(x1)))	(149)
  5#(5(3(x1)))	→	2#(x1)	(168)
  5#(5(4(x1)))	→	4#(2(2(x1)))	(171)
  4#(5(1(x1)))	→	3#(3(x1))	(150)
  3#(5(2(x1)))	→	4#(3(2(2(2(x1)))))	(116)
  4#(5(1(x1)))	→	3#(x1)	(151)
  3#(5(2(x1)))	→	3#(2(2(2(x1))))	(117)
  3#(5(2(x1)))	→	2#(2(2(x1)))	(118)
  3#(5(2(x1)))	→	2#(2(x1))	(119)
  3#(5(2(x1)))	→	2#(3(3(2(1(2(x1))))))	(124)
  3#(5(2(x1)))	→	3#(3(2(1(2(x1)))))	(125)
  3#(5(2(x1)))	→	3#(2(1(2(x1))))	(126)
  3#(5(2(x1)))	→	2#(1(2(x1)))	(127)
  3#(5(2(x1)))	→	1#(2(x1))	(128)
  3#(5(3(x1)))	→	4#(2(x1))	(137)
  4#(5(2(x1)))	→	4#(x1)	(154)
  4#(5(4(x1)))	→	4#(2(x1))	(158)
  4#(5(4(x1)))	→	2#(x1)	(159)
  3#(5(3(x1)))	→	2#(x1)	(138)
  3#(5(4(x1)))	→	1#(2(x1))	(142)
  3#(5(4(x1)))	→	2#(x1)	(143)
  5#(5(4(x1)))	→	2#(2(x1))	(172)
  5#(5(4(x1)))	→	2#(x1)	(173)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

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

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

  2#(5(x1))	→	1#(x1)	(42)
  1#(2(5(x1)))	→	5#(4(x1))	(62)
  5#(5(3(x1)))	→	1#(2(2(x1)))	(166)
  1#(2(5(x1)))	→	4#(x1)	(63)
  4#(5(x1))	→	2#(2(1(3(2(1(x1))))))	(51)
  2#(5(1(x1)))	→	2#(2(2(1(2(3(x1))))))	(78)
  2#(5(1(x1)))	→	2#(2(1(2(3(x1)))))	(79)
  2#(5(1(x1)))	→	2#(1(2(3(x1))))	(80)
  2#(5(1(x1)))	→	1#(2(3(x1)))	(81)
  1#(2(5(x1)))	→	1#(x1)	(68)
  1#(4(5(x1)))	→	2#(1(x1))	(76)
  2#(5(1(x1)))	→	2#(3(x1))	(82)
  2#(5(1(x1)))	→	3#(x1)	(83)
  3#(5(x1))	→	1#(x1)	(46)
  1#(4(5(x1)))	→	1#(x1)	(77)
  2#(5(2(x1)))	→	2#(2(3(3(x1))))	(85)
  2#(5(2(x1)))	→	2#(3(3(x1)))	(86)
  2#(5(2(x1)))	→	3#(3(x1))	(87)
  2#(5(2(x1)))	→	3#(x1)	(88)
  3#(5(1(x1)))	→	5#(x1)	(106)
  5#(5(3(x1)))	→	2#(2(x1))	(167)
  2#(5(3(x1)))	→	4#(1(3(3(x1))))	(90)
  4#(5(x1))	→	2#(1(3(2(1(x1)))))	(52)
  2#(5(3(x1)))	→	1#(3(3(x1)))	(91)
  2#(5(3(x1)))	→	3#(3(x1))	(92)
  3#(5(1(x1)))	→	4#(2(2(3(4(x1)))))	(107)
  4#(5(x1))	→	1#(3(2(1(x1))))	(53)
  4#(5(x1))	→	3#(2(1(x1)))	(54)
  3#(5(1(x1)))	→	2#(2(3(4(x1))))	(108)
  2#(5(4(x1)))	→	1#(x1)	(96)
  3#(5(1(x1)))	→	2#(3(4(x1)))	(109)
  3#(5(1(x1)))	→	3#(4(x1))	(110)
  3#(5(1(x1)))	→	4#(x1)	(111)
  4#(5(x1))	→	2#(1(x1))	(55)
  4#(5(x1))	→	1#(x1)	(56)
  4#(5(1(x1)))	→	5#(3(3(x1)))	(149)
  5#(5(3(x1)))	→	2#(x1)	(168)
  5#(5(4(x1)))	→	4#(2(2(x1)))	(171)
  4#(5(1(x1)))	→	3#(3(x1))	(150)
  3#(5(2(x1)))	→	4#(3(2(2(2(x1)))))	(116)
  4#(5(1(x1)))	→	3#(x1)	(151)
  3#(5(2(x1)))	→	3#(2(2(2(x1))))	(117)
  3#(5(2(x1)))	→	2#(2(2(x1)))	(118)
  3#(5(2(x1)))	→	2#(2(x1))	(119)
  3#(5(2(x1)))	→	2#(3(3(2(1(2(x1))))))	(124)
  3#(5(2(x1)))	→	3#(3(2(1(2(x1)))))	(125)
  3#(5(2(x1)))	→	3#(2(1(2(x1))))	(126)
  3#(5(2(x1)))	→	2#(1(2(x1)))	(127)
  3#(5(2(x1)))	→	1#(2(x1))	(128)
  3#(5(3(x1)))	→	4#(2(x1))	(137)
  4#(5(2(x1)))	→	4#(x1)	(154)
  4#(5(4(x1)))	→	4#(2(x1))	(158)
  4#(5(4(x1)))	→	2#(x1)	(159)
  3#(5(3(x1)))	→	2#(x1)	(138)
  3#(5(4(x1)))	→	1#(2(x1))	(142)
  3#(5(4(x1)))	→	2#(x1)	(143)
  5#(5(4(x1)))	→	2#(2(x1))	(172)
  5#(5(4(x1)))	→	2#(x1)	(173)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.