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 NaTT @ 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)

  (13)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

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

  5#(9(x1))

  →

  5#(x1)

  (13)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

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

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [7(x1)]	=	1
  [1(x1)]	=	x1 + 1
  [4(x1)]	=	1
  [7#(x1)]	=	26289
  [5(x1)]	=	3
  [3(x1)]	=	x1 + 26287
  [8#(x1)]	=	x1 + 0
  [2#(x1)]	=	26289
  [9(x1)]	=	26288
  [8(x1)]	=	26290
  [9#(x1)]	=	26289
  [0(x1)]	=	x1 + 17678
  [3#(x1)]	=	26289
  [5#(x1)]	=	0
  [2(x1)]	=	1
  [6(x1)]	=	2

  together with the usable rules

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

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

  8#(8(4(x1)))	→	9#(x1)	(29)
  3#(5(x1))	→	8#(9(7(x1)))	(17)

  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

    9#(x1)	→	3#(x1)	(30)
    9#(x1)	→	2#(3(x1))	(23)
    9#(x1)	→	3#(2(3(x1)))	(24)
    9#(x1)	→	2#(x1)	(28)
    3#(5(x1))	→	7#(x1)	(15)
    3#(5(x1))	→	9#(7(x1))	(18)
    7#(1(x1))	→	9#(x1)	(21)
    3#(8(x1))	→	7#(x1)	(16)
    3#(8(x1))	→	2#(7(x1))	(27)
    3#(8(x1))	→	3#(2(7(x1)))	(20)
    3#(9(x1))	→	3#(x1)	(14)
    3#(9(x1))	→	9#(3(x1))	(22)
    2#(6(x1))	→	3#(x1)	(25)

    1.1.2.1.1 Reduction Pair Processor with Usable Rules

    Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

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

    together with the usable rules

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

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

    9#(x1)	→	3#(x1)	(30)
    9#(x1)	→	2#(3(x1))	(23)
    9#(x1)	→	3#(2(3(x1)))	(24)
    9#(x1)	→	2#(x1)	(28)
    3#(5(x1))	→	7#(x1)	(15)
    3#(5(x1))	→	9#(7(x1))	(18)
    7#(1(x1))	→	9#(x1)	(21)
    3#(8(x1))	→	7#(x1)	(16)
    3#(9(x1))	→	3#(x1)	(14)
    3#(9(x1))	→	9#(3(x1))	(22)

    could be deleted.

    1.1.2.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      3#(8(x1))	→	2#(7(x1))	(27)
      3#(8(x1))	→	3#(2(7(x1)))	(20)
      2#(6(x1))	→	3#(x1)	(25)

      1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

      [7(x1)]	=	0 0 1 1 · x1 + 2 58719
      [1(x1)]	=	1 0 0 0 · x1 + 1 535958
      [4(x1)]	=	1 0 1 0 · x1 + 38987 0
      [7#(x1)]	=	0 2
      [5(x1)]	=	1 0 1 1 · x1 + 379527 97712
      [3(x1)]	=	1 0 1 0 · x1 + 176164 5892
      [8#(x1)]	=	0 0
      [2#(x1)]	=	0 1 1 0 · x1 + 0 0
      [9(x1)]	=	1 0 1 0 · x1 + 379528 117438
      [8(x1)]	=	1 1 0 1 · x1 + 58721 267979
      [9#(x1)]	=	24654 2
      [0(x1)]	=	1 19725
      [3#(x1)]	=	1 0 0 0 · x1 + 215150 2
      [5#(x1)]	=	0 0
      [2(x1)]	=	0 1 0 1 · x1 + 1 1
      [6(x1)]	=	0 0 1 0 · x1 + 2 215150

      together with the usable rules

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

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

      3#(8(x1))	→	2#(7(x1))	(27)
      3#(8(x1))	→	3#(2(7(x1)))	(20)

      could be deleted.

      1.1.2.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.