Certification Problem

Input (TPDB TRS_Standard/TCT_12/polycounter-5)

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#(s(x1),x2,x3,x4,x5)	→	f#(x1,x2,x3,x4,x5)	(11)
  f#(0,s(x2),x3,x4,x5)	→	f#(x2,x2,x3,x4,x5)	(10)
  f#(0,0,s(x3),x4,x5)	→	f#(x3,x3,x3,x4,x5)	(9)
  f#(0,0,0,s(x4),x5)	→	f#(x4,x4,x4,x4,x5)	(8)
  f#(0,0,0,0,s(x5))	→	f#(x5,x5,x5,x5,x5)	(7)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [f(x1,...,x5)]	=	0
  [0]	=	1
  [f#(x1,...,x5)]	=	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))

  →

  f#(x5,x5,x5,x5,x5)

  (7)

  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)	→	f#(x4,x4,x4,x4,x5)	(8)
    f#(s(x1),x2,x3,x4,x5)	→	f#(x1,x2,x3,x4,x5)	(11)
    f#(0,0,s(x3),x4,x5)	→	f#(x3,x3,x3,x4,x5)	(9)
    f#(0,s(x2),x3,x4,x5)	→	f#(x2,x2,x3,x4,x5)	(10)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [s(x1)]	=	x1 + 1
    [f(x1,...,x5)]	=	0
    [0]	=	1
    [f#(x1,...,x5)]	=	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)

    →

    f#(x4,x4,x4,x4,x5)

    (8)

    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#(s(x1),x2,x3,x4,x5)	→	f#(x1,x2,x3,x4,x5)	(11)
      f#(0,0,s(x3),x4,x5)	→	f#(x3,x3,x3,x4,x5)	(9)
      f#(0,s(x2),x3,x4,x5)	→	f#(x2,x2,x3,x4,x5)	(10)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [s(x1)]	=	x1 + 1
      [f(x1,...,x5)]	=	0
      [0]	=	1
      [f#(x1,...,x5)]	=	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)

      →

      f#(x3,x3,x3,x4,x5)

      (9)

      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#(s(x1),x2,x3,x4,x5)	→	f#(x1,x2,x3,x4,x5)	(11)
        f#(0,s(x2),x3,x4,x5)	→	f#(x2,x2,x3,x4,x5)	(10)

        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,...,x5)]	=	0
        [0]	=	1
        [f#(x1,...,x5)]	=	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)

        →

        f#(x2,x2,x3,x4,x5)

        (10)

        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#(s(x1),x2,x3,x4,x5)

          →

          f#(x1,x2,x3,x4,x5)

          (11)

          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,...,x5)]	=	0
          [0]	=	1
          [f#(x1,...,x5)]	=	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)

          →

          f#(x1,x2,x3,x4,x5)

          (11)

          could be deleted.

          1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 0 components.