Certification Problem

Input (TPDB SRS_Standard/Waldmann_06_SRS/e)

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 2 components.

• The 1^st component contains the pair

  4#(x1)	→	9#(6(6(x1)))	(37)
  9#(7(x1))	→	7#(5(x1))	(31)
  7#(0(x1))	→	9#(3(x1))	(34)
  9#(x1)	→	7#(x1)	(41)
  7#(2(x1))	→	4#(x1)	(33)
  4#(x1)	→	6#(x1)	(39)
  6#(2(x1))	→	7#(7(x1))	(42)
  6#(2(x1))	→	7#(x1)	(43)
  9#(7(x1))	→	5#(x1)	(32)
  5#(2(6(x1)))	→	6#(2(4(x1)))	(28)
  5#(2(6(x1)))	→	2#(4(x1))	(29)
  2#(8(x1))	→	4#(x1)	(21)
  2#(8(x1))	→	7#(x1)	(27)
  2#(4(x1))	→	7#(x1)	(45)
  5#(2(6(x1)))	→	4#(x1)	(30)
  9#(5(9(x1)))	→	7#(x1)	(36)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [4#(x1)]	=	0
  [9#(x1)]	=	0
  [6(x1)]	=	0
  [7(x1)]	=	0
  [7#(x1)]	=	0
  [5(x1)]	=	0
  [0(x1)]	=	0
  [3(x1)]	=	0
  [2(x1)]	=	0
  [6#(x1)]	=	0
  [5#(x1)]	=	0
  [4(x1)]	=	0
  [2#(x1)]	=	1 · x1
  [8(x1)]	=	1
  [9(x1)]	=	0
  [1(x1)]	=	0

  together with the usable rules

  0(3(x1))	→	5(3(x1))	(20)
  5(3(x1))	→	6(0(x1))	(6)
  6(9(x1))	→	9(x1)	(13)
  9(7(x1))	→	7(5(x1))	(10)
  7(2(x1))	→	4(x1)	(11)
  4(x1)	→	9(6(6(x1)))	(15)
  9(5(9(x1)))	→	5(7(x1))	(14)
  5(9(x1))	→	0(x1)	(4)
  5(2(6(x1)))	→	6(2(4(x1)))	(9)
  6(2(x1))	→	7(7(x1))	(17)
  7(0(x1))	→	9(3(x1))	(12)
  9(x1)	→	6(7(x1))	(16)
  6(6(x1))	→	3(x1)	(19)
  4(x1)	→	5(2(3(x1)))	(5)
  4(7(x1))	→	1(3(x1))	(8)

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

  2#(8(x1))	→	4#(x1)	(21)
  2#(8(x1))	→	7#(x1)	(27)

  could be deleted.

  1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

  [4#(x1)]	=	1 -∞ -∞ + 1 1 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [9#(x1)]	=	1 -∞ -∞ + 0 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [6(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 -∞ 0 · x1
  [7(x1)]	=	-∞ -∞ 0 + 0 -∞ 0 0 0 0 0 0 0 · x1
  [7#(x1)]	=	1 -∞ -∞ + 0 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [5(x1)]	=	0 -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1
  [0(x1)]	=	0 -∞ -∞ + 0 0 0 0 -∞ 0 0 -∞ 0 · x1
  [3(x1)]	=	0 -∞ 0 + 0 -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1
  [2(x1)]	=	0 0 0 + 0 0 0 0 1 0 0 0 0 · x1
  [6#(x1)]	=	0 -∞ -∞ + 0 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [5#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [4(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
  [2#(x1)]	=	1 -∞ -∞ + -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [9(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
  [1(x1)]	=	0 0 -∞ + -∞ 0 0 -∞ -∞ -∞ 0 -∞ -∞ · x1
  [8(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1

  the pair

  9#(7(x1))

  →

  5#(x1)

  (32)

  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

    9#(7(x1))	→	7#(5(x1))	(31)
    7#(0(x1))	→	9#(3(x1))	(34)
    9#(x1)	→	7#(x1)	(41)
    7#(2(x1))	→	4#(x1)	(33)
    4#(x1)	→	9#(6(6(x1)))	(37)
    9#(5(9(x1)))	→	7#(x1)	(36)
    4#(x1)	→	6#(x1)	(39)
    6#(2(x1))	→	7#(7(x1))	(42)
    6#(2(x1))	→	7#(x1)	(43)

    1.1.1.1.1.1 Reduction Pair Processor

    Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

    [9#(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [7(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 0 0 0 -∞ -∞ 0 · x1
    [7#(x1)]	=	0 -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [5(x1)]	=	0 0 0 + -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ 0 · x1
    [0(x1)]	=	0 0 0 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [3(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [2(x1)]	=	0 1 0 + 0 0 0 0 0 0 0 1 1 · x1
    [4#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [6(x1)]	=	0 0 -∞ + 0 0 -∞ 0 -∞ 0 -∞ 0 0 · x1
    [9(x1)]	=	0 0 -∞ + 0 0 0 -∞ -∞ 0 0 0 0 · x1
    [6#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [4(x1)]	=	0 0 0 + 0 0 1 0 0 0 0 0 0 · x1
    [8(x1)]	=	0 -∞ 0 + 1 1 1 0 0 0 0 -∞ 0 · x1
    [1(x1)]	=	0 0 0 + -∞ 0 -∞ -∞ 0 0 0 -∞ -∞ · x1

    the pair

    6#(2(x1))

    →

    7#(7(x1))

    (42)

    could be deleted.

    1.1.1.1.1.1.1 Reduction Pair Processor

    Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

    [9#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [7(x1)]	=	0 0 0 + 0 -∞ -∞ 0 -∞ 0 0 0 -∞ · x1
    [7#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [5(x1)]	=	0 0 0 + 0 -∞ 0 0 0 0 0 -∞ 0 · x1
    [0(x1)]	=	0 0 -∞ + 0 0 -∞ 0 0 -∞ 0 -∞ -∞ · x1
    [3(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [2(x1)]	=	-∞ 0 -∞ + 0 0 0 0 0 0 0 1 1 · x1
    [4#(x1)]	=	0 -∞ -∞ + 0 1 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [6(x1)]	=	0 0 0 + 0 0 0 0 -∞ 0 0 0 0 · x1
    [9(x1)]	=	0 0 0 + 0 0 0 0 0 -∞ 0 0 0 · x1
    [6#(x1)]	=	0 -∞ -∞ + 0 1 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [4(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
    [8(x1)]	=	0 -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1
    [1(x1)]	=	0 -∞ 0 + 0 -∞ -∞ -∞ 0 0 0 0 0 · x1

    the pair

    6#(2(x1))

    →

    7#(x1)

    (43)

    could be deleted.

    1.1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      7#(0(x1))	→	9#(3(x1))	(34)
      9#(x1)	→	7#(x1)	(41)
      7#(2(x1))	→	4#(x1)	(33)
      4#(x1)	→	9#(6(6(x1)))	(37)
      9#(7(x1))	→	7#(5(x1))	(31)
      9#(5(9(x1)))	→	7#(x1)	(36)

      1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

      [7#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [0(x1)]	=	1 1 0 + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 -∞ · x1
      [9#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [3(x1)]	=	0 1 0 + -∞ -∞ -∞ 0 0 -∞ -∞ -∞ -∞ · x1
      [2(x1)]	=	0 1 1 + 0 0 -∞ 0 0 -∞ 0 0 0 · x1
      [4#(x1)]	=	1 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [6(x1)]	=	0 1 0 + 0 0 -∞ 0 -∞ -∞ 0 0 0 · x1
      [7(x1)]	=	1 1 0 + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1
      [5(x1)]	=	1 1 0 + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1
      [9(x1)]	=	1 1 1 + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1
      [4(x1)]	=	1 1 1 + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1
      [8(x1)]	=	1 0 0 + 0 0 0 0 0 0 0 0 0 · x1
      [1(x1)]	=	1 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ 0 0 0 · x1

      the pair

      7#(0(x1))

      →

      9#(3(x1))

      (34)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        7#(2(x1))	→	4#(x1)	(33)
        4#(x1)	→	9#(6(6(x1)))	(37)
        9#(5(9(x1)))	→	7#(x1)	(36)
        9#(x1)	→	7#(x1)	(41)

        1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

        Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

        [7#(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
        [2(x1)]	=	0 -∞ -∞ + 0 0 1 1 1 1 0 0 0 · x1
        [4#(x1)]	=	0 -∞ -∞ + 1 1 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
        [9#(x1)]	=	0 -∞ -∞ + -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
        [6(x1)]	=	-∞ -∞ 0 + 0 -∞ 0 0 0 -∞ 0 0 0 · x1
        [5(x1)]	=	-∞ 0 -∞ + 0 -∞ -∞ 0 -∞ 0 0 -∞ 0 · x1
        [9(x1)]	=	-∞ 0 0 + 0 0 0 0 -∞ 0 0 0 0 · x1
        [0(x1)]	=	-∞ 0 0 + 0 0 -∞ 0 0 -∞ -∞ 0 -∞ · x1
        [3(x1)]	=	0 -∞ -∞ + 0 0 -∞ 0 0 -∞ -∞ -∞ -∞ · x1
        [7(x1)]	=	-∞ 0 -∞ + 0 -∞ 0 0 -∞ 0 0 0 0 · x1
        [4(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
        [8(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
        [1(x1)]	=	0 -∞ 0 + 0 0 0 0 0 0 0 0 -∞ · x1

        the pair

        9#(5(9(x1)))

        →

        7#(x1)

        (36)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [7#(x1)]	=	1 + 1 · x1
        [2(x1)]	=	1 + 1 · x1
        [4#(x1)]	=	1
        [9#(x1)]	=	1 + 1 · x1
        [6(x1)]	=	0
        [0(x1)]	=	0
        [3(x1)]	=	0
        [5(x1)]	=	0
        [9(x1)]	=	0
        [7(x1)]	=	0
        [4(x1)]	=	0
        [8(x1)]	=	1
        [1(x1)]	=	1 · x1

        together with the usable rules

        0(3(x1))	→	5(3(x1))	(20)
        5(3(x1))	→	6(0(x1))	(6)
        6(9(x1))	→	9(x1)	(13)
        9(7(x1))	→	7(5(x1))	(10)
        7(2(x1))	→	4(x1)	(11)
        4(x1)	→	9(6(6(x1)))	(15)
        9(5(9(x1)))	→	5(7(x1))	(14)
        5(9(x1))	→	0(x1)	(4)
        5(2(6(x1)))	→	6(2(4(x1)))	(9)
        6(2(x1))	→	7(7(x1))	(17)
        7(0(x1))	→	9(3(x1))	(12)
        9(x1)	→	6(7(x1))	(16)
        6(6(x1))	→	3(x1)	(19)
        4(x1)	→	5(2(3(x1)))	(5)
        4(7(x1))	→	1(3(x1))	(8)

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

        7#(2(x1))

        →

        4#(x1)

        (33)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  5#(3(x1))	→	0#(x1)	(26)
  0#(3(x1))	→	5#(3(x1))	(46)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [3(x1)]	=	1 · x1
  [0#(x1)]	=	1 · x1
  [5#(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.2.1 Size-Change Termination

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

  0#(3(x1))	→	5#(3(x1))	(46)
  1	≥	1
  5#(3(x1))	→	0#(x1)	(26)
  1	>	1

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