Certification Problem

Input (TPDB TRS_Standard/MNZ_10/nvsr)

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

• The 1^st component contains the pair

  h#(f(x),g(x))	→	f#(s(x))	(22)
  f#(g(x))	→	g#(g(f(x)))	(16)
  g#(x)	→	h#(x,x)	(13)
  h#(f(x),g(x))	→	s#(x)	(23)
  s#(s(0))	→	f#(s(0))	(25)
  f#(g(x))	→	g#(f(x))	(17)
  g#(s(x))	→	s#(s(g(x)))	(19)
  s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
  f#(g(x))	→	f#(x)	(18)
  f#(s(s(0)))	→	s#(s(s(s(s(0)))))	(27)
  f#(s(s(0)))	→	s#(s(s(s(0))))	(28)
  f#(s(s(0)))	→	s#(s(s(0)))	(29)
  f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
  f#(s(s(x)))	→	f#(x)	(31)
  f#(s(s(x)))	→	g#(h(x,x))	(32)
  g#(s(x))	→	s#(g(x))	(20)
  g#(s(x))	→	g#(x)	(21)
  f#(s(s(x)))	→	h#(x,x)	(33)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [f#(x1)]	=	2 + 2 · x1
  [g#(x1)]	=	2 + x1
  [h#(x1, x2)]	=	2 + x1
  [s#(x1)]	=	2
  [s(x1)]	=	x1
  [h(x1, x2)]	=	x1
  [0]	=	0
  [f(x1)]	=	2 · x1
  [g(x1)]	=	2 + x1

  the pairs

  f#(g(x))	→	g#(g(f(x)))	(16)
  f#(g(x))	→	g#(f(x))	(17)
  f#(g(x))	→	f#(x)	(18)

  could be deleted.

  1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [f#(x1)]	=	1 + 2 · x1
  [g#(x1)]	=	1 + 2 · x1
  [h#(x1, x2)]	=	-1 + 2 · x2
  [s#(x1)]	=	1
  [s(x1)]	=	x1
  [h(x1, x2)]	=	x1
  [0]	=	0
  [f(x1)]	=	2 · x1
  [g(x1)]	=	1 + x1

  the pairs

  g#(x)	→	h#(x,x)	(13)
  f#(s(s(x)))	→	h#(x,x)	(33)

  could be deleted.

  1.1.1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  s#(s(0))	→	f#(h(0,0))	(34)
  s#(s(0))	→	f#(f(0))	(35)

  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(s(0)))	→	s#(s(s(s(s(0)))))	(27)
    s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
    f#(s(s(0)))	→	s#(s(s(s(0))))	(28)
    f#(s(s(0)))	→	s#(s(s(0)))	(29)
    f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
    h#(f(x),g(x))	→	f#(s(x))	(22)
    f#(s(s(x)))	→	f#(x)	(31)
    f#(s(s(x)))	→	g#(h(x,x))	(32)
    g#(s(x))	→	s#(s(g(x)))	(19)
    g#(s(x))	→	s#(g(x))	(20)
    g#(s(x))	→	g#(x)	(21)
    h#(f(x),g(x))	→	s#(x)	(23)

    1.1.1.1.1.1.1 Narrowing Processor

    We consider all narrowings of the pair below position 1 to get the following set of pairs

    f#(s(s(0)))	→	s#(h(s(s(s(0))),0))	(36)
    f#(s(s(0)))	→	s#(h(0,s(s(s(0)))))	(37)
    f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
    f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
    f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
    f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
    f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
    f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
    f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)

    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(s(0)))	→	s#(s(s(s(0))))	(28)
      s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
      f#(s(s(0)))	→	s#(s(s(0)))	(29)
      f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
      h#(f(x),g(x))	→	f#(s(x))	(22)
      f#(s(s(x)))	→	f#(x)	(31)
      f#(s(s(x)))	→	g#(h(x,x))	(32)
      g#(s(x))	→	s#(s(g(x)))	(19)
      g#(s(x))	→	s#(g(x))	(20)
      g#(s(x))	→	g#(x)	(21)
      f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
      f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
      f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
      f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
      f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
      f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
      f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)
      h#(f(x),g(x))	→	s#(x)	(23)

      1.1.1.1.1.1.1.1.1 Narrowing Processor

      We consider all narrowings of the pair below position 1 to get the following set of pairs

      f#(s(s(0)))	→	s#(h(s(s(0)),0))	(45)
      f#(s(s(0)))	→	s#(h(0,s(s(0))))	(46)
      f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
      f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)
      f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
      f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)
      f#(s(s(0)))	→	s#(s(s(f(0))))	(51)

      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(s(0)))	→	s#(s(s(0)))	(29)
        s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
        f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
        h#(f(x),g(x))	→	f#(s(x))	(22)
        f#(s(s(x)))	→	f#(x)	(31)
        f#(s(s(x)))	→	g#(h(x,x))	(32)
        g#(s(x))	→	s#(s(g(x)))	(19)
        g#(s(x))	→	s#(g(x))	(20)
        g#(s(x))	→	g#(x)	(21)
        f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
        f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
        f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
        f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
        f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
        f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
        f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)
        f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
        f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)
        f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
        f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)
        f#(s(s(0)))	→	s#(s(s(f(0))))	(51)
        h#(f(x),g(x))	→	s#(x)	(23)

        1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

        We consider all narrowings of the pair below position 1 to get the following set of pairs

        f#(s(s(0)))	→	s#(h(s(0),0))	(52)
        f#(s(s(0)))	→	s#(h(0,s(0)))	(53)
        f#(s(s(0)))	→	s#(f(s(0)))	(54)
        f#(s(s(0)))	→	s#(s(h(0,0)))	(55)
        f#(s(s(0)))	→	s#(s(f(0)))	(56)

        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(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
          h#(f(x),g(x))	→	f#(s(x))	(22)
          f#(s(s(x)))	→	f#(x)	(31)
          f#(s(s(x)))	→	g#(h(x,x))	(32)
          g#(s(x))	→	s#(s(g(x)))	(19)
          s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
          f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
          f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
          f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
          f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
          f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
          f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
          f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)
          f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
          f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)
          f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
          f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)
          f#(s(s(0)))	→	s#(s(s(f(0))))	(51)
          f#(s(s(0)))	→	s#(f(s(0)))	(54)
          f#(s(s(0)))	→	s#(s(h(0,0)))	(55)
          f#(s(s(0)))	→	s#(s(f(0)))	(56)
          g#(s(x))	→	s#(g(x))	(20)
          g#(s(x))	→	g#(x)	(21)
          h#(f(x),g(x))	→	s#(x)	(23)

          1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

          We consider all narrowings of the pair below position 1 to get the following set of pairs

          g#(s(y0))	→	s#(h(g(y0),0))	(57)
          g#(s(y0))	→	s#(h(0,g(y0)))	(58)
          g#(s(x0))	→	s#(s(h(x0,x0)))	(59)
          g#(s(s(x0)))	→	s#(s(s(s(g(x0)))))	(60)

          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

            h#(f(x),g(x))	→	f#(s(x))	(22)
            f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
            h#(f(x),g(x))	→	s#(x)	(23)
            s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
            f#(s(s(x)))	→	f#(x)	(31)
            f#(s(s(x)))	→	g#(h(x,x))	(32)
            g#(s(x))	→	s#(g(x))	(20)
            g#(s(x))	→	g#(x)	(21)
            g#(s(x0))	→	s#(s(h(x0,x0)))	(59)
            g#(s(s(x0)))	→	s#(s(s(s(g(x0)))))	(60)
            f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
            f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
            f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
            f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
            f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
            f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
            f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)
            f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
            f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)
            f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
            f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)
            f#(s(s(0)))	→	s#(s(s(f(0))))	(51)
            f#(s(s(0)))	→	s#(f(s(0)))	(54)
            f#(s(s(0)))	→	s#(s(h(0,0)))	(55)
            f#(s(s(0)))	→	s#(s(f(0)))	(56)

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

            We consider all narrowings of the pair below position 1 to get the following set of pairs

            g#(s(x0))	→	s#(h(x0,x0))	(61)
            g#(s(s(x0)))	→	s#(s(s(g(x0))))	(62)

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

            [h#(x1, x2)]	=	0 -∞ -∞ + 0 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
            [f(x1)]	=	-∞ 0 -∞ + 0 0 0 0 0 0 -∞ -∞ 0 · x1
            [g(x1)]	=	0 -∞ 0 + 0 0 0 0 0 0 0 0 0 · x1
            [f#(x1)]	=	0 -∞ -∞ + 0 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 -∞ -∞ + 0 0 0 0 0 0 -∞ -∞ 0 · x1
            [h(x1, x2)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ 0 -∞ -∞ 0 · x1 + 0 -∞ 0 -∞ -∞ 0 -∞ -∞ -∞ · x2
            [s#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [0]	=	0 -∞ -∞
            [g#(x1)]	=	0 -∞ -∞ + 0 1 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1

            the pairs

            g#(s(s(x0)))	→	s#(s(s(s(g(x0)))))	(60)
            g#(s(s(x0)))	→	s#(s(s(g(x0))))	(62)

            could be deleted.

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

            [h#(x1, x2)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x2
            [f(x1)]	=	0 -∞ 1 + 0 0 -∞ -∞ 0 0 0 0 0 · x1
            [g(x1)]	=	0 1 0 + 0 0 0 0 -∞ 0 0 0 0 · x1
            [f#(x1)]	=	0 -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 -∞ 1 + 0 0 -∞ -∞ -∞ 0 0 -∞ 0 · x1
            [h(x1, x2)]	=	0 -∞ 0 + 0 0 -∞ -∞ -∞ 0 0 -∞ 0 · x1 + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ 0 · x2
            [s#(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [0]	=	0 -∞ -∞
            [g#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1

            the pairs

            g#(s(x0))	→	s#(s(h(x0,x0)))	(59)
            g#(s(x0))	→	s#(h(x0,x0))	(61)

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

            • The 1^st component contains the pair

              f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
              h#(f(x),g(x))	→	f#(s(x))	(22)
              f#(s(s(x)))	→	f#(x)	(31)
              f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
              s#(s(s(s(s(s(s(0)))))))	→	f#(s(s(0)))	(26)
              f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
              f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
              f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
              f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(42)
              f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
              f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(44)
              f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
              f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)
              f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
              f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)
              f#(s(s(0)))	→	s#(s(s(f(0))))	(51)
              f#(s(s(0)))	→	s#(f(s(0)))	(54)
              f#(s(s(0)))	→	s#(s(h(0,0)))	(55)
              f#(s(s(0)))	→	s#(s(f(0)))	(56)
              h#(f(x),g(x))	→	s#(x)	(23)

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

              [f#(x1)]	=	0 -∞ -∞ + 0 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + -∞ -∞ -∞ 0 -∞ 0 -∞ 0 0 · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	-∞ 0 0 + 0 -∞ -∞ 0 0 0 0 0 0 · x1
              [g(x1)]	=	0 -∞ 0 + 0 0 0 -∞ 0 0 0 0 0 · x1
              [h(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x1 + -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x2
              [0]	=	0 0 -∞
              [s#(x1)]	=	0 -∞ -∞ + 0 -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1

              the pair

              f#(s(s(0)))

              →

              s#(s(h(0,0)))

              (55)

              could be deleted.

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

              [f#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + 0 0 0 0 0 0 -∞ -∞ 0 · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 0 -∞ + 0 0 1 0 0 1 -∞ -∞ 1 · x1
              [g(x1)]	=	0 0 0 + -∞ 0 0 -∞ 0 0 0 0 0 · x1
              [h(x1, x2)]	=	0 0 -∞ + -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ 0 · x1 + -∞ -∞ 0 -∞ 0 0 -∞ -∞ -∞ · x2
              [0]	=	1 0 -∞
              [s#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1

              the pairs

              f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(38)
              f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
              f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
              f#(s(s(0)))	→	s#(s(h(s(0),0)))	(47)
              f#(s(s(0)))	→	s#(s(s(h(0,0))))	(50)

              could be deleted.

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

              [f#(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 0 + 0 -∞ -∞ -∞ -∞ 0 0 0 0 · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 0 0 + 0 -∞ -∞ 0 -∞ 0 0 0 0 · x1
              [g(x1)]	=	0 0 0 + 0 0 0 0 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 0 0 + 0 -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x1 + -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 1 0

              the pairs

              f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(39)
              f#(s(s(0)))	→	s#(s(h(0,s(0))))	(48)

              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 Reduction Pair Processor

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

              [f#(x1)]	=	0 -∞ -∞ + -∞ -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + -∞ 0 0 0 0 0 -∞ 0 -∞ · x1
              [h#(x1, x2)]	=	1 -∞ -∞ + 0 0 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ 0 -∞ 0 0 · x1
              [g(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
              [h(x1, x2)]	=	0 0 -∞ + -∞ 0 0 0 0 0 -∞ 0 -∞ · x1 + -∞ 0 -∞ 0 0 0 -∞ 0 -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + -∞ -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 -∞ -∞

              the pairs

              f#(s(s(0)))	→	s#(s(f(s(0))))	(49)
              f#(s(s(0)))	→	s#(s(f(0)))	(56)

              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.1 Reduction Pair Processor

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

              [f#(x1)]	=	1 -∞ -∞ + -∞ -∞ 2 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + -∞ -∞ 2 -∞ 0 0 -∞ -∞ 0 · x1
              [h#(x1, x2)]	=	1 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 0 -∞ + -∞ -∞ 2 -∞ 0 -∞ -∞ -∞ 0 · x1
              [g(x1)]	=	0 0 0 + 0 2 2 -∞ 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ 2 -∞ -∞ 0 -∞ -∞ 0 · x1 + -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + -∞ 1 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 -∞ -∞

              the pair

              h#(f(x),g(x))

              →

              s#(x)

              (23)

              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.1.1 Reduction Pair Processor

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

              [f#(x1)]	=	1 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + -∞ 0 -∞ 0 0 0 -∞ 0 -∞ · x1
              [h#(x1, x2)]	=	1 -∞ -∞ + -∞ 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ 0 -∞ 0 -∞ · x1
              [g(x1)]	=	0 0 0 + 0 0 0 0 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 0 -∞ + -∞ 0 -∞ 0 0 0 -∞ 0 -∞ · x1 + -∞ 0 -∞ 0 0 0 -∞ 0 -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + -∞ 1 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 -∞ 0

              the pair

              f#(s(s(0)))

              →

              s#(f(s(0)))

              (54)

              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.1.1.1 Reduction Pair Processor

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

              [f#(x1)]	=	1 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + -∞ -∞ 1 -∞ 0 0 -∞ 0 -∞ · x1
              [h#(x1, x2)]	=	1 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 -∞ -∞ + 0 -∞ 1 -∞ 0 0 -∞ 0 0 · x1
              [g(x1)]	=	0 0 0 + 0 1 1 -∞ 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 0 -∞ + -∞ -∞ 0 -∞ 0 0 -∞ 0 -∞ · x1 + -∞ -∞ 1 -∞ -∞ -∞ -∞ 0 -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 -∞ -∞

              the pair

              f#(s(s(0)))

              →

              s#(s(s(f(0))))

              (51)

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

              [f#(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 0 -∞ + 0 -∞ -∞ 0 0 0 0 0 0 · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 0 0 + 0 -∞ -∞ 0 -∞ 0 0 0 0 · x1
              [g(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 0 0 0 0 0 · x1
              [h(x1, x2)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ 0 -∞ -∞ 0 · x1 + 0 -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ · x2
              [s#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 1 -∞

              the pair

              f#(s(s(0)))

              →

              s#(s(s(h(0,s(0)))))

              (41)

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

              [f#(x1)]	=	0 -∞ -∞ + -∞ 0 2 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ 0 0 -∞ 0 0 · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + -∞ 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ 0 2 -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 -∞ -∞ + 0 -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x1
              [g(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x1 + -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 · x2
              [s#(x1)]	=	0 -∞ -∞ + 0 -∞ 2 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 0 -∞

              the pair

              f#(s(s(0)))

              →

              s#(s(s(s(f(0)))))

              (44)

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

              [f#(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [s(x1)]	=	0 -∞ 0 + -∞ 1 -∞ -∞ 0 0 -∞ 0 -∞ · x1
              [h#(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
              [f(x1)]	=	0 -∞ -∞ + -∞ 1 -∞ -∞ 0 -∞ -∞ 0 -∞ · x1
              [g(x1)]	=	0 -∞ -∞ + -∞ 1 -∞ -∞ 0 0 -∞ 0 0 · x1
              [h(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ 0 -∞ -∞ 0 -∞ · x1 + -∞ 1 -∞ -∞ 0 0 -∞ 0 -∞ · x2
              [s#(x1)]	=	-∞ -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
              [0]	=	0 -∞ -∞

              the pair

              s#(s(s(s(s(s(s(0)))))))

              →

              f#(s(s(0)))

              (26)

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

                h#(f(x),g(x))	→	f#(s(x))	(22)
                f#(s(s(x)))	→	h#(f(x),g(h(x,x)))	(30)
                f#(s(s(x)))	→	f#(x)	(31)

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

                [h#(x1, x2)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
                [f(x1)]	=	1 -∞ 1 + -∞ 1 -∞ -∞ 0 -∞ -∞ 1 -∞ · x1
                [g(x1)]	=	0 1 2 + 0 1 0 -∞ 0 -∞ -∞ 0 0 · x1
                [f#(x1)]	=	0 -∞ -∞ + -∞ 1 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
                [s(x1)]	=	1 -∞ 0 + -∞ 0 -∞ -∞ -∞ -∞ 0 1 0 · x1
                [h(x1, x2)]	=	0 -∞ 0 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1 + -∞ 0 -∞ -∞ -∞ -∞ -∞ 0 -∞ · x2
                [0]	=	0 -∞ 1

                the pair

                f#(s(s(x)))

                →

                h#(f(x),g(h(x,x)))

                (30)

                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.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(s(x)))

                  →

                  f#(x)

                  (31)

                  1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

                  Using the linear polynomial interpretation over the naturals

                  [s(x1)]	=	1 · x1
                  [f#(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.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.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.

                  f#(s(s(x)))	→	f#(x)	(31)
                  1	>	1

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

            • The 2^nd component contains the pair

              g#(s(x))

              →

              g#(x)

              (21)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

              Using the linear polynomial interpretation over the naturals

              [s(x1)]	=	1 · x1
              [g#(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.1.1.1.1.1.1.1.1.1.1.1.1.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.

              g#(s(x))	→	g#(x)	(21)
              1	>	1

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