Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/85477)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

1.1 Dependency Pair Transformation

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

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

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

  →

  2#(x1)

  (210)

  1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  2#(4(5(2(1(3(5(5(1(1(1(0(0(4(5(0(1(2(0(2(5(x1)))))))))))))))))))))	→	2#(x1)	(210)
  1	>	1

  As there is no critical graph in the transitive closure, there are no infinite chains.

• The 2^nd component contains the pair

  2#(5(1(2(0(0(5(1(2(2(1(0(2(1(5(x1)))))))))))))))	→	3#(4(3(4(1(x1)))))	(109)
  3#(4(2(2(1(5(3(3(2(x1)))))))))	→	0#(3(5(3(3(0(2(x1)))))))	(40)
  0#(0(1(2(2(x1)))))	→	2#(3(3(2(2(x1)))))	(31)
  2#(5(1(2(0(0(5(1(2(2(1(0(2(1(5(x1)))))))))))))))	→	3#(4(1(x1)))	(110)
  3#(4(2(2(1(5(3(3(2(x1)))))))))	→	0#(2(x1))	(45)
  0#(5(5(3(1(3(3(0(2(0(x1))))))))))	→	2#(5(0(4(0(5(0(x1)))))))	(49)
  0#(5(5(3(1(3(3(0(2(0(x1))))))))))	→	0#(5(0(x1)))	(52)

  1.1.1.2 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  1(2(1(3(4(2(4(4(1(2(5(2(3(3(3(5(1(0(0(x1)))))))))))))))))))	→	1(5(3(2(5(0(5(2(3(0(0(3(1(5(3(4(4(3(0(x1)))))))))))))))))))	(25)
  3(4(2(2(1(5(3(3(2(x1)))))))))	→	3(1(0(3(5(3(3(0(2(x1)))))))))	(4)
  3(2(0(0(4(0(0(0(2(5(1(0(x1))))))))))))	→	1(5(2(4(0(4(2(0(0(5(0(2(x1))))))))))))	(9)
  5(2(3(1(2(1(5(4(5(1(1(0(0(x1)))))))))))))	→	5(2(0(5(4(3(4(3(3(0(5(0(0(x1)))))))))))))	(15)

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

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

  →

  2#(3(3(2(2(x1)))))

  (31)

  could be deleted.

  1.1.1.2.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  1(2(1(3(4(2(4(4(1(2(5(2(3(3(3(5(1(0(0(x1)))))))))))))))))))	→	1(5(3(2(5(0(5(2(3(0(0(3(1(5(3(4(4(3(0(x1)))))))))))))))))))	(25)
  3(4(2(2(1(5(3(3(2(x1)))))))))	→	3(1(0(3(5(3(3(0(2(x1)))))))))	(4)
  2(1(3(3(4(3(0(2(0(4(0(3(1(x1)))))))))))))	→	2(4(1(3(0(1(3(3(2(1(3(4(4(x1)))))))))))))	(13)
  2(5(0(2(2(0(3(3(1(4(2(5(0(0(0(x1)))))))))))))))	→	5(3(1(3(1(4(4(2(5(4(5(4(4(1(0(x1)))))))))))))))	(16)
  2(5(1(2(0(0(5(1(2(2(1(0(2(1(5(x1)))))))))))))))	→	0(3(2(5(5(2(4(4(3(5(3(4(3(4(1(x1)))))))))))))))	(17)
  2(4(5(2(1(3(5(5(1(1(1(0(0(4(5(0(1(2(0(2(5(x1)))))))))))))))))))))	→	2(0(0(2(2(1(2(1(2(2(2(0(5(3(3(2(5(2(2(5(2(x1)))))))))))))))))))))	(29)
  3(2(0(0(4(0(0(0(2(5(1(0(x1))))))))))))	→	1(5(2(4(0(4(2(0(0(5(0(2(x1))))))))))))	(9)
  5(2(3(1(2(1(5(4(5(1(1(0(0(x1)))))))))))))	→	5(2(0(5(4(3(4(3(3(0(5(0(0(x1)))))))))))))	(15)

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

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

  →

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

  (40)

  could be deleted.

  1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  1(2(1(3(4(2(4(4(1(2(5(2(3(3(3(5(1(0(0(x1)))))))))))))))))))	→	1(5(3(2(5(0(5(2(3(0(0(3(1(5(3(4(4(3(0(x1)))))))))))))))))))	(25)
  3(4(2(2(1(5(3(3(2(x1)))))))))	→	3(1(0(3(5(3(3(0(2(x1)))))))))	(4)
  3(2(0(0(4(0(0(0(2(5(1(0(x1))))))))))))	→	1(5(2(4(0(4(2(0(0(5(0(2(x1))))))))))))	(9)

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

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

  →

  0#(2(x1))

  (45)

  could be deleted.

  1.1.1.2.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

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

    →

    0#(5(0(x1)))

    (52)

    1.1.1.2.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

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

    →

    0#(5(0(x1)))

    (52)

    could be deleted.

    1.1.1.2.1.1.1.1.1 P is empty

    There are no pairs anymore.