Certification Problem

Input (TPDB SRS_Standard/Zantema_06/abc)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

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

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 6 components.

• The 1^st component contains the pair

  aa#(ab(bc(cb(x1))))	→	ba#(aa(ab(x1)))	(57)
  ba#(ab(bc(cb(x1))))	→	ba#(aa(ab(x1)))	(71)
  ba#(ab(bc(cb(x1))))	→	aa#(ab(x1))	(72)
  aa#(ab(bc(cb(x1))))	→	aa#(ab(x1))	(58)
  aa#(ab(bc(cc(x1))))	→	ba#(aa(ac(x1)))	(64)
  ba#(ab(bc(cc(x1))))	→	ba#(aa(ac(x1)))	(78)
  ba#(ab(bc(cc(x1))))	→	aa#(ac(x1))	(79)
  aa#(ab(bc(cc(x1))))	→	aa#(ac(x1))	(65)
  ba#(aa(x1))	→	ba#(x1)	(81)

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  aa#(ab(bc(cb(x1))))	→	ba#(aa(ab(x1)))	(57)
  ba#(ab(bc(cb(x1))))	→	ba#(aa(ab(x1)))	(71)
  ba#(ab(bc(cb(x1))))	→	aa#(ab(x1))	(72)
  aa#(ab(bc(cb(x1))))	→	aa#(ab(x1))	(58)
  aa#(ab(bc(cc(x1))))	→	ba#(aa(ac(x1)))	(64)
  ba#(ab(bc(cc(x1))))	→	ba#(aa(ac(x1)))	(78)
  ba#(ab(bc(cc(x1))))	→	aa#(ac(x1))	(79)
  aa#(ab(bc(cc(x1))))	→	aa#(ac(x1))	(65)

  could be deleted.

  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 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)	(81)
  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#(cc(x1))

  →

  ac#(x1)

  (87)

  1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  ac#(cc(x1))	→	ac#(x1)	(87)
  1	>	1

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

• The 3^rd component contains the pair

  ca#(aa(x1))

  →

  ca#(x1)

  (83)

  1.1.1.1.1.3 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.3.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)	(83)
  1	>	1

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

• The 4^th component contains the pair

  ab#(bb(x1))

  →

  ab#(x1)

  (84)

  1.1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [bb(x1)]	=	1 · x1
  [ab#(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.4.1 Size-Change Termination

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

  ab#(bb(x1))	→	ab#(x1)	(84)
  1	>	1

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

• The 5^th component contains the pair

  cb#(bb(x1))

  →

  cb#(x1)

  (85)

  1.1.1.1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [bb(x1)]	=	1 · x1
  [cb#(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.5.1 Size-Change Termination

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

  cb#(bb(x1))	→	cb#(x1)	(85)
  1	>	1

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

• The 6^th component contains the pair

  bc#(cc(x1))

  →

  bc#(x1)

  (88)

  1.1.1.1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [cc(x1)]	=	1 · x1
  [bc#(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.6.1 Size-Change Termination

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

  bc#(cc(x1))	→	bc#(x1)	(88)
  1	>	1

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