Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212534)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

There are 146 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#(1(2(x1)))	→	0#(4(x1))	(54)
  0#(1(2(x1)))	→	0#(x1)	(52)
  0#(1(2(x1)))	→	4#(x1)	(55)
  4#(2(0(1(2(x1)))))	→	0#(x1)	(181)
  0#(1(2(x1)))	→	4#(0(x1))	(57)
  0#(1(2(x1)))	→	4#(0(4(x1)))	(59)
  0#(1(2(5(x1))))	→	2#(x1)	(74)
  2#(1(1(5(x1))))	→	2#(1(x1))	(89)
  2#(1(0(1(5(x1)))))	→	2#(5(1(x1)))	(142)
  2#(1(0(1(5(x1)))))	→	5#(1(x1))	(143)
  5#(1(4(2(2(x1)))))	→	2#(4(2(x1)))	(187)
  2#(1(4(5(0(x1)))))	→	5#(x1)	(154)
  5#(0(1(2(2(x1)))))	→	5#(2(0(2(x1))))	(183)
  5#(0(1(2(2(x1)))))	→	2#(0(2(x1)))	(184)
  5#(0(1(2(2(x1)))))	→	0#(2(x1))	(185)
  0#(1(4(2(x1))))	→	4#(0(x1))	(76)
  0#(1(4(2(x1))))	→	0#(x1)	(77)
  0#(1(4(2(x1))))	→	4#(x1)	(84)
  0#(1(0(1(2(x1)))))	→	0#(x1)	(103)
  0#(1(1(2(5(x1)))))	→	5#(1(2(x1)))	(105)
  5#(1(4(2(2(x1)))))	→	4#(2(x1))	(188)
  0#(1(1(2(5(x1)))))	→	2#(x1)	(106)
  2#(3(5(5(x1))))	→	2#(5(x1))	(95)
  2#(5(3(2(x1))))	→	2#(2(x1))	(97)
  2#(2(4(3(5(x1)))))	→	4#(2(2(x1)))	(161)
  2#(2(4(3(5(x1)))))	→	2#(2(x1))	(162)
  2#(2(4(3(5(x1)))))	→	2#(x1)	(163)
  2#(1(4(3(5(x1)))))	→	5#(4(4(2(x1))))	(144)
  2#(1(4(3(5(x1)))))	→	4#(4(2(x1)))	(145)
  2#(1(4(3(5(x1)))))	→	4#(2(x1))	(146)
  2#(1(4(3(5(x1)))))	→	2#(x1)	(147)
  2#(3(1(1(2(x1)))))	→	2#(1(2(0(x1))))	(164)
  2#(3(1(1(2(x1)))))	→	2#(0(x1))	(165)
  2#(3(1(1(2(x1)))))	→	0#(x1)	(166)
  0#(1(1(4(2(x1)))))	→	2#(1(x1))	(109)
  0#(1(1(5(4(x1)))))	→	5#(x1)	(116)
  5#(1(4(3(2(x1)))))	→	4#(2(x1))	(191)
  5#(5(4(3(2(x1)))))	→	4#(5(2(x1)))	(193)
  5#(5(4(3(2(x1)))))	→	5#(2(x1))	(194)
  0#(1(2(3(5(x1)))))	→	4#(5(2(x1)))	(118)
  0#(1(2(3(5(x1)))))	→	5#(2(x1))	(119)
  0#(1(2(3(5(x1)))))	→	2#(x1)	(120)
  2#(3(3(1(5(x1)))))	→	2#(x1)	(174)
  2#(5(0(3(5(x1)))))	→	0#(5(x1))	(177)
  0#(1(4(0(2(x1)))))	→	0#(x1)	(137)
  0#(1(2(3(5(x1)))))	→	0#(2(5(x1)))	(126)
  0#(1(2(3(5(x1)))))	→	2#(5(x1))	(127)
  0#(1(2(3(5(x1)))))	→	0#(2(0(x1)))	(129)
  0#(1(2(3(5(x1)))))	→	2#(0(x1))	(130)
  0#(1(2(3(5(x1)))))	→	0#(x1)	(131)
  0#(4(5(3(5(x1)))))	→	4#(5(x1))	(140)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  0#(1(2(5(x1))))	→	2#(x1)	(74)
  2#(1(1(5(x1))))	→	2#(1(x1))	(89)
  5#(1(4(2(2(x1)))))	→	2#(4(2(x1)))	(187)
  5#(0(1(2(2(x1)))))	→	2#(0(2(x1)))	(184)
  5#(0(1(2(2(x1)))))	→	0#(2(x1))	(185)
  5#(1(4(2(2(x1)))))	→	4#(2(x1))	(188)
  0#(1(1(2(5(x1)))))	→	2#(x1)	(106)
  2#(3(5(5(x1))))	→	2#(5(x1))	(95)
  2#(5(3(2(x1))))	→	2#(2(x1))	(97)
  2#(2(4(3(5(x1)))))	→	4#(2(2(x1)))	(161)
  2#(2(4(3(5(x1)))))	→	2#(2(x1))	(162)
  2#(2(4(3(5(x1)))))	→	2#(x1)	(163)
  2#(1(4(3(5(x1)))))	→	4#(4(2(x1)))	(145)
  2#(1(4(3(5(x1)))))	→	4#(2(x1))	(146)
  2#(1(4(3(5(x1)))))	→	2#(x1)	(147)
  5#(1(4(3(2(x1)))))	→	4#(2(x1))	(191)
  5#(5(4(3(2(x1)))))	→	4#(5(2(x1)))	(193)
  5#(5(4(3(2(x1)))))	→	5#(2(x1))	(194)
  0#(1(2(3(5(x1)))))	→	2#(x1)	(120)
  2#(3(3(1(5(x1)))))	→	2#(x1)	(174)
  2#(5(0(3(5(x1)))))	→	0#(5(x1))	(177)
  0#(1(2(3(5(x1)))))	→	0#(2(0(x1)))	(129)
  0#(1(2(3(5(x1)))))	→	2#(0(x1))	(130)
  0#(1(2(3(5(x1)))))	→	0#(x1)	(131)
  0#(4(5(3(5(x1)))))	→	4#(5(x1))	(140)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 3 components.

  • The 1^st component contains the pair

    0#(1(2(x1)))	→	0#(x1)	(52)
    0#(1(2(x1)))	→	0#(4(x1))	(54)
    0#(1(2(x1)))	→	4#(x1)	(55)
    4#(2(0(1(2(x1)))))	→	0#(x1)	(181)
    0#(1(2(x1)))	→	4#(0(x1))	(57)
    0#(1(2(x1)))	→	4#(0(4(x1)))	(59)
    0#(1(4(2(x1))))	→	4#(0(x1))	(76)
    0#(1(4(2(x1))))	→	0#(x1)	(77)
    0#(1(4(2(x1))))	→	4#(x1)	(84)
    0#(1(0(1(2(x1)))))	→	0#(x1)	(103)
    0#(1(2(3(5(x1)))))	→	4#(5(2(x1)))	(118)
    0#(1(2(3(5(x1)))))	→	0#(2(5(x1)))	(126)
    0#(1(4(0(2(x1)))))	→	0#(x1)	(137)

    1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pairs

    0#(1(2(x1)))	→	0#(x1)	(52)
    0#(1(2(x1)))	→	0#(4(x1))	(54)
    0#(1(2(x1)))	→	4#(x1)	(55)
    4#(2(0(1(2(x1)))))	→	0#(x1)	(181)
    0#(1(2(x1)))	→	4#(0(x1))	(57)
    0#(1(2(x1)))	→	4#(0(4(x1)))	(59)
    0#(1(4(2(x1))))	→	4#(0(x1))	(76)
    0#(1(4(2(x1))))	→	0#(x1)	(77)
    0#(1(4(2(x1))))	→	4#(x1)	(84)
    0#(1(0(1(2(x1)))))	→	0#(x1)	(103)
    0#(1(2(3(5(x1)))))	→	4#(5(2(x1)))	(118)
    0#(1(4(0(2(x1)))))	→	0#(x1)	(137)

    could be deleted.

    1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    2(1(1(5(x1))))	→	2(5(1(4(1(x1)))))	(15)
    2(1(1(5(x1))))	→	5(1(3(2(1(x1)))))	(16)
    2(1(2(0(x1))))	→	2(2(1(0(3(x1)))))	(17)
    2(3(5(5(x1))))	→	5(1(0(3(2(5(x1))))))	(18)
    2(5(3(2(x1))))	→	5(1(3(2(2(x1)))))	(19)
    2(1(0(1(5(x1)))))	→	1(0(3(2(5(1(x1))))))	(33)
    2(1(4(3(5(x1)))))	→	1(3(5(4(4(2(x1))))))	(34)
    2(1(4(3(5(x1)))))	→	5(4(4(1(3(2(x1))))))	(35)
    2(1(4(5(0(x1)))))	→	2(4(1(0(3(5(x1))))))	(36)
    2(2(3(5(0(x1)))))	→	5(2(4(2(0(3(x1))))))	(37)
    2(2(4(3(5(x1)))))	→	5(1(3(4(2(2(x1))))))	(38)
    2(3(1(1(2(x1)))))	→	1(3(2(1(2(0(x1))))))	(39)
    2(3(1(1(2(x1)))))	→	4(1(2(2(1(3(x1))))))	(40)
    2(3(2(0(5(x1)))))	→	2(2(1(0(3(5(x1))))))	(41)
    2(3(3(1(5(x1)))))	→	1(3(5(1(3(2(x1))))))	(42)
    2(5(0(3(5(x1)))))	→	5(2(1(3(0(5(x1))))))	(43)

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

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

    →

    0#(2(5(x1)))

    (126)

    could be deleted.

    1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.

  • The 2^nd component contains the pair

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

    →

    2#(5(1(x1)))

    (142)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    5(1(2(0(x1))))	→	2(5(1(0(3(x1)))))	(20)
    5(1(4(2(2(x1)))))	→	5(1(3(2(4(2(x1))))))	(46)
    5(1(4(3(2(x1)))))	→	4(5(1(3(4(2(x1))))))	(47)

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

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

    →

    2#(5(1(x1)))

    (142)

    could be deleted.

    1.1.1.1.2.1 P is empty

    There are no pairs anymore.

  • The 3^rd component contains the pair

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

    →

    5#(2(0(2(x1))))

    (183)

    1.1.1.1.3 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    2(1(1(5(x1))))	→	2(5(1(4(1(x1)))))	(15)
    2(1(1(5(x1))))	→	5(1(3(2(1(x1)))))	(16)
    2(1(2(0(x1))))	→	2(2(1(0(3(x1)))))	(17)
    2(3(5(5(x1))))	→	5(1(0(3(2(5(x1))))))	(18)
    2(5(3(2(x1))))	→	5(1(3(2(2(x1)))))	(19)
    2(1(0(1(5(x1)))))	→	1(0(3(2(5(1(x1))))))	(33)
    2(1(4(3(5(x1)))))	→	1(3(5(4(4(2(x1))))))	(34)
    2(1(4(3(5(x1)))))	→	5(4(4(1(3(2(x1))))))	(35)
    2(1(4(5(0(x1)))))	→	2(4(1(0(3(5(x1))))))	(36)
    2(2(3(5(0(x1)))))	→	5(2(4(2(0(3(x1))))))	(37)
    2(2(4(3(5(x1)))))	→	5(1(3(4(2(2(x1))))))	(38)
    2(3(1(1(2(x1)))))	→	1(3(2(1(2(0(x1))))))	(39)
    2(3(1(1(2(x1)))))	→	4(1(2(2(1(3(x1))))))	(40)
    2(3(2(0(5(x1)))))	→	2(2(1(0(3(5(x1))))))	(41)
    2(3(3(1(5(x1)))))	→	1(3(5(1(3(2(x1))))))	(42)
    2(5(0(3(5(x1)))))	→	5(2(1(3(0(5(x1))))))	(43)

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

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

    →

    5#(2(0(2(x1))))

    (183)

    could be deleted.

    1.1.1.1.3.1 P is empty

    There are no pairs anymore.