Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-478)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Closure Under Flat Contexts

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

1.1 Semantic Labeling

Root-labeling is applied.

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  ac#(cb(ba(x1)))	→	aa#(ac(ca(x1)))	(47)
  aa#(ac(x1))	→	bb#(bc(cc(x1)))	(40)
  bb#(ba(ac(x1)))	→	bc#(x1)	(43)
  bc#(cb(bc(x1)))	→	cc#(x1)	(57)
  cc#(cb(bc(x1)))	→	cc#(x1)	(62)
  cc#(cb(bb(x1)))	→	ac#(cb(x1))	(61)
  ac#(cb(bc(x1)))	→	aa#(ac(cc(x1)))	(53)
  aa#(ac(x1))	→	cc#(x1)	(38)
  cc#(cb(bb(x1)))	→	cb#(x1)	(60)
  cb#(ba(ac(x1)))	→	cc#(x1)	(45)
  cb#(ba(ab(x1)))	→	cb#(x1)	(44)
  aa#(ab(x1))	→	bb#(bc(cb(x1)))	(36)
  bb#(ba(ab(x1)))	→	bb#(x1)	(42)
  aa#(ab(x1))	→	bc#(cb(x1))	(35)
  bc#(cb(bb(x1)))	→	ac#(cb(x1))	(56)
  ac#(cb(bc(x1)))	→	cc#(x1)	(51)
  ac#(cb(bb(x1)))	→	aa#(ac(cb(x1)))	(50)
  aa#(ab(x1))	→	cb#(x1)	(34)
  ac#(cb(bb(x1)))	→	ac#(cb(x1))	(49)
  ac#(cb(bb(x1)))	→	cb#(x1)	(48)
  bc#(cb(bb(x1)))	→	cb#(x1)	(55)

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

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

  together with the usable rules

  aa(aa(x1))	→	ab(bb(bc(ca(x1))))	(10)
  aa(ab(x1))	→	ab(bb(bc(cb(x1))))	(11)
  aa(ac(x1))	→	ab(bb(bc(cc(x1))))	(12)
  ab(ba(aa(x1)))	→	aa(x1)	(13)
  ab(ba(ab(x1)))	→	ab(x1)	(14)
  ab(ba(ac(x1)))	→	ac(x1)	(15)
  bb(ba(aa(x1)))	→	ba(x1)	(16)
  bb(ba(ab(x1)))	→	bb(x1)	(17)
  bb(ba(ac(x1)))	→	bc(x1)	(18)
  cb(ba(aa(x1)))	→	ca(x1)	(19)
  cb(ba(ab(x1)))	→	cb(x1)	(20)
  cb(ba(ac(x1)))	→	cc(x1)	(21)
  ac(cb(ba(x1)))	→	aa(ac(ca(x1)))	(22)
  ac(cb(bb(x1)))	→	aa(ac(cb(x1)))	(23)
  ac(cb(bc(x1)))	→	aa(ac(cc(x1)))	(24)
  bc(cb(ba(x1)))	→	ba(ac(ca(x1)))	(25)
  bc(cb(bb(x1)))	→	ba(ac(cb(x1)))	(26)
  bc(cb(bc(x1)))	→	ba(ac(cc(x1)))	(27)
  cc(cb(ba(x1)))	→	ca(ac(ca(x1)))	(28)
  cc(cb(bb(x1)))	→	ca(ac(cb(x1)))	(29)
  cc(cb(bc(x1)))	→	ca(ac(cc(x1)))	(30)

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

  ac#(cb(ba(x1)))

  →

  aa#(ac(ca(x1)))

  (47)

  could be deleted.

  1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

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

  together with the usable rules

  aa(aa(x1))	→	ab(bb(bc(ca(x1))))	(10)
  aa(ab(x1))	→	ab(bb(bc(cb(x1))))	(11)
  aa(ac(x1))	→	ab(bb(bc(cc(x1))))	(12)
  ab(ba(aa(x1)))	→	aa(x1)	(13)
  ab(ba(ab(x1)))	→	ab(x1)	(14)
  ab(ba(ac(x1)))	→	ac(x1)	(15)
  bb(ba(aa(x1)))	→	ba(x1)	(16)
  bb(ba(ab(x1)))	→	bb(x1)	(17)
  bb(ba(ac(x1)))	→	bc(x1)	(18)
  cb(ba(aa(x1)))	→	ca(x1)	(19)
  cb(ba(ab(x1)))	→	cb(x1)	(20)
  cb(ba(ac(x1)))	→	cc(x1)	(21)
  ac(cb(ba(x1)))	→	aa(ac(ca(x1)))	(22)
  ac(cb(bb(x1)))	→	aa(ac(cb(x1)))	(23)
  ac(cb(bc(x1)))	→	aa(ac(cc(x1)))	(24)
  bc(cb(ba(x1)))	→	ba(ac(ca(x1)))	(25)
  bc(cb(bb(x1)))	→	ba(ac(cb(x1)))	(26)
  bc(cb(bc(x1)))	→	ba(ac(cc(x1)))	(27)
  cc(cb(ba(x1)))	→	ca(ac(ca(x1)))	(28)
  cc(cb(bb(x1)))	→	ca(ac(cb(x1)))	(29)
  cc(cb(bc(x1)))	→	ca(ac(cc(x1)))	(30)

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

  bb#(ba(ac(x1)))	→	bc#(x1)	(43)
  ac#(cb(bc(x1)))	→	aa#(ac(cc(x1)))	(53)
  cc#(cb(bb(x1)))	→	cb#(x1)	(60)
  ac#(cb(bb(x1)))	→	cb#(x1)	(48)
  bc#(cb(bb(x1)))	→	cb#(x1)	(55)

  could be deleted.

  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#(cb(bc(x1)))	→	cc#(x1)	(51)
    cc#(cb(bc(x1)))	→	cc#(x1)	(62)
    cc#(cb(bb(x1)))	→	ac#(cb(x1))	(61)
    ac#(cb(bb(x1)))	→	aa#(ac(cb(x1)))	(50)
    aa#(ac(x1))	→	cc#(x1)	(38)
    aa#(ab(x1))	→	bc#(cb(x1))	(35)
    bc#(cb(bc(x1)))	→	cc#(x1)	(57)
    bc#(cb(bb(x1)))	→	ac#(cb(x1))	(56)
    ac#(cb(bb(x1)))	→	ac#(cb(x1))	(49)
    aa#(ab(x1))	→	cb#(x1)	(34)
    cb#(ba(ac(x1)))	→	cc#(x1)	(45)
    cb#(ba(ab(x1)))	→	cb#(x1)	(44)

    1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the arctic semiring over the integers

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

    together with the usable rules

    aa(aa(x1))	→	ab(bb(bc(ca(x1))))	(10)
    aa(ab(x1))	→	ab(bb(bc(cb(x1))))	(11)
    aa(ac(x1))	→	ab(bb(bc(cc(x1))))	(12)
    ab(ba(aa(x1)))	→	aa(x1)	(13)
    ab(ba(ab(x1)))	→	ab(x1)	(14)
    ab(ba(ac(x1)))	→	ac(x1)	(15)
    bb(ba(aa(x1)))	→	ba(x1)	(16)
    bb(ba(ab(x1)))	→	bb(x1)	(17)
    bb(ba(ac(x1)))	→	bc(x1)	(18)
    cb(ba(aa(x1)))	→	ca(x1)	(19)
    cb(ba(ab(x1)))	→	cb(x1)	(20)
    cb(ba(ac(x1)))	→	cc(x1)	(21)
    ac(cb(ba(x1)))	→	aa(ac(ca(x1)))	(22)
    ac(cb(bb(x1)))	→	aa(ac(cb(x1)))	(23)
    ac(cb(bc(x1)))	→	aa(ac(cc(x1)))	(24)
    bc(cb(ba(x1)))	→	ba(ac(ca(x1)))	(25)
    bc(cb(bb(x1)))	→	ba(ac(cb(x1)))	(26)
    bc(cb(bc(x1)))	→	ba(ac(cc(x1)))	(27)
    cc(cb(ba(x1)))	→	ca(ac(ca(x1)))	(28)
    cc(cb(bb(x1)))	→	ca(ac(cb(x1)))	(29)
    cc(cb(bc(x1)))	→	ca(ac(cc(x1)))	(30)

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

    ac#(cb(bc(x1)))	→	cc#(x1)	(51)
    bc#(cb(bc(x1)))	→	cc#(x1)	(57)
    bc#(cb(bb(x1)))	→	ac#(cb(x1))	(56)
    ac#(cb(bb(x1)))	→	ac#(cb(x1))	(49)
    aa#(ab(x1))	→	cb#(x1)	(34)

    could be deleted.

    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

      cb#(ba(ab(x1)))

      →

      cb#(x1)

      (44)

      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.

      cb#(ba(ab(x1)))	→	cb#(x1)	(44)
      1	>	1

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

    • The 2^nd component contains the pair

      ac#(cb(bb(x1)))	→	aa#(ac(cb(x1)))	(50)
      aa#(ac(x1))	→	cc#(x1)	(38)
      cc#(cb(bc(x1)))	→	cc#(x1)	(62)
      cc#(cb(bb(x1)))	→	ac#(cb(x1))	(61)

      1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the arctic semiring over the integers

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

      together with the usable rules

      aa(aa(x1))	→	ab(bb(bc(ca(x1))))	(10)
      aa(ab(x1))	→	ab(bb(bc(cb(x1))))	(11)
      aa(ac(x1))	→	ab(bb(bc(cc(x1))))	(12)
      ab(ba(aa(x1)))	→	aa(x1)	(13)
      ab(ba(ab(x1)))	→	ab(x1)	(14)
      ab(ba(ac(x1)))	→	ac(x1)	(15)
      bb(ba(aa(x1)))	→	ba(x1)	(16)
      bb(ba(ab(x1)))	→	bb(x1)	(17)
      bb(ba(ac(x1)))	→	bc(x1)	(18)
      cb(ba(aa(x1)))	→	ca(x1)	(19)
      cb(ba(ab(x1)))	→	cb(x1)	(20)
      cb(ba(ac(x1)))	→	cc(x1)	(21)
      ac(cb(ba(x1)))	→	aa(ac(ca(x1)))	(22)
      ac(cb(bb(x1)))	→	aa(ac(cb(x1)))	(23)
      ac(cb(bc(x1)))	→	aa(ac(cc(x1)))	(24)
      bc(cb(ba(x1)))	→	ba(ac(ca(x1)))	(25)
      bc(cb(bb(x1)))	→	ba(ac(cb(x1)))	(26)
      bc(cb(bc(x1)))	→	ba(ac(cc(x1)))	(27)
      cc(cb(ba(x1)))	→	ca(ac(ca(x1)))	(28)
      cc(cb(bb(x1)))	→	ca(ac(cb(x1)))	(29)
      cc(cb(bc(x1)))	→	ca(ac(cc(x1)))	(30)

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

      cc#(cb(bb(x1)))

      →

      ac#(cb(x1))

      (61)

      could be deleted.

      1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        cc#(cb(bc(x1)))

        →

        cc#(x1)

        (62)

        1.1.1.1.1.1.1.1.1.2.1.1 Size-Change Termination

        Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

        cc#(cb(bc(x1)))	→	cc#(x1)	(62)
        1	>	1

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

  • The 2^nd component contains the pair

    bb#(ba(ab(x1)))

    →

    bb#(x1)

    (42)

    1.1.1.1.1.1.1.2 Size-Change Termination

    Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

    bb#(ba(ab(x1)))	→	bb#(x1)	(42)
    1	>	1

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