Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t000)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(0) = 1 weight(0) = 1
prec(1) = 11 weight(1) = 9
prec(2) = 9 weight(2) = 2
prec(3) = 8 weight(3) = 7
prec(4) = 3 weight(4) = 11
prec(5) = 10 weight(5) = 8
prec(6) = 0 weight(6) = 12
prec(7) = 7 weight(7) = 17
prec(8) = 4 weight(8) = 22
prec(9) = 5 weight(9) = 27
prec(+) = 6 weight(+) = 8
prec(c) = 2 weight(c) = 9
all of the following rules can be deleted.

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

1.1 R is empty

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