Certification Problem

Input (TPDB SRS_Standard/Zantema_06/11)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  l#(r(a(x1)))	→	a#(l(c(c(r(x1)))))	(10)
  a#(l(x1))	→	l#(a(x1))	(5)
  a#(l(x1))	→	a#(x1)	(6)
  a#(c(x1))	→	c#(a(x1))	(7)
  c#(a(r(x1)))	→	a#(x1)	(9)
  a#(c(x1))	→	a#(x1)	(8)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [l#(x1)]	=	1 · x1
  [r(x1)]	=	1 + 1 · x1
  [a(x1)]	=	1 · x1
  [a#(x1)]	=	1 · x1
  [l(x1)]	=	1 · x1
  [c(x1)]	=	1 · x1
  [c#(x1)]	=	1 · x1

  the pair

  c#(a(r(x1)))

  →

  a#(x1)

  (9)

  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

    a#(l(x1))	→	l#(a(x1))	(5)
    l#(r(a(x1)))	→	a#(l(c(c(r(x1)))))	(10)
    a#(l(x1))	→	a#(x1)	(6)
    a#(c(x1))	→	a#(x1)	(8)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [a#(x1)]	=	1 · x1
    [l(x1)]	=	1 + 1 · x1
    [l#(x1)]	=	1
    [a(x1)]	=	0
    [r(x1)]	=	0
    [c(x1)]	=	1 · x1

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

    a#(l(x1))

    →

    a#(x1)

    (6)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 2 components.

    • The 1^st component contains the pair

      a#(c(x1))

      →

      a#(x1)

      (8)

      1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [c(x1)]	=	1 · x1
      [a#(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.1.1.1 Size-Change Termination

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

      a#(c(x1))	→	a#(x1)	(8)
      1	>	1

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

    • The 2^nd component contains the pair

      l#(r(a(x1)))	→	a#(l(c(c(r(x1)))))	(10)
      a#(l(x1))	→	l#(a(x1))	(5)

      1.1.1.1.1.1.2 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

      [l#(x1)]	=	x1
      [l(x1)]	=	2 + x1
      [r(x1)]	=	2
      [a(x1)]	=	1 + x1
      [c(x1)]	=	-1 + x1
      [a#(x1)]	=	-2 + 2 · x1

      the pair

      a#(l(x1))

      →

      l#(a(x1))

      (5)

      could be deleted.

      1.1.1.1.1.1.2.1 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [r(x1)]	=	1 · x1
      [a(x1)]	=	1 · x1
      [l(x1)]	=	1 · x1
      [c(x1)]	=	1 · x1
      [a#(x1)]	=	1 · x1
      [l#(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.1.2.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

      [l#(x1)]	=	1 + 1 · x1
      [r(x1)]	=	1 + 1 · x1
      [a(x1)]	=	1 + 1 · x1
      [a#(x1)]	=	1 · x1
      [l(x1)]	=	1 + 1 · x1
      [c(x1)]	=	1

      the pair

      l#(r(a(x1)))

      →

      a#(l(c(c(r(x1)))))

      (10)

      could be deleted.

      1.1.1.1.1.1.2.1.1.1 P is empty

      There are no pairs anymore.