Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z043)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

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

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

  bc#(cb(ba(aa(ab(x1)))))	→	bc#(cb(ba(ac(cb(x1)))))	(24)
  bc#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(25)
  ac#(cb(ba(aa(ac(x1)))))	→	bc#(cb(ba(ac(cc(x1)))))	(28)
  ac#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(30)
  cc#(cb(ba(aa(ac(x1)))))	→	bc#(cb(ba(ac(cc(x1)))))	(14)
  cc#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(16)
  cc#(cb(ba(aa(ab(x1)))))	→	bc#(cb(ba(ac(cb(x1)))))	(17)
  cc#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(18)
  ac#(cb(ba(aa(ab(x1)))))	→	bc#(cb(ba(ac(cb(x1)))))	(31)
  ac#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(32)

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

  ac(cb(ba(aa(ac(x1)))))	→	aa(aa(ab(ba(aa(ab(bc(cb(ba(ac(cc(x1)))))))))))	(11)
  ac(cb(ba(aa(ab(x1)))))	→	aa(aa(ab(ba(aa(ab(bc(cb(ba(ac(cb(x1)))))))))))	(12)
  ac(cb(ba(aa(aa(x1)))))	→	aa(aa(ab(ba(aa(ab(bc(cb(ba(ac(ca(x1)))))))))))	(13)

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

  bc#(cb(ba(aa(ab(x1)))))	→	bc#(cb(ba(ac(cb(x1)))))	(24)
  bc#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(25)

  could be deleted.

  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#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(30)
    cc#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(16)
    cc#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(18)
    ac#(cb(ba(aa(ab(x1)))))	→	ac#(cb(x1))	(32)

    1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [cb(x1)]	=	1 · x1
    [ba(x1)]	=	1 · x1
    [aa(x1)]	=	1 · x1
    [ac(x1)]	=	1 · x1
    [ab(x1)]	=	1 · x1
    [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.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

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

    the pairs

    ac#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(30)
    cc#(cb(ba(aa(ac(x1)))))	→	cc#(x1)	(16)

    could be deleted.

    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

      ac#(cb(ba(aa(ab(x1)))))

      →

      ac#(cb(x1))

      (32)

      1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

      [ac#(x1)]	=	-2 + x1
      [cb(x1)]	=	2 · x1
      [ba(x1)]	=	2 · x1
      [aa(x1)]	=	2 · x1
      [ab(x1)]	=	2 + 2 · x1

      the pair

      ac#(cb(ba(aa(ab(x1)))))

      →

      ac#(cb(x1))

      (32)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1 P is empty

      There are no pairs anymore.