Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3336)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ 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

  4#(5(4(x1)))	→	2#(x1)	(155)
  2#(5(4(x1)))	→	1#(x1)	(93)
  1#(4(5(x1)))	→	1#(x1)	(73)
  1#(2(5(x1)))	→	1#(x1)	(64)
  1#(2(5(x1)))	→	4#(x1)	(60)
  4#(5(2(x1)))	→	4#(x1)	(152)
  4#(5(1(x1)))	→	3#(x1)	(147)
  3#(5(4(x1)))	→	1#(2(x1))	(142)
  3#(5(4(x1)))	→	2#(x1)	(141)
  2#(5(3(x1)))	→	1#(3(3(x1)))	(90)
  2#(5(2(x1)))	→	3#(x1)	(84)
  3#(5(3(x1)))	→	2#(x1)	(134)
  2#(5(1(x1)))	→	1#(2(3(x1)))	(80)
  2#(5(1(x1)))	→	3#(x1)	(78)
  3#(5(2(x1)))	→	1#(2(x1))	(124)
  3#(5(1(x1)))	→	4#(x1)	(107)
  4#(5(x1))	→	1#(3(2(1(x1))))	(54)
  4#(5(x1))	→	1#(x1)	(51)
  3#(5(1(x1)))	→	5#(x1)	(104)
  5#(5(4(x1)))	→	2#(x1)	(169)
  2#(5(x1))	→	1#(x1)	(39)
  5#(5(3(x1)))	→	1#(2(2(x1)))	(166)
  5#(5(3(x1)))	→	2#(x1)	(164)
  3#(5(x1))	→	1#(x1)	(43)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

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

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

  together with the usable rules

  2(5(x1))	→	1(3(3(0(1(0(x1))))))	(1)
  2(5(x1))	→	2(2(0(5(0(1(x1))))))	(2)
  3(5(x1))	→	1(3(2(0(0(1(x1))))))	(3)
  3(5(x1))	→	3(2(0(5(3(0(x1))))))	(4)
  4(5(x1))	→	2(2(1(3(2(1(x1))))))	(5)
  4(5(x1))	→	3(2(0(5(0(0(x1))))))	(6)
  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)
  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)
  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)
  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)

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

  4#(5(4(x1)))	→	2#(x1)	(155)
  2#(5(4(x1)))	→	1#(x1)	(93)
  1#(4(5(x1)))	→	1#(x1)	(73)
  1#(2(5(x1)))	→	1#(x1)	(64)
  1#(2(5(x1)))	→	4#(x1)	(60)
  4#(5(2(x1)))	→	4#(x1)	(152)
  4#(5(1(x1)))	→	3#(x1)	(147)
  3#(5(4(x1)))	→	1#(2(x1))	(142)
  3#(5(4(x1)))	→	2#(x1)	(141)
  2#(5(3(x1)))	→	1#(3(3(x1)))	(90)
  2#(5(2(x1)))	→	3#(x1)	(84)
  3#(5(3(x1)))	→	2#(x1)	(134)
  2#(5(1(x1)))	→	1#(2(3(x1)))	(80)
  2#(5(1(x1)))	→	3#(x1)	(78)
  3#(5(2(x1)))	→	1#(2(x1))	(124)
  3#(5(1(x1)))	→	4#(x1)	(107)
  4#(5(x1))	→	1#(3(2(1(x1))))	(54)
  4#(5(x1))	→	1#(x1)	(51)
  3#(5(1(x1)))	→	5#(x1)	(104)
  5#(5(4(x1)))	→	2#(x1)	(169)
  2#(5(x1))	→	1#(x1)	(39)
  5#(5(3(x1)))	→	1#(2(2(x1)))	(166)
  5#(5(3(x1)))	→	2#(x1)	(164)
  3#(5(x1))	→	1#(x1)	(43)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.