Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/27280)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  1#(2(1(0(x1))))	→	1#(2(1(x1)))	(36)
  1#(2(1(0(x1))))	→	1#(1(2(1(x1))))	(37)
  1#(2(1(0(x1))))	→	1#(x1)	(35)

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [2(x1)]	=	-6 · x1 + 0
  [1#(x1)]	=	0 · x1 + 0
  [1(x1)]	=	0 · x1 + 0
  [0(x1)]	=	6 · x1 + 7

  together with the usable rules

  1(2(1(0(x1))))	→	2(1(0(2(1(0(1(1(2(1(x1))))))))))	(18)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))	(19)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))	(20)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))	(21)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))	(22)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))	(23)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))	(24)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))	(25)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))	(26)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))	(27)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))	(28)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))))	(29)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	(30)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))	(31)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(32)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(33)
  1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(34)

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

  1#(2(1(0(x1))))	→	1#(2(1(x1)))	(36)
  1#(2(1(0(x1))))	→	1#(1(2(1(x1))))	(37)

  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.

  1#(2(1(0(x1))))	→	1#(x1)	(35)
  1	>	1

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