Certification Problem

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

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Closure Under Flat Contexts

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

1.1.1 Semantic Labeling

Root-labeling is applied.

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

  ba#(ab(x1))	→	bb#(x1)	(43)
  bb#(bc(ca(x1)))	→	ba#(aa(x1))	(93)
  ba#(aa(x1))	→	ba#(x1)	(42)
  ba#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(61)
  cb#(bc(ca(x1)))	→	ca#(aa(x1))	(98)
  ca#(aa(x1))	→	ca#(x1)	(44)
  ca#(ab(x1))	→	cb#(x1)	(45)
  cb#(bc(ca(x1)))	→	aa#(x1)	(99)
  aa#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(47)
  cb#(bc(cb(x1)))	→	ca#(ab(x1))	(100)
  ca#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(75)
  cb#(bc(cb(x1)))	→	ab#(x1)	(101)
  ab#(bc(ca(x1)))	→	aa#(aa(x1))	(88)
  aa#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(48)
  ba#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(62)
  ba#(aa(aa(x1)))	→	ab#(ba(x1))	(63)
  ab#(bc(ca(x1)))	→	aa#(x1)	(89)
  aa#(aa(aa(x1)))	→	ab#(ba(x1))	(49)
  ab#(bc(cb(x1)))	→	aa#(ab(x1))	(90)
  aa#(aa(aa(x1)))	→	ba#(x1)	(50)
  ba#(aa(aa(x1)))	→	ba#(x1)	(64)
  ba#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(66)
  ba#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(67)
  ba#(aa(ab(x1)))	→	ab#(bb(x1))	(68)
  ab#(bc(cb(x1)))	→	ab#(x1)	(91)
  ba#(aa(ab(x1)))	→	bb#(x1)	(69)
  bb#(bc(ca(x1)))	→	aa#(x1)	(94)
  aa#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(52)
  aa#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(53)
  ba#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(71)
  ba#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(72)
  ba#(aa(ac(x1)))	→	ab#(bc(x1))	(73)
  aa#(aa(ab(x1)))	→	ab#(bb(x1))	(54)
  aa#(aa(ab(x1)))	→	bb#(x1)	(55)
  bb#(bc(cb(x1)))	→	ba#(ab(x1))	(95)
  bb#(bc(cb(x1)))	→	ab#(x1)	(96)
  aa#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(57)
  aa#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(58)
  aa#(aa(ac(x1)))	→	ab#(bc(x1))	(59)
  ca#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(76)
  ca#(aa(aa(x1)))	→	ab#(ba(x1))	(77)
  ca#(aa(aa(x1)))	→	ba#(x1)	(78)
  ca#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(80)
  ca#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(81)
  ca#(aa(ab(x1)))	→	ab#(bb(x1))	(82)
  ca#(aa(ab(x1)))	→	bb#(x1)	(83)
  ca#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(85)
  ca#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(86)
  ca#(aa(ac(x1)))	→	ab#(bc(x1))	(87)

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  bb#(bc(ca(x1)))	→	ba#(aa(x1))	(93)
  ba#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(61)
  cb#(bc(ca(x1)))	→	ca#(aa(x1))	(98)
  cb#(bc(ca(x1)))	→	aa#(x1)	(99)
  aa#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(47)
  cb#(bc(cb(x1)))	→	ca#(ab(x1))	(100)
  ca#(aa(aa(x1)))	→	cb#(ba(ab(ba(x1))))	(75)
  cb#(bc(cb(x1)))	→	ab#(x1)	(101)
  ab#(bc(ca(x1)))	→	aa#(aa(x1))	(88)
  aa#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(48)
  ba#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(62)
  ba#(aa(aa(x1)))	→	ab#(ba(x1))	(63)
  ab#(bc(ca(x1)))	→	aa#(x1)	(89)
  aa#(aa(aa(x1)))	→	ab#(ba(x1))	(49)
  ab#(bc(cb(x1)))	→	aa#(ab(x1))	(90)
  aa#(aa(aa(x1)))	→	ba#(x1)	(50)
  ba#(aa(aa(x1)))	→	ba#(x1)	(64)
  ba#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(66)
  ba#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(67)
  ba#(aa(ab(x1)))	→	ab#(bb(x1))	(68)
  ab#(bc(cb(x1)))	→	ab#(x1)	(91)
  ba#(aa(ab(x1)))	→	bb#(x1)	(69)
  bb#(bc(ca(x1)))	→	aa#(x1)	(94)
  aa#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(52)
  aa#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(53)
  ba#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(71)
  ba#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(72)
  ba#(aa(ac(x1)))	→	ab#(bc(x1))	(73)
  aa#(aa(ab(x1)))	→	ab#(bb(x1))	(54)
  aa#(aa(ab(x1)))	→	bb#(x1)	(55)
  bb#(bc(cb(x1)))	→	ba#(ab(x1))	(95)
  bb#(bc(cb(x1)))	→	ab#(x1)	(96)
  aa#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(57)
  aa#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(58)
  aa#(aa(ac(x1)))	→	ab#(bc(x1))	(59)
  ca#(aa(aa(x1)))	→	ba#(ab(ba(x1)))	(76)
  ca#(aa(aa(x1)))	→	ab#(ba(x1))	(77)
  ca#(aa(aa(x1)))	→	ba#(x1)	(78)
  ca#(aa(ab(x1)))	→	cb#(ba(ab(bb(x1))))	(80)
  ca#(aa(ab(x1)))	→	ba#(ab(bb(x1)))	(81)
  ca#(aa(ab(x1)))	→	ab#(bb(x1))	(82)
  ca#(aa(ab(x1)))	→	bb#(x1)	(83)
  ca#(aa(ac(x1)))	→	cb#(ba(ab(bc(x1))))	(85)
  ca#(aa(ac(x1)))	→	ba#(ab(bc(x1)))	(86)
  ca#(aa(ac(x1)))	→	ab#(bc(x1))	(87)

  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

    ba#(aa(x1))

    →

    ba#(x1)

    (42)

    1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [aa(x1)]	=	1 · x1
    [ba#(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 Size-Change Termination

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

    ba#(aa(x1))	→	ba#(x1)	(42)
    1	>	1

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

  • The 2^nd component contains the pair

    ca#(aa(x1))

    →

    ca#(x1)

    (44)

    1.1.1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [aa(x1)]	=	1 · x1
    [ca#(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.2.1 Size-Change Termination

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

    ca#(aa(x1))	→	ca#(x1)	(44)
    1	>	1

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