Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/abaaaaaa-aaaaaaabaaab.srs)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Semantic Labeling

Root-labeling is applied.

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  ab#(ba(aa(aa(aa(aa(aa(aa(x1))))))))	→	ab#(ba(x1))	(5)
  ab#(ba(aa(aa(aa(aa(aa(aa(x1))))))))	→	ab#(ba(aa(aa(ab(ba(x1))))))	(4)

  1.1.1.1 Split

  We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD

  There are no rules.

  and the rules RD

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

  →

  aa(aa(aa(aa(aa(aa(ab(ba(aa(aa(ab(bb(x1))))))))))))

  (3)

  are deleted.

  1.1.1.1.1 Semantic Labeling Processor

  The following interpretations form a model of the rules.

  As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

  [bb(x1)]	=	0
  [ba(x1)]	=	0
  [ab#(x1)]	=	0
  [ab(x1)]	=	0
  [aa(x1)]	=	1 + 1x1

  We obtain the set of labeled pairs

  ab#0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))	→	ab#0(ba0(x1))	(8)
  ab#0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))	→	ab#0(ba0(aa1(aa0(ab0(ba0(x1))))))	(9)
  ab#0(ba1(aa0(aa1(aa0(aa1(aa0(aa1(x1))))))))	→	ab#0(ba0(aa1(aa0(ab0(ba1(x1))))))	(10)
  ab#0(ba1(aa0(aa1(aa0(aa1(aa0(aa1(x1))))))))	→	ab#0(ba1(x1))	(11)

  and the set of labeled rules:

  ab0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))	→	aa1(aa0(aa1(aa0(aa1(aa0(ab0(ba0(aa1(aa0(ab0(ba0(x1))))))))))))	(12)
  ab0(ba1(aa0(aa1(aa0(aa1(aa0(aa1(x1))))))))	→	aa1(aa0(aa1(aa0(aa1(aa0(ab0(ba0(aa1(aa0(ab0(ba1(x1))))))))))))	(13)
  ab0(ba1(aa0(aa1(aa0(aa1(aa0(ab0(x1))))))))	→	aa1(aa0(aa1(aa0(aa1(aa0(ab0(ba0(aa1(aa0(ab0(bb0(x1))))))))))))	(14)
  ab0(ba1(aa0(aa1(aa0(aa1(aa0(ab1(x1))))))))	→	aa1(aa0(aa1(aa0(aa1(aa0(ab0(ba0(aa1(aa0(ab0(bb1(x1))))))))))))	(15)

  1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    ab#0(ba1(aa0(aa1(aa0(aa1(aa0(aa1(x1))))))))

    →

    ab#0(ba1(x1))

    (11)

    1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [ab#0(x1)]	=	1 · x1
    [ba1(x1)]	=	1 · x1
    [aa0(x1)]	=	1 · x1
    [aa1(x1)]	=	1 · x1

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

    ab#0(ba1(aa0(aa1(aa0(aa1(aa0(aa1(x1))))))))

    →

    ab#0(ba1(x1))

    (11)

    and no rules could be deleted.

    1.1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.

  • The 2^nd component contains the pair

    ab#0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))	→	ab#0(ba0(aa1(aa0(ab0(ba0(x1))))))	(9)
    ab#0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))	→	ab#0(ba0(x1))	(8)

    1.1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [ab0(x1)]	=	1 · x1
    [ba0(x1)]	=	1 · x1
    [aa1(x1)]	=	1 · x1
    [aa0(x1)]	=	1 · x1
    [ab#0(x1)]	=	1 · x1

    together with the usable rule

    ab0(ba0(aa1(aa0(aa1(aa0(aa1(aa0(x1))))))))

    →

    aa1(aa0(aa1(aa0(aa1(aa0(ab0(ba0(aa1(aa0(ab0(ba0(x1))))))))))))

    (12)

    (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

    1.1.1.1.1.1.2.1 P is empty

    There are no pairs anymore.

  1.1.1.1.2 Switch to Innermost Termination

  The TRS does not have overlaps with the pairs and is locally confluent:

  20

  Hence, it suffices to show innermost termination in the following.

  1.1.1.1.2.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

  [ab#(x1)]	=	0 -∞ -∞ + -∞ 0 -∞ -∞ -∞ -∞ -∞ -∞ -∞ · x1
  [ba(x1)]	=	-∞ -∞ 0 + 0 -∞ -∞ 0 -∞ -∞ 0 0 0 · x1
  [aa(x1)]	=	-∞ -∞ 0 + 0 0 -∞ 0 0 0 1 0 0 · x1
  [ab(x1)]	=	-∞ -∞ -∞ + 0 0 -∞ 0 0 -∞ 0 0 -∞ · x1

  the pairs

  ab#(ba(aa(aa(aa(aa(aa(aa(x1))))))))	→	ab#(ba(x1))	(5)
  ab#(ba(aa(aa(aa(aa(aa(aa(x1))))))))	→	ab#(ba(aa(aa(ab(ba(x1))))))	(4)

  could be deleted.

  1.1.1.1.2.1.1 P is empty

  There are no pairs anymore.