Certification Problem

Input (TPDB TRS_Standard/TCT_12/polycounter-10)

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 1 component.

• The 1^st component contains the pair

  f#(0,0,0,0,0,0,s(x7),x8,x9,x10)	→	f#(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10)	(21)
  f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
  f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)
  f#(0,0,0,0,0,0,0,0,s(x9),x10)	→	f#(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10)	(18)
  f#(0,0,0,0,0,0,0,s(x8),x9,x10)	→	f#(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10)	(14)
  f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
  f#(0,0,0,0,0,0,0,0,0,s(x10))	→	f#(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10)	(17)
  f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
  f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
  f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)	→	f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)	(12)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [f(x1,...,x10)]	=	0
  [0]	=	1
  [f#(x1,...,x10)]	=	x10 + 0

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

  f#(0,0,0,0,0,0,0,0,0,s(x10))

  →

  f#(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10)

  (17)

  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

    f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
    f#(0,0,0,0,0,0,0,s(x8),x9,x10)	→	f#(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10)	(14)
    f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
    f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
    f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
    f#(0,0,0,0,0,0,s(x7),x8,x9,x10)	→	f#(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10)	(21)
    f#(0,0,0,0,0,0,0,0,s(x9),x10)	→	f#(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10)	(18)
    f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)	→	f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)	(12)
    f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [s(x1)]	=	x1 + 1
    [f(x1,...,x10)]	=	0
    [0]	=	1
    [f#(x1,...,x10)]	=	x9 + 0

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

    f#(0,0,0,0,0,0,0,0,s(x9),x10)

    →

    f#(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10)

    (18)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
      f#(0,0,0,0,0,0,0,s(x8),x9,x10)	→	f#(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10)	(14)
      f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
      f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
      f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
      f#(0,0,0,0,0,0,s(x7),x8,x9,x10)	→	f#(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10)	(21)
      f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)	→	f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)	(12)
      f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [s(x1)]	=	x1 + 1
      [f(x1,...,x10)]	=	0
      [0]	=	1
      [f#(x1,...,x10)]	=	x8 + 0

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

      f#(0,0,0,0,0,0,0,s(x8),x9,x10)

      →

      f#(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10)

      (14)

      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

        f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
        f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
        f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
        f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
        f#(0,0,0,0,0,0,s(x7),x8,x9,x10)	→	f#(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10)	(21)
        f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)	→	f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)	(12)
        f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [s(x1)]	=	x1 + 1
        [f(x1,...,x10)]	=	0
        [0]	=	0
        [f#(x1,...,x10)]	=	x7 + 0

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

        f#(0,0,0,0,0,0,s(x7),x8,x9,x10)

        →

        f#(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10)

        (21)

        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

          f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
          f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
          f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
          f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
          f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)	→	f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)	(12)
          f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

          1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the Max-polynomial interpretation

          [s(x1)]	=	x1 + 1
          [f(x1,...,x10)]	=	0
          [0]	=	1
          [f#(x1,...,x10)]	=	x6 + 0

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

          f#(0,0,0,0,0,s(x6),x7,x8,x9,x10)

          →

          f#(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10)

          (12)

          could be deleted.

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

            f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
            f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
            f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
            f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)	→	f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)	(13)
            f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

            1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

            Using the Max-polynomial interpretation

            [s(x1)]	=	x1 + 1
            [f(x1,...,x10)]	=	0
            [0]	=	1
            [f#(x1,...,x10)]	=	x5 + 0

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

            f#(0,0,0,0,s(x5),x6,x7,x8,x9,x10)

            →

            f#(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10)

            (13)

            could be deleted.

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

              f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)	→	f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)	(16)
              f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
              f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
              f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

              Using the Max-polynomial interpretation

              [s(x1)]	=	x1 + 2
              [f(x1,...,x10)]	=	0
              [0]	=	1
              [f#(x1,...,x10)]	=	x4 + 0

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

              f#(0,0,0,s(x4),x5,x6,x7,x8,x9,x10)

              →

              f#(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10)

              (16)

              could be deleted.

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

                f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
                f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)	→	f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)	(15)
                f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                Using the Max-polynomial interpretation

                [s(x1)]	=	x1 + 1
                [f(x1,...,x10)]	=	0
                [0]	=	1
                [f#(x1,...,x10)]	=	x3 + 0

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

                f#(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10)

                →

                f#(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10)

                (15)

                could be deleted.

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

                  f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(20)
                  f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)	→	f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)	(19)

                  1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                  Using the Max-polynomial interpretation

                  [s(x1)]	=	x1 + 1
                  [f(x1,...,x10)]	=	0
                  [0]	=	1
                  [f#(x1,...,x10)]	=	x2 + 0

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

                  f#(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10)

                  →

                  f#(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10)

                  (19)

                  could be deleted.

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

                    f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)

                    →

                    f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)

                    (20)

                    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                    Using the Max-polynomial interpretation

                    [s(x1)]	=	x1 + 1
                    [f(x1,...,x10)]	=	0
                    [0]	=	1
                    [f#(x1,...,x10)]	=	x1 + 0

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

                    f#(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10)

                    →

                    f#(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)

                    (20)

                    could be deleted.

                    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

                    The dependency pairs are split into 0 components.