Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/2-matchbox)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

{c(☐), a(☐), b(☐)}

1.1 Semantic Labeling

Root-labeling is applied.

1.1.1 Rule Removal

1.1.1.1 Dependency Pair Transformation

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(39)
  bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(ba(x1)))))))	(40)
  bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(ba(x1))))))	(41)
  bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(ba(x1)))))	(42)
  bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(ba(x1))))	(43)
  bb#(bb(ba(aa(x1))))	→	bb#(bb(ba(x1)))	(44)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(31)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(46)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bc(x1)))))))	(47)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bc(x1))))))	(48)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bc(x1)))))	(49)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bc(x1))))	(50)
  bb#(bb(ba(ac(x1))))	→	bb#(bb(bc(x1)))	(51)
  bb#(bb(ba(ac(x1))))	→	bb#(bc(x1))	(52)
  bb#(bb(ba(ac(x1))))	→	bc#(x1)	(53)
  bc#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(68)
  ab#(bb(bc(cc(ca(x1)))))	→	ac#(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(75)
  ac#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(61)
  ab#(bb(bc(cc(ca(x1)))))	→	cc#(cc(ca(aa(aa(aa(aa(x1)))))))	(76)
  cc#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(54)
  ab#(bb(bc(cc(cc(x1)))))	→	ac#(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(78)
  ac#(cc(ca(x1)))	→	bb#(bb(ba(x1)))	(62)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(x1)))))))	(32)
  bb#(bb(bc(cc(ca(x1)))))	→	bc#(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(82)
  bc#(cc(ca(x1)))	→	bb#(bb(ba(x1)))	(69)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(x1))))))	(33)
  bb#(bb(bc(cc(ca(x1)))))	→	cc#(cc(ca(aa(aa(aa(aa(x1)))))))	(83)
  cc#(cc(ca(x1)))	→	bb#(bb(ba(x1)))	(55)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(x1)))))	(34)
  bb#(bb(bc(cc(cc(x1)))))	→	bc#(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(85)
  bc#(cc(cc(x1)))	→	ab#(bb(bb(bc(x1))))	(71)
  ab#(bb(bc(cc(cc(x1)))))	→	cc#(cc(ca(aa(aa(aa(ac(x1)))))))	(79)
  ab#(bb(bc(cc(cc(x1)))))	→	ac#(x1)	(81)
  ac#(cc(cc(x1)))	→	ab#(bb(bb(bc(x1))))	(64)
  ac#(cc(cc(x1)))	→	bb#(bb(bc(x1)))	(65)
  bb#(bb(bc(cc(cc(x1)))))	→	cc#(cc(ca(aa(aa(aa(ac(x1)))))))	(86)
  bb#(bb(bc(cc(cc(x1)))))	→	ac#(x1)	(88)
  ac#(cc(cc(x1)))	→	bb#(bc(x1))	(66)
  ac#(cc(cc(x1)))	→	bc#(x1)	(67)
  bc#(cc(cc(x1)))	→	bb#(bb(bc(x1)))	(72)
  bc#(cc(cc(x1)))	→	bb#(bc(x1))	(73)
  bc#(cc(cc(x1)))	→	bc#(x1)	(74)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(x1))))	(35)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(x1)))	(36)
  bb#(bb(ba(ab(x1))))	→	bb#(bb(x1))	(37)
  bb#(bb(ba(ab(x1))))	→	bb#(x1)	(38)

  1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [bb(x1)]	=	1 · x1
  [ba(x1)]	=	1 · x1
  [aa(x1)]	=	1 · x1
  [ab(x1)]	=	1 · x1
  [ac(x1)]	=	1 · x1
  [bc(x1)]	=	1 · x1
  [cc(x1)]	=	1 · x1
  [ca(x1)]	=	1 · x1
  [bb#(x1)]	=	1 · x1
  [bc#(x1)]	=	1 · x1
  [ab#(x1)]	=	1 · x1
  [ac#(x1)]	=	1 · x1
  [cc#(x1)]	=	1 · x1

  together with the usable rules

  bb(bb(ba(aa(x1))))	→	bb(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(11)
  bb(bb(ba(ab(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(10)
  bb(bb(ba(ac(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(12)
  bb(bb(bc(cc(ca(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(29)
  bb(bb(bc(cc(cc(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(30)
  ac(cc(ca(x1)))	→	aa(aa(aa(ab(bb(bb(ba(x1)))))))	(17)
  ac(cc(cc(x1)))	→	aa(aa(aa(ab(bb(bb(bc(x1)))))))	(18)
  cc(cc(ca(x1)))	→	ca(aa(aa(ab(bb(bb(ba(x1)))))))	(14)
  bc(cc(ca(x1)))	→	ba(aa(aa(ab(bb(bb(ba(x1)))))))	(20)
  bc(cc(cc(x1)))	→	ba(aa(aa(ab(bb(bb(bc(x1)))))))	(21)
  ab(bb(bc(cc(ca(x1)))))	→	ac(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(26)
  ab(bb(bc(cc(cc(x1)))))	→	ac(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(27)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  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

  [bb#(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [bb(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ 0 0 -∞ 0 · x1
  [ba(x1)]	=	-∞ 0 -∞ + 0 -∞ -∞ 0 0 0 0 0 -∞ · x1
  [aa(x1)]	=	-∞ -∞ 0 + 0 -∞ -∞ 0 0 -∞ 0 0 0 · x1
  [ab(x1)]	=	-∞ 0 0 + 0 0 -∞ 1 0 0 -∞ 0 0 · x1
  [ac(x1)]	=	-∞ -∞ 0 + 0 -∞ 0 0 0 0 0 0 0 · x1
  [bc(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 0 0 0 0 0 · x1
  [bc#(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [cc(x1)]	=	-∞ -∞ 0 + 0 0 -∞ 0 0 0 0 1 0 · x1
  [ca(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 0 -∞ 0 0 -∞ · x1
  [ab#(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ac#(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [cc#(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1

  the pairs

  bc#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(68)
  bc#(cc(ca(x1)))	→	bb#(bb(ba(x1)))	(69)
  bb#(bb(bc(cc(ca(x1)))))	→	cc#(cc(ca(aa(aa(aa(aa(x1)))))))	(83)
  bc#(cc(cc(x1)))	→	ab#(bb(bb(bc(x1))))	(71)
  bb#(bb(bc(cc(cc(x1)))))	→	cc#(cc(ca(aa(aa(aa(ac(x1)))))))	(86)
  bb#(bb(bc(cc(cc(x1)))))	→	ac#(x1)	(88)
  bc#(cc(cc(x1)))	→	bb#(bb(bc(x1)))	(72)
  bc#(cc(cc(x1)))	→	bb#(bc(x1))	(73)
  bc#(cc(cc(x1)))	→	bc#(x1)	(74)

  could be deleted.

  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

    ac#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(61)
    ab#(bb(bc(cc(ca(x1)))))	→	ac#(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(75)
    ac#(cc(cc(x1)))	→	ab#(bb(bb(bc(x1))))	(64)
    ab#(bb(bc(cc(ca(x1)))))	→	cc#(cc(ca(aa(aa(aa(aa(x1)))))))	(76)
    cc#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(54)
    ab#(bb(bc(cc(cc(x1)))))	→	ac#(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(78)
    ab#(bb(bc(cc(cc(x1)))))	→	cc#(cc(ca(aa(aa(aa(ac(x1)))))))	(79)
    ab#(bb(bc(cc(cc(x1)))))	→	ac#(x1)	(81)

    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

    [ac#(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [cc(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ -∞ 0 0 1 -∞ · x1
    [ca(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ 0 -∞ -∞ · x1
    [ab#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 -∞ · x1
    [ba(x1)]	=	0 -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bc(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 1 0 · x1
    [aa(x1)]	=	-∞ 0 0 + 0 -∞ -∞ 0 0 0 0 0 0 · x1
    [cc#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [ac(x1)]	=	-∞ 0 0 + 0 1 0 0 0 -∞ 0 0 0 · x1
    [ab(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1

    the pair

    ab#(bb(bc(cc(cc(x1)))))

    →

    ac#(x1)

    (81)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [ac#(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [cc(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ -∞ -∞ 0 -∞ 0 -∞ · x1
    [ca(x1)]	=	-∞ -∞ 0 + 0 0 0 -∞ -∞ 0 -∞ 0 0 · x1
    [ab#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	0 0 0 + -∞ 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [ba(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
    [bc(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 1 0 · x1
    [aa(x1)]	=	0 0 -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [cc#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [ac(x1)]	=	0 0 1 + 0 0 0 0 0 1 -∞ 0 -∞ · x1
    [ab(x1)]	=	0 0 -∞ + 0 0 0 0 0 0 0 0 0 · x1

    together with the usable rules

    bb(bb(ba(ab(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(10)
    bb(bb(ba(aa(x1))))	→	bb(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(11)
    bb(bb(ba(ac(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(12)
    cc(cc(ca(x1)))	→	ca(aa(aa(ab(bb(bb(ba(x1)))))))	(14)
    bc(cc(ca(x1)))	→	ba(aa(aa(ab(bb(bb(ba(x1)))))))	(20)
    bc(cc(cc(x1)))	→	ba(aa(aa(ab(bb(bb(bc(x1)))))))	(21)
    bb(bb(bc(cc(ca(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(29)
    bb(bb(bc(cc(cc(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(30)

    (w.r.t. the implicit argument filter of the reduction pair), the pairs

    ab#(bb(bc(cc(ca(x1)))))	→	ac#(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(75)
    ab#(bb(bc(cc(ca(x1)))))	→	cc#(cc(ca(aa(aa(aa(aa(x1)))))))	(76)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [ac#(x1)]	=	0 -∞ -∞ + -∞ 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [cc(x1)]	=	0 0 0 + -∞ 0 0 -∞ 0 -∞ 0 0 -∞ · x1
    [ca(x1)]	=	1 0 0 + 0 -∞ -∞ 0 0 0 0 0 0 · x1
    [ab#(x1)]	=	0 -∞ -∞ + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	0 -∞ -∞ + 0 0 -∞ -∞ 0 0 -∞ 0 -∞ · x1
    [ba(x1)]	=	0 -∞ 0 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bc(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ 0 0 0 · x1
    [cc#(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [aa(x1)]	=	0 0 0 + -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [ac(x1)]	=	0 0 0 + 0 0 0 0 0 0 -∞ -∞ 0 · x1
    [ab(x1)]	=	0 0 -∞ + -∞ -∞ 0 0 0 0 -∞ -∞ 0 · x1

    together with the usable rule

    cc(cc(ca(x1)))

    →

    ca(aa(aa(ab(bb(bb(ba(x1)))))))

    (14)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    ac#(cc(ca(x1)))

    →

    ab#(bb(bb(ba(x1))))

    (61)

    could be deleted.

    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

    [ac#(x1)]	=	0 -∞ -∞ + -∞ -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [cc(x1)]	=	0 0 0 + 0 0 0 1 0 0 0 0 0 · x1
    [ab#(x1)]	=	-∞ -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	-∞ -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1
    [bc(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ · x1
    [cc#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [ca(x1)]	=	-∞ 0 0 + 0 -∞ -∞ 1 0 -∞ 0 0 -∞ · x1
    [ba(x1)]	=	0 0 0 + -∞ 0 -∞ 0 0 -∞ 0 0 -∞ · x1
    [aa(x1)]	=	-∞ 0 0 + 0 -∞ -∞ 0 0 -∞ 0 0 0 · x1
    [ac(x1)]	=	-∞ 0 0 + 0 -∞ -∞ -∞ -∞ 0 0 0 1 · x1
    [ab(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 1 · x1

    the pair

    ac#(cc(cc(x1)))

    →

    ab#(bb(bb(bc(x1))))

    (64)

    could be deleted.

    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

      ab#(bb(bc(cc(cc(x1)))))	→	cc#(cc(ca(aa(aa(aa(ac(x1)))))))	(79)
      cc#(cc(ca(x1)))	→	ab#(bb(bb(ba(x1))))	(54)

      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

      [ab#(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [bb(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ 0 0 -∞ 0 0 0 · x1
      [bc(x1)]	=	-∞ -∞ -∞ + 0 -∞ 0 0 -∞ -∞ 0 -∞ 0 · x1
      [cc(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ 0 -∞ 1 -∞ · x1
      [cc#(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
      [ca(x1)]	=	-∞ 0 -∞ + 0 0 0 0 0 0 0 0 0 · x1
      [aa(x1)]	=	-∞ -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1
      [ac(x1)]	=	-∞ -∞ -∞ + 0 -∞ 0 0 -∞ 0 0 -∞ 0 · x1
      [ba(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ -∞ -∞ -∞ 0 0 0 · x1
      [ab(x1)]	=	-∞ -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1

      the pair

      ab#(bb(bc(cc(cc(x1)))))

      →

      cc#(cc(ca(aa(aa(aa(ac(x1)))))))

      (79)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [cc#(x1)]	=	1 + 1 · x1
      [cc(x1)]	=	0
      [ca(x1)]	=	0
      [ab#(x1)]	=	0
      [bb(x1)]	=	0
      [ba(x1)]	=	0
      [ab(x1)]	=	0
      [aa(x1)]	=	0
      [ac(x1)]	=	0
      [bc(x1)]	=	0

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

      cc#(cc(ca(x1)))

      →

      ab#(bb(bb(ba(x1))))

      (54)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

      There are no pairs anymore.

  • The 2^nd component contains the pair

    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(ba(x1)))))))	(40)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(39)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(ba(x1))))))	(41)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(ba(x1)))))	(42)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(ba(x1))))	(43)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(ba(x1)))	(44)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(31)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(46)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bc(x1)))))))	(47)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bc(x1))))))	(48)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bc(x1)))))	(49)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bc(x1))))	(50)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bc(x1)))	(51)
    bb#(bb(ba(ac(x1))))	→	bb#(bc(x1))	(52)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(x1)))))))	(32)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(x1))))))	(33)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(x1)))))	(34)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(x1))))	(35)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(x1)))	(36)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(x1))	(37)
    bb#(bb(ba(ab(x1))))	→	bb#(x1)	(38)

    1.1.1.1.1.1.1.1.2 Reduction Pair Processor

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

    [bb#(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	-∞ -∞ -∞ + 0 0 0 0 -∞ 0 0 0 0 · x1
    [ba(x1)]	=	1 0 -∞ + 0 0 0 -∞ 0 -∞ -∞ 0 0 · x1
    [aa(x1)]	=	0 0 0 + 0 0 0 0 -∞ -∞ 0 0 0 · x1
    [ab(x1)]	=	0 0 0 + 1 0 1 -∞ 0 0 0 0 0 · x1
    [ac(x1)]	=	-∞ 0 -∞ + 0 0 0 0 0 -∞ 0 0 0 · x1
    [bc(x1)]	=	-∞ -∞ -∞ + 0 0 0 0 0 0 0 0 0 · x1
    [cc(x1)]	=	-∞ 1 0 + 0 1 0 0 0 0 0 0 0 · x1
    [ca(x1)]	=	0 1 -∞ + 0 0 0 0 0 0 0 0 0 · x1

    the pair

    bb#(bb(ba(ab(x1))))

    →

    bb#(bb(x1))

    (37)

    could be deleted.

    1.1.1.1.1.1.1.1.2.1 Reduction Pair Processor

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

    [bb#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	0 -∞ 0 + 0 0 -∞ 0 0 0 0 0 0 · x1
    [ba(x1)]	=	0 -∞ 0 + -∞ -∞ -∞ -∞ -∞ -∞ 0 -∞ 0 · x1
    [aa(x1)]	=	0 0 0 + 0 -∞ -∞ 0 0 -∞ 0 -∞ 0 · x1
    [ab(x1)]	=	-∞ 0 1 + 0 0 0 0 0 0 1 1 1 · x1
    [ac(x1)]	=	0 0 -∞ + 0 0 -∞ 0 0 -∞ 0 0 -∞ · x1
    [bc(x1)]	=	0 0 -∞ + 0 0 -∞ 0 0 -∞ 0 0 -∞ · x1
    [cc(x1)]	=	-∞ 1 -∞ + 0 0 0 0 0 0 1 1 0 · x1
    [ca(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ 0 1 0 1 · x1

    the pairs

    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(31)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(x1)))))))	(32)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(bb(x1))))))	(33)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(bb(x1)))))	(34)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(bb(x1))))	(35)
    bb#(bb(ba(ab(x1))))	→	bb#(bb(bb(x1)))	(36)
    bb#(bb(ba(ab(x1))))	→	bb#(x1)	(38)

    could be deleted.

    1.1.1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [bb#(x1)]	=	1 · x1
    [bb(x1)]	=	1
    [ba(x1)]	=	0
    [aa(x1)]	=	0
    [ac(x1)]	=	0
    [bc(x1)]	=	0
    [ab(x1)]	=	0
    [cc(x1)]	=	0
    [ca(x1)]	=	0

    together with the usable rules

    bb(bb(ba(ab(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bb(x1))))))))	(10)
    bb(bb(ba(aa(x1))))	→	bb(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(11)
    bb(bb(ba(ac(x1))))	→	bb(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(12)
    bb(bb(bc(cc(ca(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(aa(x1))))))))	(29)
    bb(bb(bc(cc(cc(x1)))))	→	bc(cc(cc(ca(aa(aa(aa(ac(x1))))))))	(30)
    bc(cc(ca(x1)))	→	ba(aa(aa(ab(bb(bb(ba(x1)))))))	(20)
    bc(cc(cc(x1)))	→	ba(aa(aa(ab(bb(bb(bc(x1)))))))	(21)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    bb#(bb(ba(ac(x1))))

    →

    bb#(bc(x1))

    (52)

    could be deleted.

    1.1.1.1.1.1.1.1.2.1.1.1 Reduction Pair Processor

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

    [bb#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	-∞ -∞ 0 + 0 0 0 0 0 0 0 -∞ 0 · x1
    [ba(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ 0 0 0 0 0 -∞ · x1
    [aa(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ 0 -∞ 0 0 0 -∞ · x1
    [ac(x1)]	=	-∞ -∞ 1 + 0 -∞ 0 0 -∞ 0 1 -∞ 1 · x1
    [bc(x1)]	=	0 0 0 + 0 -∞ 0 0 -∞ 0 0 -∞ 0 · x1
    [ab(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 1 0 · x1
    [cc(x1)]	=	0 1 0 + -∞ 0 0 1 -∞ 1 -∞ -∞ 0 · x1
    [ca(x1)]	=	0 1 0 + -∞ -∞ -∞ 1 1 1 -∞ -∞ -∞ · x1

    the pairs

    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(bc(x1))))))))	(46)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bb(bc(x1)))))))	(47)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bb(bc(x1))))))	(48)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bb(bc(x1)))))	(49)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bb(bc(x1))))	(50)
    bb#(bb(ba(ac(x1))))	→	bb#(bb(bc(x1)))	(51)

    could be deleted.

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

    [bb#(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	0 0 0 + -∞ 0 0 0 -∞ -∞ -∞ 0 0 · x1
    [ba(x1)]	=	0 0 0 + -∞ 0 -∞ 0 0 0 0 0 0 · x1
    [aa(x1)]	=	0 1 -∞ + 0 0 0 0 1 0 0 -∞ 0 · x1
    [ab(x1)]	=	0 -∞ 0 + 0 0 0 -∞ 0 -∞ 0 0 0 · x1
    [ac(x1)]	=	0 0 0 + 0 -∞ -∞ 1 -∞ -∞ 0 -∞ -∞ · x1
    [bc(x1)]	=	0 0 0 + 1 -∞ -∞ 0 -∞ -∞ 0 -∞ -∞ · x1
    [cc(x1)]	=	0 1 0 + -∞ 1 0 1 -∞ -∞ 0 -∞ 0 · x1
    [ca(x1)]	=	0 1 0 + -∞ -∞ -∞ 1 1 1 -∞ -∞ 0 · x1

    the pair

    bb#(bb(ba(aa(x1))))

    →

    bb#(bb(ba(x1)))

    (44)

    could be deleted.

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

    [bb#(x1)]	=	0 -∞ -∞ + 0 -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
    [bb(x1)]	=	-∞ -∞ 0 + 0 -∞ -∞ 0 -∞ -∞ 0 0 -∞ · x1
    [ba(x1)]	=	0 0 0 + -∞ 0 0 1 0 0 0 0 0 · x1
    [aa(x1)]	=	0 -∞ 0 + -∞ 0 0 -∞ 0 -∞ 0 0 0 · x1
    [ab(x1)]	=	-∞ 0 -∞ + 0 0 -∞ 0 0 0 0 0 0 · x1
    [ac(x1)]	=	-∞ -∞ -∞ + 0 -∞ 0 -∞ -∞ 0 0 0 1 · x1
    [bc(x1)]	=	-∞ 0 0 + 0 0 1 -∞ -∞ 0 0 0 0 · x1
    [cc(x1)]	=	0 -∞ 1 + 0 -∞ 0 0 0 1 0 1 0 · x1
    [ca(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ 0 1 0 -∞ 0 -∞ · x1

    the pairs

    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(ba(x1)))))))	(40)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(bb(bb(ba(x1))))))))	(39)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(bb(ba(x1))))))	(41)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(bb(ba(x1)))))	(42)
    bb#(bb(ba(aa(x1))))	→	bb#(bb(bb(ba(x1))))	(43)

    could be deleted.

    1.1.1.1.1.1.1.1.2.1.1.1.1.1.1 P is empty

    There are no pairs anymore.