Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212263)

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

  2#(5(2(1(0(x1)))))	→	2#(x1)	(123)
  2#(2(4(0(5(x1)))))	→	2#(x1)	(136)
  2#(4(1(5(4(x1)))))	→	2#(x1)	(133)
  2#(4(2(1(0(x1)))))	→	2#(4(x1))	(121)
  2#(2(1(5(x1))))	→	2#(x1)	(119)
  2#(2(0(5(x1))))	→	2#(x1)	(114)
  2#(2(5(4(x1))))	→	2#(x1)	(111)
  2#(2(1(0(x1))))	→	2#(2(0(x1)))	(96)

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

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

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

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

  2#(5(2(1(0(x1)))))	→	2#(x1)	(123)
  2#(2(4(0(5(x1)))))	→	2#(x1)	(136)
  2#(4(2(1(0(x1)))))	→	2#(4(x1))	(121)
  2#(2(0(5(x1))))	→	2#(x1)	(114)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    2#(4(1(5(4(x1)))))	→	2#(x1)	(133)
    2#(2(1(5(x1))))	→	2#(x1)	(119)
    2#(2(5(4(x1))))	→	2#(x1)	(111)

    1.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(1(5(4(x1)))))	→	2#(x1)	(133)
    1	>	1
    2#(2(1(5(x1))))	→	2#(x1)	(119)
    1	>	1
    2#(2(5(4(x1))))	→	2#(x1)	(111)
    1	>	1

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