Certification Problem

Input (TPDB SRS_Relative/Waldmann_19/random-195)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by matchbox @ termCOMP 2023)

1 Split

We split R in the relative problem D/R-D and R-D, where the rules D

1.1 Closure Under Flat Contexts

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

1.1.1 Closure Under Flat Contexts

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

1.1.1.1 Semantic Labeling

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

There are 567 ruless (increase limit for explicit display).

1.1.1.1.1 Rule Removal

There are 398 ruless (increase limit for explicit display).

1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.

1.2 Split

We split R in the relative problem D/R-D and R-D, where the rules D

1.2.1 Closure Under Flat Contexts

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

1.2.1.1 Closure Under Flat Contexts

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

1.2.1.1.1 Closure Under Flat Contexts

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

There are 162 ruless (increase limit for explicit display).

1.2.1.1.1.1 Semantic Labeling

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

There are 4374 ruless (increase limit for explicit display).

1.2.1.1.1.1.1 Rule Removal

There are 3780 ruless (increase limit for explicit display).

1.2.1.1.1.1.1.1 String Reversal

There are 594 ruless (increase limit for explicit display).

1.2.1.1.1.1.1.1.1 Rule Removal