The rewrite relation of the following TRS is considered.
There are 108 ruless (increase limit for explicit display).
| prec(NUMERAL) | = | 0 | stat(NUMERAL) | = | mul | |
| prec(0) | = | 5 | stat(0) | = | mul | |
| prec(BIT0) | = | 4 | stat(BIT0) | = | lex | |
| prec(SUC) | = | 6 | stat(SUC) | = | lex | |
| prec(BIT1) | = | 1 | stat(BIT1) | = | mul | |
| prec(PRE) | = | 7 | stat(PRE) | = | lex | |
| prec(if) | = | 2 | stat(if) | = | mul | |
| prec(eq) | = | 7 | stat(eq) | = | lex | |
| prec(plus) | = | 8 | stat(plus) | = | lex | |
| prec(mult) | = | 9 | stat(mult) | = | lex | |
| prec(exp) | = | 10 | stat(exp) | = | lex | |
| prec(EVEN) | = | 5 | stat(EVEN) | = | lex | |
| prec(T) | = | 5 | stat(T) | = | mul | |
| prec(F) | = | 3 | stat(F) | = | mul | |
| prec(ODD) | = | 11 | stat(ODD) | = | lex | |
| prec(le) | = | 12 | stat(le) | = | lex | |
| prec(lt) | = | 12 | stat(lt) | = | lex | |
| prec(ge) | = | 5 | stat(ge) | = | lex | |
| prec(gt) | = | 5 | stat(gt) | = | lex | |
| prec(minus) | = | 13 | stat(minus) | = | lex |
| π(NUMERAL) | = | [1] |
| π(0) | = | [] |
| π(BIT0) | = | [1] |
| π(SUC) | = | [1] |
| π(BIT1) | = | [1] |
| π(PRE) | = | [1] |
| π(if) | = | [1,2,3] |
| π(eq) | = | [1,2] |
| π(plus) | = | [1,2] |
| π(mult) | = | [1,2] |
| π(exp) | = | [2,1] |
| π(EVEN) | = | [1] |
| π(T) | = | [] |
| π(F) | = | [] |
| π(ODD) | = | [1] |
| π(le) | = | [2,1] |
| π(lt) | = | [2,1] |
| π(ge) | = | [2,1] |
| π(gt) | = | [2,1] |
| π(minus) | = | [2,1] |
There are 108 ruless (increase limit for explicit display).
There are no rules in the TRS. Hence, it is terminating.