Certification Problem

Input (TPDB TRS_Standard/MNZ_10/1)

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

  f#(g(x))	→	g#(g(f(x)))	(19)
  g#(x)	→	h#(x,x)	(16)
  h#(f(x),g(x))	→	f#(s(x))	(25)
  f#(g(x))	→	g#(f(x))	(20)
  g#(s(x))	→	s#(s(g(x)))	(22)
  s#(s(0))	→	f#(s(0))	(15)
  f#(g(x))	→	f#(x)	(21)
  s#(s(0))	→	k#(s(0))	(28)
  k#(s(s(0)))	→	s#(s(s(s(s(0)))))	(30)
  s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
  k#(s(s(0)))	→	s#(s(s(s(0))))	(31)
  k#(s(s(0)))	→	s#(s(s(0)))	(32)
  g#(s(x))	→	s#(g(x))	(23)
  g#(s(x))	→	g#(x)	(24)
  h#(f(x),g(x))	→	s#(x)	(26)
  h#(k(x),g(x))	→	k#(s(x))	(33)
  h#(k(x),g(x))	→	s#(x)	(34)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  h#(f(x),g(x))	→	f#(s(x))	(25)
  s#(s(0))	→	f#(s(0))	(15)
  f#(g(x))	→	f#(x)	(21)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    g#(s(x))

    →

    g#(x)

    (24)

    1.1.1.1.1 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 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)	(24)
    1	>	1

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

  • The 2^nd component contains the pair

    k#(s(s(0)))	→	s#(s(s(s(s(0)))))	(30)
    s#(s(0))	→	k#(s(0))	(28)
    k#(s(s(0)))	→	s#(s(s(s(0))))	(31)
    s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
    k#(s(s(0)))	→	s#(s(s(0)))	(32)

    1.1.1.1.2 Reduction Pair Processor

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

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

    the pair

    s#(s(0))

    →

    k#(s(0))

    (28)

    could be deleted.

    1.1.1.1.2.1 Narrowing Processor

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

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

    1.1.1.1.2.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
      k#(s(s(0)))	→	s#(s(s(s(0))))	(31)
      k#(s(s(0)))	→	s#(s(s(0)))	(32)
      k#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(37)
      k#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(38)
      k#(s(s(0)))	→	s#(s(s(f(s(0)))))	(39)
      k#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
      k#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
      k#(s(s(0)))	→	s#(s(s(k(s(0)))))	(42)
      k#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
      k#(s(s(0)))	→	s#(s(s(s(k(0)))))	(44)

      1.1.1.1.2.1.1.1 Narrowing Processor

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

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

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

        k#(s(s(0)))	→	s#(s(s(0)))	(32)
        s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
        k#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(37)
        k#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(38)
        k#(s(s(0)))	→	s#(s(s(f(s(0)))))	(39)
        k#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
        k#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
        k#(s(s(0)))	→	s#(s(s(k(s(0)))))	(42)
        k#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
        k#(s(s(0)))	→	s#(s(s(s(k(0)))))	(44)
        k#(s(s(0)))	→	s#(s(f(s(0))))	(47)
        k#(s(s(0)))	→	s#(s(h(s(0),0)))	(48)
        k#(s(s(0)))	→	s#(s(h(0,s(0))))	(49)
        k#(s(s(0)))	→	s#(s(k(s(0))))	(50)
        k#(s(s(0)))	→	s#(s(s(h(0,0))))	(51)
        k#(s(s(0)))	→	s#(s(s(k(0))))	(52)

        1.1.1.1.2.1.1.1.1.1 Narrowing Processor

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

        k#(s(s(0)))	→	s#(f(s(0)))	(53)
        k#(s(s(0)))	→	s#(h(s(0),0))	(54)
        k#(s(s(0)))	→	s#(h(0,s(0)))	(55)
        k#(s(s(0)))	→	s#(k(s(0)))	(56)
        k#(s(s(0)))	→	s#(s(h(0,0)))	(57)
        k#(s(s(0)))	→	s#(s(k(0)))	(58)

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

          k#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(37)
          s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
          k#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(38)
          k#(s(s(0)))	→	s#(s(s(f(s(0)))))	(39)
          k#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
          k#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(41)
          k#(s(s(0)))	→	s#(s(s(k(s(0)))))	(42)
          k#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
          k#(s(s(0)))	→	s#(s(s(s(k(0)))))	(44)
          k#(s(s(0)))	→	s#(s(f(s(0))))	(47)
          k#(s(s(0)))	→	s#(s(h(s(0),0)))	(48)
          k#(s(s(0)))	→	s#(s(h(0,s(0))))	(49)
          k#(s(s(0)))	→	s#(s(k(s(0))))	(50)
          k#(s(s(0)))	→	s#(s(s(h(0,0))))	(51)
          k#(s(s(0)))	→	s#(s(s(k(0))))	(52)
          k#(s(s(0)))	→	s#(f(s(0)))	(53)
          k#(s(s(0)))	→	s#(k(s(0)))	(56)
          k#(s(s(0)))	→	s#(s(h(0,0)))	(57)
          k#(s(s(0)))	→	s#(s(k(0)))	(58)

          1.1.1.1.2.1.1.1.1.1.1.1 Reduction Pair Processor

          Using the linear polynomial interpretation over the naturals

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

          the pair

          k#(s(s(0)))

          →

          s#(f(s(0)))

          (53)

          could be deleted.

          1.1.1.1.2.1.1.1.1.1.1.1.1 Reduction Pair Processor

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

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

          the pair

          k#(s(s(0)))

          →

          s#(s(k(0)))

          (58)

          could be deleted.

          1.1.1.1.2.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

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

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

          the pair

          k#(s(s(0)))

          →

          s#(k(s(0)))

          (56)

          could be deleted.

          1.1.1.1.2.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

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

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

          the pairs

          k#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(37)
          s#(s(s(s(s(s(s(0)))))))	→	k#(s(s(0)))	(29)
          k#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(38)
          k#(s(s(0)))	→	s#(s(s(f(s(0)))))	(39)
          k#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(40)
          k#(s(s(0)))	→	s#(s(s(k(s(0)))))	(42)
          k#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(43)
          k#(s(s(0)))	→	s#(s(s(s(k(0)))))	(44)
          k#(s(s(0)))	→	s#(s(f(s(0))))	(47)
          k#(s(s(0)))	→	s#(s(h(s(0),0)))	(48)
          k#(s(s(0)))	→	s#(s(h(0,s(0))))	(49)
          k#(s(s(0)))	→	s#(s(k(s(0))))	(50)
          k#(s(s(0)))	→	s#(s(s(h(0,0))))	(51)
          k#(s(s(0)))	→	s#(s(s(k(0))))	(52)
          k#(s(s(0)))	→	s#(s(h(0,0)))	(57)

          could be deleted.

          1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1 Instantiation Processor

          We instantiate the pair to the following set of pairs

          There are no rules.

          1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

          There are no pairs anymore.