Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/160234)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

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

  5#(5(1(4(5(x1)))))	→	5#(5(x1))	(211)
  5#(4(0(2(1(x1)))))	→	5#(2(0(x1)))	(209)
  5#(4(0(2(1(x1)))))	→	2#(0(x1))	(208)
  2#(5(1(5(2(x1)))))	→	1#(5(5(2(x1))))	(198)
  1#(4(0(1(5(x1)))))	→	0#(5(x1))	(180)
  0#(5(0(1(5(x1)))))	→	1#(x1)	(167)
  1#(0(1(4(5(x1)))))	→	1#(0(5(x1)))	(178)
  1#(0(1(4(5(x1)))))	→	0#(5(x1))	(177)
  0#(4(0(2(1(x1)))))	→	1#(2(0(x1)))	(165)
  1#(0(0(1(5(x1)))))	→	1#(x1)	(172)
  1#(5(1(5(x1))))	→	1#(x1)	(96)
  1#(1(4(5(x1))))	→	1#(x1)	(93)
  0#(4(0(2(1(x1)))))	→	2#(0(x1))	(164)
  2#(5(1(5(2(x1)))))	→	5#(5(2(x1)))	(197)
  5#(4(0(2(1(x1)))))	→	0#(x1)	(207)
  0#(4(0(2(1(x1)))))	→	0#(x1)	(163)
  0#(2(4(2(1(x1)))))	→	0#(x1)	(159)
  0#(1(5(0(5(x1)))))	→	5#(1(0(5(0(x1)))))	(158)
  5#(1(0(1(5(x1)))))	→	1#(5(1(0(5(x1)))))	(206)
  5#(1(0(1(5(x1)))))	→	5#(1(0(5(x1))))	(205)
  5#(1(0(1(5(x1)))))	→	1#(0(5(x1)))	(204)
  5#(1(0(1(5(x1)))))	→	0#(5(x1))	(203)
  0#(1(5(0(5(x1)))))	→	1#(0(5(0(x1))))	(157)
  0#(1(5(0(5(x1)))))	→	0#(5(0(x1)))	(156)
  0#(1(5(0(5(x1)))))	→	5#(0(x1))	(155)
  5#(0(1(4(5(x1)))))	→	5#(5(x1))	(200)
  5#(0(1(2(x1))))	→	0#(5(1(x1)))	(115)
  5#(0(1(2(x1))))	→	5#(1(x1))	(114)
  5#(0(1(2(x1))))	→	1#(x1)	(113)
  0#(1(5(0(5(x1)))))	→	0#(x1)	(154)
  0#(1(4(2(5(x1)))))	→	0#(5(1(x1)))	(145)
  0#(1(4(2(5(x1)))))	→	5#(1(x1))	(144)
  0#(1(4(2(5(x1)))))	→	1#(x1)	(143)
  0#(1(3(5(2(x1)))))	→	1#(5(2(x1)))	(141)
  0#(1(2(1(5(x1)))))	→	1#(x1)	(136)
  0#(1(0(4(5(x1)))))	→	1#(x1)	(130)
  0#(0(1(2(5(x1)))))	→	1#(x1)	(122)
  0#(2(5(2(x1))))	→	0#(5(x1))	(90)
  0#(2(5(2(x1))))	→	5#(x1)	(89)
  0#(2(1(2(x1))))	→	1#(x1)	(85)
  0#(1(5(5(x1))))	→	0#(5(5(x1)))	(83)
  0#(1(5(2(x1))))	→	0#(5(2(x1)))	(81)
  0#(1(5(2(x1))))	→	1#(0(5(x1)))	(79)
  0#(1(5(2(x1))))	→	0#(5(x1))	(78)
  0#(1(5(2(x1))))	→	5#(x1)	(74)
  0#(1(2(5(x1))))	→	1#(x1)	(67)
  0#(1(2(2(x1))))	→	1#(2(x1))	(64)
  0#(1(2(1(x1))))	→	0#(1(2(4(1(3(x1))))))	(63)
  0#(1(2(x1)))	→	1#(x1)	(48)
  0#(1(1(2(x1))))	→	1#(1(x1))	(57)
  0#(1(1(2(x1))))	→	1#(x1)	(56)
  2#(0(5(1(2(x1)))))	→	1#(5(2(2(x1))))	(192)
  2#(0(5(1(2(x1)))))	→	5#(2(2(x1)))	(191)
  2#(0(5(1(2(x1)))))	→	2#(2(x1))	(190)
  2#(0(4(2(1(x1)))))	→	0#(x1)	(186)
  2#(0(1(5(x1))))	→	0#(5(x1))	(108)
  2#(0(1(2(x1))))	→	1#(x1)	(104)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(5#)	=	0		stat(5#)	=	lex
  prec(2#)	=	0		stat(2#)	=	lex
  prec(1#)	=	0		stat(1#)	=	lex
  prec(0#)	=	0		stat(0#)	=	lex
  prec(5)	=	0		stat(5)	=	lex
  prec(4)	=	0		stat(4)	=	lex
  prec(3)	=	0		stat(3)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(1)	=	0		stat(1)	=	lex
  prec(2)	=	0		stat(2)	=	lex

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

  together with the usable rules

  0(1(2(x1)))	→	2(3(0(3(1(x1)))))	(1)
  0(0(0(2(x1))))	→	3(0(0(3(0(2(x1))))))	(2)
  0(0(2(2(x1))))	→	2(3(0(0(3(2(x1))))))	(3)
  0(1(1(2(x1))))	→	2(3(0(3(1(1(x1))))))	(4)
  0(1(2(1(x1))))	→	0(1(2(4(1(3(x1))))))	(5)
  0(1(2(2(x1))))	→	2(3(0(3(1(2(x1))))))	(6)
  0(1(2(5(x1))))	→	2(0(5(3(1(x1)))))	(7)
  0(1(5(1(x1))))	→	1(0(3(5(3(1(x1))))))	(8)
  0(1(5(2(x1))))	→	2(4(1(0(3(5(x1))))))	(9)
  0(1(5(2(x1))))	→	2(4(3(1(0(5(x1))))))	(10)
  0(1(5(2(x1))))	→	3(1(3(0(5(2(x1))))))	(11)
  0(1(5(5(x1))))	→	1(3(0(5(5(x1)))))	(12)
  0(2(1(2(x1))))	→	2(2(3(0(3(1(x1))))))	(13)
  0(2(5(2(x1))))	→	2(2(3(0(5(x1)))))	(14)
  1(1(4(5(x1))))	→	5(4(1(3(1(x1)))))	(15)
  1(5(1(5(x1))))	→	1(3(5(5(3(1(x1))))))	(16)
  1(5(5(1(x1))))	→	1(5(3(1(5(3(x1))))))	(17)
  2(0(1(2(x1))))	→	2(2(3(0(3(1(x1))))))	(18)
  2(0(1(5(x1))))	→	2(1(3(0(5(x1)))))	(19)
  5(0(1(2(x1))))	→	3(0(5(3(1(2(x1))))))	(20)
  5(0(1(2(x1))))	→	4(2(3(0(5(1(x1))))))	(21)
  0(0(0(0(1(x1)))))	→	0(0(1(0(0(3(x1))))))	(22)
  0(0(1(2(5(x1)))))	→	2(0(0(5(3(1(x1))))))	(23)
  0(0(1(5(2(x1)))))	→	0(1(0(3(5(2(x1))))))	(24)
  0(1(0(4(5(x1)))))	→	5(4(0(0(3(1(x1))))))	(25)
  0(1(1(1(2(x1)))))	→	1(0(3(1(1(2(x1))))))	(26)
  0(1(2(1(5(x1)))))	→	2(1(0(5(3(1(x1))))))	(27)
  0(1(3(5(2(x1)))))	→	3(0(4(1(5(2(x1))))))	(28)
  0(1(4(2(5(x1)))))	→	2(4(3(0(5(1(x1))))))	(29)
  0(1(4(4(2(x1)))))	→	1(0(4(4(4(2(x1))))))	(30)
  0(1(5(0(1(x1)))))	→	0(1(1(0(5(3(x1))))))	(31)
  0(1(5(0(5(x1)))))	→	3(5(1(0(5(0(x1))))))	(32)
  0(2(4(2(1(x1)))))	→	2(1(2(4(3(0(x1))))))	(33)
  0(4(0(2(1(x1)))))	→	3(0(4(1(2(0(x1))))))	(34)
  0(5(0(1(5(x1)))))	→	0(5(0(5(3(1(x1))))))	(35)
  1(0(0(1(5(x1)))))	→	5(1(0(0(3(1(x1))))))	(36)
  1(0(1(4(5(x1)))))	→	1(4(4(1(0(5(x1))))))	(37)
  1(4(0(1(5(x1)))))	→	1(4(1(3(0(5(x1))))))	(38)
  2(0(1(5(2(x1)))))	→	2(1(0(3(5(2(x1))))))	(39)
  2(0(4(2(1(x1)))))	→	2(1(4(2(3(0(x1))))))	(40)
  2(0(5(1(2(x1)))))	→	0(3(1(5(2(2(x1))))))	(41)
  2(2(1(1(2(x1)))))	→	2(2(1(3(1(2(x1))))))	(42)
  2(5(1(5(2(x1)))))	→	2(4(1(5(5(2(x1))))))	(43)
  5(0(1(4(5(x1)))))	→	4(1(0(3(5(5(x1))))))	(44)
  5(1(0(1(5(x1)))))	→	3(1(5(1(0(5(x1))))))	(45)
  5(4(0(2(1(x1)))))	→	4(1(3(5(2(0(x1))))))	(46)
  5(5(1(4(5(x1)))))	→	5(4(1(3(5(5(x1))))))	(47)

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

  5#(5(1(4(5(x1)))))	→	5#(5(x1))	(211)
  5#(4(0(2(1(x1)))))	→	5#(2(0(x1)))	(209)
  5#(4(0(2(1(x1)))))	→	2#(0(x1))	(208)
  2#(5(1(5(2(x1)))))	→	1#(5(5(2(x1))))	(198)
  1#(4(0(1(5(x1)))))	→	0#(5(x1))	(180)
  0#(5(0(1(5(x1)))))	→	1#(x1)	(167)
  1#(0(1(4(5(x1)))))	→	1#(0(5(x1)))	(178)
  1#(0(1(4(5(x1)))))	→	0#(5(x1))	(177)
  0#(4(0(2(1(x1)))))	→	1#(2(0(x1)))	(165)
  1#(0(0(1(5(x1)))))	→	1#(x1)	(172)
  1#(5(1(5(x1))))	→	1#(x1)	(96)
  1#(1(4(5(x1))))	→	1#(x1)	(93)
  0#(4(0(2(1(x1)))))	→	2#(0(x1))	(164)
  2#(5(1(5(2(x1)))))	→	5#(5(2(x1)))	(197)
  5#(4(0(2(1(x1)))))	→	0#(x1)	(207)
  0#(4(0(2(1(x1)))))	→	0#(x1)	(163)
  0#(2(4(2(1(x1)))))	→	0#(x1)	(159)
  5#(1(0(1(5(x1)))))	→	1#(5(1(0(5(x1)))))	(206)
  5#(1(0(1(5(x1)))))	→	5#(1(0(5(x1))))	(205)
  5#(1(0(1(5(x1)))))	→	1#(0(5(x1)))	(204)
  5#(1(0(1(5(x1)))))	→	0#(5(x1))	(203)
  0#(1(5(0(5(x1)))))	→	1#(0(5(0(x1))))	(157)
  0#(1(5(0(5(x1)))))	→	0#(5(0(x1)))	(156)
  0#(1(5(0(5(x1)))))	→	5#(0(x1))	(155)
  5#(0(1(4(5(x1)))))	→	5#(5(x1))	(200)
  5#(0(1(2(x1))))	→	1#(x1)	(113)
  0#(1(5(0(5(x1)))))	→	0#(x1)	(154)
  0#(1(4(2(5(x1)))))	→	1#(x1)	(143)
  0#(1(3(5(2(x1)))))	→	1#(5(2(x1)))	(141)
  0#(1(2(1(5(x1)))))	→	1#(x1)	(136)
  0#(1(0(4(5(x1)))))	→	1#(x1)	(130)
  0#(0(1(2(5(x1)))))	→	1#(x1)	(122)
  0#(2(1(2(x1))))	→	1#(x1)	(85)
  0#(1(5(5(x1))))	→	0#(5(5(x1)))	(83)
  0#(1(5(2(x1))))	→	0#(5(2(x1)))	(81)
  0#(1(5(2(x1))))	→	1#(0(5(x1)))	(79)
  0#(1(5(2(x1))))	→	0#(5(x1))	(78)
  0#(1(5(2(x1))))	→	5#(x1)	(74)
  0#(1(2(5(x1))))	→	1#(x1)	(67)
  0#(1(2(2(x1))))	→	1#(2(x1))	(64)
  0#(1(2(x1)))	→	1#(x1)	(48)
  0#(1(1(2(x1))))	→	1#(1(x1))	(57)
  0#(1(1(2(x1))))	→	1#(x1)	(56)
  2#(0(5(1(2(x1)))))	→	1#(5(2(2(x1))))	(192)
  2#(0(5(1(2(x1)))))	→	5#(2(2(x1)))	(191)
  2#(0(5(1(2(x1)))))	→	2#(2(x1))	(190)
  2#(0(4(2(1(x1)))))	→	0#(x1)	(186)
  2#(0(1(5(x1))))	→	0#(5(x1))	(108)
  2#(0(1(2(x1))))	→	1#(x1)	(104)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.