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 ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(c) = 0 weight(c) = 4
prec(9) = 5 weight(9) = 6
prec(8) = 8 weight(8) = 6
prec(7) = 11 weight(7) = 6
prec(6) = 6 weight(6) = 6
prec(5) = 15 weight(5) = 6
prec(4) = 13 weight(4) = 6
prec(3) = 9 weight(3) = 6
prec(2) = 1 weight(2) = 6
prec(1) = 2 weight(1) = 4
prec(+) = 4 weight(+) = 2
prec(0) = 10 weight(0) = 2
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.