Certification Problem

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

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

• The 1^st component contains the pair

  ac#(cc(ca(x1)))	→	aa#(ac(ca(x1)))	(70)
  aa#(ab(ba(x1)))	→	ac#(ca(x1))	(55)
  ac#(cc(ca(x1)))	→	ac#(ca(x1))	(71)
  ac#(cc(cb(x1)))	→	aa#(ac(cb(x1)))	(75)
  aa#(ab(bb(x1)))	→	ac#(cb(x1))	(57)
  ac#(cc(cb(x1)))	→	ac#(cb(x1))	(76)
  ac#(cc(cc(x1)))	→	aa#(ac(cc(x1)))	(80)
  aa#(ab(bc(x1)))	→	ac#(cc(x1))	(59)
  ac#(cc(cc(x1)))	→	ac#(cc(x1))	(81)

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the pairs

  ac#(cc(ca(x1)))	→	aa#(ac(ca(x1)))	(70)
  ac#(cc(ca(x1)))	→	ac#(ca(x1))	(71)
  ac#(cc(cb(x1)))	→	aa#(ac(cb(x1)))	(75)
  ac#(cc(cb(x1)))	→	ac#(cb(x1))	(76)
  ac#(cc(cc(x1)))	→	aa#(ac(cc(x1)))	(80)
  ac#(cc(cc(x1)))	→	ac#(cc(x1))	(81)

  could be deleted.

  1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  ba#(aa(x1))

  →

  ba#(x1)

  (53)

  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
  [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.2.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)	(53)
  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#(ab(ba(x1)))	→	ca#(x1)	(62)
  ca#(aa(x1))	→	ca#(x1)	(54)
  ca#(ab(bb(x1)))	→	cb#(x1)	(63)
  cb#(ba(x1))	→	ca#(x1)	(65)
  cb#(bb(x1))	→	cb#(x1)	(66)

  1.1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  ca#(ab(bb(x1)))	→	cb#(x1)	(63)
  1	>	1
  cb#(ba(x1))	→	ca#(x1)	(65)
  1	>	1
  cb#(bb(x1))	→	cb#(x1)	(66)
  1	>	1
  ca#(ab(ba(x1)))	→	ca#(x1)	(62)
  1	>	1
  ca#(aa(x1))	→	ca#(x1)	(54)
  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)

  (64)

  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)	(64)
  1	>	1

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