Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/214011)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

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

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

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

  →

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

  (117)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

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

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

  together with the usable rules

  5(1(3(x1)))	→	5(3(1(2(x1))))	(8)
  5(1(2(3(x1))))	→	5(5(3(1(2(x1)))))	(21)
  3(2(4(1(3(x1)))))	→	4(3(4(3(1(2(x1))))))	(39)

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

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

  →

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

  (117)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  5#(5(0(1(x1))))	→	5#(5(x1))	(97)
  5#(2(4(2(3(x1)))))	→	5#(3(2(x1)))	(153)
  5#(2(4(2(3(x1)))))	→	3#(2(x1))	(152)
  3#(2(0(1(x1))))	→	5#(x1)	(75)
  5#(5(0(1(x1))))	→	5#(x1)	(96)
  5#(4(3(3(x1))))	→	5#(x1)	(93)

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the

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

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

  together with the usable rules

  5(1(3(x1)))	→	5(3(1(2(x1))))	(8)
  5(1(2(3(x1))))	→	5(5(3(1(2(x1)))))	(21)
  5(2(0(1(x1))))	→	5(3(1(0(2(4(x1))))))	(22)
  5(4(3(3(x1))))	→	3(1(3(4(5(x1)))))	(23)
  5(5(0(1(x1))))	→	1(0(2(4(5(5(x1))))))	(24)
  5(2(4(2(3(x1)))))	→	3(2(4(5(3(2(x1))))))	(44)
  5(4(2(0(1(x1)))))	→	5(1(2(0(2(4(x1))))))	(45)
  3(2(4(1(3(x1)))))	→	4(3(4(3(1(2(x1))))))	(39)
  3(2(0(1(x1))))	→	1(3(0(2(4(5(x1))))))	(16)

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

  5#(5(0(1(x1))))	→	5#(5(x1))	(97)
  3#(2(0(1(x1))))	→	5#(x1)	(75)
  5#(5(0(1(x1))))	→	5#(x1)	(96)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    5#(4(3(3(x1))))	→	5#(x1)	(93)
    5#(2(4(2(3(x1)))))	→	5#(3(2(x1)))	(153)

    1.1.2.1.1 Reduction Pair Processor with Usable Rules

    Using the

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

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

    together with the usable rules

    3(2(0(1(x1))))	→	1(3(0(2(4(5(x1))))))	(16)
    3(2(4(1(3(x1)))))	→	4(3(4(3(1(2(x1))))))	(39)

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

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

    →

    5#(3(2(x1)))

    (153)

    could be deleted.

    1.1.2.1.1.1 Size-Change Termination

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

    5#(4(3(3(x1))))	→	5#(x1)	(93)
    1	>	1

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