Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/aprove07)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  bar#(s(x1))	→	foo#(s(p(p(s(s(x1))))))	(29)
  foo#(s(x1))	→	foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))	(19)
  foo#(s(x1))	→	bar#(p(p(s(s(p(s(x1)))))))	(15)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [bar(x1)]	=	1 · x1 + 0
  [foo(x1)]	=	0 · x1 + -16
  [p(x1)]	=	-1 · x1 + 0
  [foo#(x1)]	=	0 · x1 + 0
  [0(x1)]	=	-∞ · x1 + 0
  [bar#(x1)]	=	0 · x1 + 0
  [s(x1)]	=	1 · x1 + 1

  together with the usable rules

  foo(0(x1))	→	0(s(p(p(p(s(s(s(p(s(x1))))))))))	(1)
  foo(s(x1))	→	p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))	(2)
  bar(0(x1))	→	0(p(s(s(s(x1)))))	(3)
  bar(s(x1))	→	p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))	(4)
  p(p(s(x1)))	→	p(x1)	(5)
  p(s(x1))	→	x1	(6)
  p(0(x1))	→	0(s(s(s(s(x1)))))	(7)

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

  foo#(s(x1))

  →

  bar#(p(p(s(s(p(s(x1)))))))

  (15)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    foo#(s(x1))

    →

    foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))

    (19)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [bar(x1)]	=	0 · x1 + 0
    [foo(x1)]	=	-6 · x1 + 1
    [p(x1)]	=	-1 · x1 + 0
    [foo#(x1)]	=	4 · x1 + 0
    [0(x1)]	=	-∞ · x1 + 0
    [s(x1)]	=	1 · x1 + 1

    together with the usable rules

    foo(0(x1))	→	0(s(p(p(p(s(s(s(p(s(x1))))))))))	(1)
    foo(s(x1))	→	p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))	(2)
    bar(0(x1))	→	0(p(s(s(s(x1)))))	(3)
    bar(s(x1))	→	p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))	(4)
    p(p(s(x1)))	→	p(x1)	(5)
    p(s(x1))	→	x1	(6)
    p(0(x1))	→	0(s(s(s(s(x1)))))	(7)

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

    foo#(s(x1))

    →

    foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))

    (19)

    could be deleted.

    1.1.1.1.1.1 P is empty

    There are no pairs anymore.

• The 2^nd component contains the pair

  p#(p(s(x1)))

  →

  p#(x1)

  (33)

  1.1.2 Size-Change Termination

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

  p#(p(s(x1)))	→	p#(x1)	(33)
  1	>	1

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