Certification Problem

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

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(☐), c(☐), b(☐)}

1.1.1 Semantic Labeling

Root-labeling is applied.

1.1.1.1 Rule Removal

1.1.1.1.1 Dependency Pair Transformation

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  ac#(cc(cb(x1)))	→	ba#(aa(aa(ab(x1))))	(64)
  ba#(aa(x1))	→	bc#(cb(ba(x1)))	(55)
  bc#(cc(cb(x1)))	→	ba#(aa(aa(ab(x1))))	(67)
  ba#(aa(x1))	→	cb#(ba(x1))	(56)
  cb#(ba(ab(ba(x1))))	→	ca#(x1)	(63)
  ca#(aa(x1))	→	cb#(ba(x1))	(50)
  ca#(aa(x1))	→	ba#(x1)	(51)
  ba#(aa(x1))	→	ba#(x1)	(57)
  ba#(ac(x1))	→	bc#(cb(bc(x1)))	(58)
  bc#(cc(cb(x1)))	→	aa#(aa(ab(x1)))	(68)
  aa#(aa(x1))	→	ac#(cb(ba(x1)))	(42)
  ac#(cc(cb(x1)))	→	aa#(aa(ab(x1)))	(65)
  aa#(aa(x1))	→	cb#(ba(x1))	(43)
  aa#(aa(x1))	→	ba#(x1)	(44)
  ba#(ac(x1))	→	bc#(x1)	(60)
  aa#(ac(x1))	→	ac#(cb(bc(x1)))	(45)
  aa#(ac(x1))	→	bc#(x1)	(47)
  ca#(ac(x1))	→	bc#(x1)	(53)

  1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  ba(aa(x1))	→	bc(cb(ba(x1)))	(21)
  ba(ac(x1))	→	bc(cb(bc(x1)))	(22)
  ba(ab(x1))	→	bc(cb(bb(x1)))	(23)
  cb(ba(ab(ba(x1))))	→	ca(x1)	(27)
  cb(ba(ab(bc(x1))))	→	cc(x1)	(28)
  bc(cc(cb(x1)))	→	bb(ba(aa(aa(ab(x1)))))	(41)
  ca(aa(x1))	→	cc(cb(ba(x1)))	(18)
  ca(ac(x1))	→	cc(cb(bc(x1)))	(19)
  ca(ab(x1))	→	cc(cb(bb(x1)))	(20)

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

  aa#(ac(x1))

  →

  ac#(cb(bc(x1)))

  (45)

  could be deleted.

  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)]	=	1 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [cc(x1)]	=	0 1 0 + 0 0 0 0 0 0 0 0 0 · x1
  [cb(x1)]	=	-∞ -∞ -∞ + 0 0 0 -∞ 0 0 0 0 0 · x1
  [ba#(x1)]	=	1 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [aa(x1)]	=	-∞ 1 0 + 0 0 0 0 0 0 0 -∞ -∞ · x1
  [ab(x1)]	=	-∞ 1 -∞ + 0 -∞ 0 0 0 0 0 -∞ 0 · x1
  [bc#(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ba(x1)]	=	-∞ 0 -∞ + 0 -∞ 0 0 -∞ 0 0 0 0 · x1
  [cb#(x1)]	=	1 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ca#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ac(x1)]	=	0 0 0 + 0 0 0 0 0 0 0 0 0 · x1
  [bc(x1)]	=	-∞ 0 0 + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [aa#(x1)]	=	0 -∞ -∞ + 0 0 0 -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [bb(x1)]	=	-∞ -∞ -∞ + 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ca(x1)]	=	0 1 0 + 0 -∞ 0 0 0 0 0 -∞ -∞ · x1

  the pair

  ba#(ac(x1))

  →

  bc#(cb(bc(x1)))

  (58)

  could be deleted.

  1.1.1.1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  cb#(ba(ab(ba(x1))))	→	ca#(x1)	(63)
  ca#(aa(x1))	→	cb#(ba(x1))	(50)
  ca#(aa(x1))	→	ba#(x1)	(51)
  bc#(cc(cb(x1)))	→	aa#(aa(ab(x1)))	(68)
  ac#(cc(cb(x1)))	→	aa#(aa(ab(x1)))	(65)
  ca#(ac(x1))	→	bc#(x1)	(53)

  could be deleted.

  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

    bc#(cc(cb(x1)))	→	ba#(aa(aa(ab(x1))))	(67)
    ba#(aa(x1))	→	bc#(cb(ba(x1)))	(55)
    ba#(aa(x1))	→	ba#(x1)	(57)
    ba#(ac(x1))	→	bc#(x1)	(60)

    1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

    ba#(ac(x1))

    →

    bc#(x1)

    (60)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pair

    ba#(aa(x1))

    →

    ba#(x1)

    (57)

    could be deleted.

    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

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

    the pair

    bc#(cc(cb(x1)))

    →

    ba#(aa(aa(ab(x1))))

    (67)

    could be deleted.

    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

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

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

    ba#(aa(x1))

    →

    bc#(cb(ba(x1)))

    (55)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.