Certification Problem

Input (TPDB TRS_Standard/MNZ_10/0)

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

  s#(s(s(0)))	→	f#(s(0))	(14)
  f#(s(s(0)))	→	s#(s(s(s(s(s(0))))))	(16)
  s#(s(s(s(s(s(s(s(0))))))))	→	f#(s(s(0)))	(15)
  f#(s(s(0)))	→	s#(s(s(s(s(0)))))	(17)
  f#(s(s(0)))	→	s#(s(s(s(0))))	(18)
  f#(s(s(0)))	→	s#(s(s(0)))	(19)
  f#(g(x))	→	g#(g(f(x)))	(23)
  g#(x)	→	h#(x,x)	(20)
  h#(f(x),g(x))	→	f#(s(x))	(29)
  f#(g(x))	→	g#(f(x))	(24)
  g#(s(x))	→	s#(s(g(x)))	(26)
  g#(s(x))	→	s#(g(x))	(27)
  g#(s(x))	→	g#(x)	(28)
  f#(g(x))	→	f#(x)	(25)
  h#(f(x),g(x))	→	s#(x)	(30)

  1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  f#(g(x))	→	g#(g(f(x)))	(23)
  f#(g(x))	→	g#(f(x))	(24)
  f#(g(x))	→	f#(x)	(25)

  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)

    (28)

    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)	(28)
    1	>	1

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

  • The 2^nd component contains the pair

    f#(s(s(0)))	→	s#(s(s(s(s(s(0))))))	(16)
    s#(s(s(0)))	→	f#(s(0))	(14)
    f#(s(s(0)))	→	s#(s(s(s(s(0)))))	(17)
    s#(s(s(s(s(s(s(s(0))))))))	→	f#(s(s(0)))	(15)
    f#(s(s(0)))	→	s#(s(s(s(0))))	(18)
    f#(s(s(0)))	→	s#(s(s(0)))	(19)

    1.1.1.1.2 Reduction Pair Processor

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

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

    the pair

    s#(s(s(0)))

    →

    f#(s(0))

    (14)

    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

    f#(s(s(0)))	→	s#(h(s(s(s(s(0)))),0))	(31)
    f#(s(s(0)))	→	s#(h(0,s(s(s(s(0))))))	(32)
    f#(s(s(0)))	→	s#(s(h(s(s(s(0))),0)))	(33)
    f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
    f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(35)
    f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
    f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
    f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(38)
    f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
    f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
    f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)

    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(s(0))))))))	→	f#(s(s(0)))	(15)
      f#(s(s(0)))	→	s#(s(s(s(s(0)))))	(17)
      f#(s(s(0)))	→	s#(s(s(s(0))))	(18)
      f#(s(s(0)))	→	s#(s(s(0)))	(19)
      f#(s(s(0)))	→	s#(s(h(s(s(s(0))),0)))	(33)
      f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
      f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(35)
      f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
      f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
      f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(38)
      f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
      f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
      f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)

      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

      f#(s(s(0)))	→	s#(h(s(s(s(0))),0))	(42)
      f#(s(s(0)))	→	s#(h(0,s(s(s(0)))))	(43)
      f#(s(s(0)))	→	s#(s(f(s(0))))	(44)
      f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(45)
      f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(46)
      f#(s(s(0)))	→	s#(s(s(f(0))))	(47)
      f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(48)
      f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(49)
      f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(50)

      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

        f#(s(s(0)))	→	s#(s(s(s(0))))	(18)
        s#(s(s(s(s(s(s(s(0))))))))	→	f#(s(s(0)))	(15)
        f#(s(s(0)))	→	s#(s(s(0)))	(19)
        f#(s(s(0)))	→	s#(s(h(s(s(s(0))),0)))	(33)
        f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
        f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(35)
        f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
        f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
        f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(38)
        f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
        f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
        f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)
        f#(s(s(0)))	→	s#(s(f(s(0))))	(44)
        f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(45)
        f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(46)
        f#(s(s(0)))	→	s#(s(s(f(0))))	(47)
        f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(48)
        f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(49)
        f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(50)

        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

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

        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

          f#(s(s(0)))	→	s#(s(s(0)))	(19)
          s#(s(s(s(s(s(s(s(0))))))))	→	f#(s(s(0)))	(15)
          f#(s(s(0)))	→	s#(s(h(s(s(s(0))),0)))	(33)
          f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
          f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(35)
          f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
          f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
          f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(38)
          f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
          f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
          f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)
          f#(s(s(0)))	→	s#(s(f(s(0))))	(44)
          f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(45)
          f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(46)
          f#(s(s(0)))	→	s#(s(s(f(0))))	(47)
          f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(48)
          f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(49)
          f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(50)
          f#(s(s(0)))	→	s#(f(s(0)))	(51)
          f#(s(s(0)))	→	s#(s(f(0)))	(54)
          f#(s(s(0)))	→	s#(s(h(s(0),0)))	(55)
          f#(s(s(0)))	→	s#(s(h(0,s(0))))	(56)
          f#(s(s(0)))	→	s#(s(s(h(0,0))))	(57)

          1.1.1.1.2.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#(f(0))	(58)
          f#(s(s(0)))	→	s#(h(s(0),0))	(59)
          f#(s(s(0)))	→	s#(h(0,s(0)))	(60)
          f#(s(s(0)))	→	s#(s(h(0,0)))	(61)

          1.1.1.1.2.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(h(s(s(s(0))),0)))	(33)
            s#(s(s(s(s(s(s(s(0))))))))	→	f#(s(s(0)))	(15)
            f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
            f#(s(s(0)))	→	s#(s(s(f(s(0)))))	(35)
            f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
            f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
            f#(s(s(0)))	→	s#(s(s(s(f(0)))))	(38)
            f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
            f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
            f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)
            f#(s(s(0)))	→	s#(s(f(s(0))))	(44)
            f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(45)
            f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(46)
            f#(s(s(0)))	→	s#(s(s(f(0))))	(47)
            f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(48)
            f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(49)
            f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(50)
            f#(s(s(0)))	→	s#(f(s(0)))	(51)
            f#(s(s(0)))	→	s#(s(f(0)))	(54)
            f#(s(s(0)))	→	s#(s(h(s(0),0)))	(55)
            f#(s(s(0)))	→	s#(s(h(0,s(0))))	(56)
            f#(s(s(0)))	→	s#(s(s(h(0,0))))	(57)
            f#(s(s(0)))	→	s#(f(0))	(58)
            f#(s(s(0)))	→	s#(s(h(0,0)))	(61)

            1.1.1.1.2.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

            Using the linear polynomial interpretation over the naturals

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

            the pair

            f#(s(s(0)))

            →

            s#(f(0))

            (58)

            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

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

            the pair

            f#(s(s(0)))

            →

            s#(s(f(0)))

            (54)

            could be deleted.

            1.1.1.1.2.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 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 -∞ 0 + -∞ 0 -∞ -∞ 0 0 0 0 0 · x1
            [0]	=	0 -∞ -∞
            [s#(x1)]	=	0 -∞ -∞ + -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [h(x1, x2)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ 0 0 -∞ 0 0 · x1 + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x2
            [f(x1)]	=	-∞ -∞ 0 + 0 -∞ -∞ -∞ 0 -∞ 0 -∞ 0 · x1
            [g(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1

            the pairs

            f#(s(s(0)))	→	s#(s(h(0,s(s(s(0))))))	(34)
            f#(s(s(0)))	→	s#(s(h(0,s(s(0)))))	(46)
            f#(s(s(0)))	→	s#(f(s(0)))	(51)
            f#(s(s(0)))	→	s#(s(h(0,s(0))))	(56)
            f#(s(s(0)))	→	s#(s(h(0,0)))	(61)

            could be deleted.

            1.1.1.1.2.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 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 -∞ 0 + -∞ 0 0 -∞ -∞ -∞ 0 0 0 · x1
            [0]	=	1 -∞ 0
            [s#(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [h(x1, x2)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ 0 · x1 + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ 0 · x2
            [f(x1)]	=	1 -∞ 1 + -∞ 0 -∞ -∞ 1 -∞ -∞ -∞ -∞ · x1
            [g(x1)]	=	0 0 -∞ + -∞ -∞ 0 0 -∞ 0 -∞ -∞ 0 · x1

            the pairs

            f#(s(s(0)))	→	s#(s(s(s(s(h(0,0))))))	(41)
            f#(s(s(0)))	→	s#(s(s(s(h(0,0)))))	(50)
            f#(s(s(0)))	→	s#(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.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 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ 0 0 -∞ 0 0 · x1
            [0]	=	0 0 -∞
            [s#(x1)]	=	0 -∞ -∞ + -∞ -∞ 1 -∞ -∞ -∞ -∞ -∞ -∞ · 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 · x1

            the pairs

            f#(s(s(0)))	→	s#(s(s(h(0,s(s(0))))))	(37)
            f#(s(s(0)))	→	s#(s(s(s(h(0,s(0))))))	(40)
            f#(s(s(0)))	→	s#(s(s(h(0,s(0)))))	(49)

            could be deleted.

            1.1.1.1.2.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 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [s(x1)]	=	0 0 -∞ + -∞ 0 0 0 -∞ 0 -∞ -∞ 0 · x1
            [0]	=	1 -∞ -∞
            [s#(x1)]	=	0 -∞ -∞ + -∞ 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
            [h(x1, x2)]	=	0 0 -∞ + -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ 0 · 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

            the pairs

            f#(s(s(0)))	→	s#(s(h(s(s(s(0))),0)))	(33)
            f#(s(s(0)))	→	s#(s(s(h(s(s(0)),0))))	(36)
            f#(s(s(0)))	→	s#(s(s(s(h(s(0),0)))))	(39)
            f#(s(s(0)))	→	s#(s(f(s(0))))	(44)
            f#(s(s(0)))	→	s#(s(h(s(s(0)),0)))	(45)
            f#(s(s(0)))	→	s#(s(s(f(0))))	(47)
            f#(s(s(0)))	→	s#(s(s(h(s(0),0))))	(48)
            f#(s(s(0)))	→	s#(s(h(s(0),0)))	(55)

            could be deleted.

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

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

            the pair

            f#(s(s(0)))

            →

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

            (35)

            could be deleted.

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

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

            the pair

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

            →

            f#(s(s(0)))

            (15)

            could be deleted.

            1.1.1.1.2.1.1.1.1.1.1.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.1.1.1.1.1.1 P is empty

            There are no pairs anymore.