Certification Problem

Input (TPDB SRS_Standard/Waldmann_06_SRS/pi)

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

  5#(9(x1))

  →

  5#(x1)

  (14)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [9(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.1.1 Size-Change Termination

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

  5#(9(x1))	→	5#(x1)	(14)
  1	>	1

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

• The 2^nd component contains the pair

  8#(8(4(x1)))	→	9#(x1)	(27)
  9#(x1)	→	3#(2(3(x1)))	(18)
  3#(5(x1))	→	8#(9(7(x1)))	(15)
  3#(5(x1))	→	9#(7(x1))	(16)
  9#(x1)	→	2#(3(x1))	(19)
  2#(6(x1))	→	3#(x1)	(21)
  3#(5(x1))	→	7#(x1)	(17)
  7#(1(x1))	→	9#(x1)	(28)
  9#(x1)	→	3#(x1)	(20)
  3#(8(x1))	→	3#(2(7(x1)))	(22)
  3#(8(x1))	→	2#(7(x1))	(23)
  3#(8(x1))	→	7#(x1)	(24)
  3#(9(x1))	→	9#(3(x1))	(29)
  9#(x1)	→	2#(x1)	(26)
  3#(9(x1))	→	3#(x1)	(30)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  3(1(x1))	→	4(1(x1))	(1)
  3(5(x1))	→	8(9(7(x1)))	(3)
  3(8(x1))	→	3(2(7(x1)))	(7)
  3(9(x1))	→	9(3(x1))	(11)
  9(x1)	→	3(2(3(x1)))	(4)
  7(1(x1))	→	6(9(x1))	(10)
  7(5(x1))	→	1(0(x1))	(12)
  2(6(x1))	→	4(3(x1))	(6)
  9(x1)	→	5(0(2(x1)))	(8)
  8(4(x1))	→	6(x1)	(5)
  8(8(4(x1)))	→	1(9(x1))	(9)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.2.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  3(1(x1))	→	4(1(x1))	(1)
  3(5(x1))	→	8(9(7(x1)))	(3)
  3(9(x1))	→	9(3(x1))	(11)
  9(x1)	→	3(2(3(x1)))	(4)
  3(8(x1))	→	3(2(7(x1)))	(7)
  2(6(x1))	→	4(3(x1))	(6)
  9(x1)	→	5(0(2(x1)))	(8)
  8(8(4(x1)))	→	1(9(x1))	(9)
  8(4(x1))	→	6(x1)	(5)

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

  8#(8(4(x1)))

  →

  9#(x1)

  (27)

  could be deleted.

  1.1.2.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    3#(5(x1))	→	9#(7(x1))	(16)
    9#(x1)	→	3#(2(3(x1)))	(18)
    3#(5(x1))	→	7#(x1)	(17)
    7#(1(x1))	→	9#(x1)	(28)
    9#(x1)	→	2#(3(x1))	(19)
    2#(6(x1))	→	3#(x1)	(21)
    3#(8(x1))	→	3#(2(7(x1)))	(22)
    3#(8(x1))	→	2#(7(x1))	(23)
    3#(8(x1))	→	7#(x1)	(24)
    3#(9(x1))	→	9#(3(x1))	(29)
    9#(x1)	→	3#(x1)	(20)
    3#(9(x1))	→	3#(x1)	(30)
    9#(x1)	→	2#(x1)	(26)

    1.1.2.1.1.1 Reduction Pair Processor

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

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

    the pair

    7#(1(x1))

    →

    9#(x1)

    (28)

    could be deleted.

    1.1.2.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      9#(x1)	→	3#(2(3(x1)))	(18)
      3#(5(x1))	→	9#(7(x1))	(16)
      9#(x1)	→	2#(3(x1))	(19)
      2#(6(x1))	→	3#(x1)	(21)
      3#(8(x1))	→	3#(2(7(x1)))	(22)
      3#(8(x1))	→	2#(7(x1))	(23)
      3#(9(x1))	→	9#(3(x1))	(29)
      9#(x1)	→	3#(x1)	(20)
      3#(9(x1))	→	3#(x1)	(30)
      9#(x1)	→	2#(x1)	(26)

      1.1.2.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 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [3#(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [2(x1)]	=	0 -∞ -∞ + -∞ 0 1 -∞ 0 0 -∞ -∞ 0 · x1
      [3(x1)]	=	0 -∞ -∞ + 0 0 1 -∞ 0 0 -∞ -∞ 0 · x1
      [5(x1)]	=	0 -∞ 0 + 0 0 -∞ -∞ -∞ -∞ 1 0 1 · x1
      [7(x1)]	=	-∞ -∞ -∞ + 0 0 1 0 0 -∞ 0 -∞ -∞ · x1
      [2#(x1)]	=	0 -∞ -∞ + -∞ 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [6(x1)]	=	0 0 -∞ + 0 0 0 -∞ 0 0 0 0 0 · x1
      [8(x1)]	=	1 -∞ -∞ + 1 0 0 -∞ 0 -∞ 0 -∞ -∞ · x1
      [9(x1)]	=	0 -∞ 1 + 0 0 1 0 0 0 0 0 1 · x1
      [1(x1)]	=	1 0 0 + 0 0 1 -∞ -∞ -∞ -∞ 0 0 · x1
      [4(x1)]	=	-∞ 0 -∞ + 0 0 0 -∞ 0 0 -∞ 0 0 · x1
      [0(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ 0 -∞ -∞ -∞ -∞ · x1

      the pair

      2#(6(x1))

      →

      3#(x1)

      (21)

      could be deleted.

      1.1.2.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        3#(5(x1))	→	9#(7(x1))	(16)
        9#(x1)	→	3#(2(3(x1)))	(18)
        3#(8(x1))	→	3#(2(7(x1)))	(22)
        3#(9(x1))	→	9#(3(x1))	(29)
        9#(x1)	→	3#(x1)	(20)
        3#(9(x1))	→	3#(x1)	(30)

        1.1.2.1.1.1.1.1.1.1 Reduction Pair Processor

        Using the linear polynomial interpretation over the naturals

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

        the pairs

        3#(5(x1))	→	9#(7(x1))	(16)
        3#(9(x1))	→	9#(3(x1))	(29)
        3#(9(x1))	→	3#(x1)	(30)

        could be deleted.

        1.1.2.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

          3#(8(x1))

          →

          3#(2(7(x1)))

          (22)

          1.1.2.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the linear polynomial interpretation over the naturals

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

          together with the usable rule

          2(6(x1))

          →

          4(3(x1))

          (6)

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

          3#(8(x1))

          →

          3#(2(7(x1)))

          (22)

          could be deleted.

          1.1.2.1.1.1.1.1.1.1.1.1.1 P is empty

          There are no pairs anymore.