by Hakusan
The rewrite relation of the following TRS is considered.
| NUMERAL(0) | → | 0 |
| BIT0(0) | → | 0 |
| SUC(NUMERAL(n)) | → | NUMERAL(SUC(n)) |
| SUC(0) | → | BIT1(0) |
| SUC(BIT0(n)) | → | BIT1(n) |
| SUC(BIT1(n)) | → | BIT0(SUC(n)) |
| PRE(NUMERAL(n)) | → | NUMERAL(PRE(n)) |
| PRE(0) | → | 0 |
| PRE(BIT0(n)) | → | if(eq(n,0),0,BIT1(PRE(n))) |
| PRE(BIT1(n)) | → | BIT0(n) |
| plus(NUMERAL(m),NUMERAL(n)) | → | NUMERAL(plus(m,n)) |
| plus(0,0) | → | 0 |
| plus(0,BIT0(n)) | → | BIT0(n) |
| plus(0,BIT1(n)) | → | BIT1(n) |
| plus(BIT0(n),0) | → | BIT0(n) |
| plus(BIT1(n),0) | → | BIT1(n) |
| plus(BIT0(m),BIT0(n)) | → | BIT0(plus(m,n)) |
| plus(BIT0(m),BIT1(n)) | → | BIT1(plus(m,n)) |
| plus(BIT1(m),BIT0(n)) | → | BIT1(plus(m,n)) |
| plus(BIT1(m),BIT1(n)) | → | BIT0(SUC(plus(m,n))) |
| mult(NUMERAL(m),NUMERAL(n)) | → | NUMERAL(mult(m,n)) |
| mult(0,0) | → | 0 |
| mult(0,BIT0(n)) | → | 0 |
| mult(0,BIT1(n)) | → | 0 |
| mult(BIT0(n),0) | → | 0 |
| mult(BIT1(n),0) | → | 0 |
| mult(BIT0(m),BIT0(n)) | → | BIT0(BIT0(mult(m,n))) |
| mult(BIT0(m),BIT1(n)) | → | plus(BIT0(m),BIT0(BIT0(mult(m,n)))) |
| mult(BIT1(m),BIT0(n)) | → | plus(BIT0(n),BIT0(BIT0(mult(m,n)))) |
| mult(BIT1(m),BIT1(n)) | → | plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n)))) |
| exp(NUMERAL(m),NUMERAL(n)) | → | NUMERAL(exp(m,n)) |
| exp(0,0) | → | BIT1(0) |
| exp(BIT0(m),0) | → | BIT1(0) |
| exp(BIT1(m),0) | → | BIT1(0) |
| exp(0,BIT0(n)) | → | mult(exp(0,n),exp(0,n)) |
| exp(BIT0(m),BIT0(n)) | → | mult(exp(BIT0(m),n),exp(BIT0(m),n)) |
| exp(BIT1(m),BIT0(n)) | → | mult(exp(BIT1(m),n),exp(BIT1(m),n)) |
| exp(0,BIT1(n)) | → | 0 |
| exp(BIT0(m),BIT1(n)) | → | mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)) |
| exp(BIT1(m),BIT1(n)) | → | mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n)) |
| EVEN(NUMERAL(n)) | → | EVEN(n) |
| EVEN(0) | → | T |
| EVEN(BIT0(n)) | → | T |
| EVEN(BIT1(n)) | → | F |
| ODD(NUMERAL(n)) | → | ODD(n) |
| ODD(0) | → | F |
| ODD(BIT0(n)) | → | F |
| ODD(BIT1(n)) | → | T |
| eq(NUMERAL(m),NUMERAL(n)) | → | eq(m,n) |
| eq(0,0) | → | T |
| eq(BIT0(n),0) | → | eq(n,0) |
| eq(BIT1(n),0) | → | F |
| eq(0,BIT0(n)) | → | eq(0,n) |
| eq(0,BIT1(n)) | → | F |
| eq(BIT0(m),BIT0(n)) | → | eq(m,n) |
| eq(BIT0(m),BIT1(n)) | → | F |
| eq(BIT1(m),BIT0(n)) | → | F |
| eq(BIT1(m),BIT1(n)) | → | eq(m,n) |
| le(NUMERAL(m),NUMERAL(n)) | → | le(m,n) |
| le(0,0) | → | T |
| le(BIT0(n),0) | → | le(n,0) |
| le(BIT1(n),0) | → | F |
| le(0,BIT0(n)) | → | T |
| le(0,BIT1(n)) | → | T |
| le(BIT0(m),BIT0(n)) | → | le(m,n) |
| le(BIT0(m),BIT1(n)) | → | le(m,n) |
| le(BIT1(m),BIT0(n)) | → | lt(m,n) |
| le(BIT1(m),BIT1(n)) | → | le(m,n) |
| lt(NUMERAL(m),NUMERAL(n)) | → | lt(m,n) |
| lt(0,0) | → | F |
| lt(BIT0(n),0) | → | F |
| lt(BIT1(n),0) | → | F |
| lt(0,BIT0(n)) | → | lt(0,n) |
| lt(0,BIT1(n)) | → | T |
| lt(BIT0(m),BIT0(n)) | → | lt(m,n) |
| lt(BIT0(m),BIT1(n)) | → | le(m,n) |
| lt(BIT1(m),BIT0(n)) | → | lt(m,n) |
| lt(BIT1(m),BIT1(n)) | → | lt(m,n) |
| ge(NUMERAL(n),NUMERAL(m)) | → | ge(n,m) |
| ge(0,0) | → | T |
| ge(0,BIT0(n)) | → | ge(0,n) |
| ge(0,BIT1(n)) | → | F |
| ge(BIT0(n),0) | → | T |
| ge(BIT1(n),0) | → | T |
| ge(BIT0(n),BIT0(m)) | → | ge(n,m) |
| ge(BIT1(n),BIT0(m)) | → | ge(n,m) |
| ge(BIT0(n),BIT1(m)) | → | gt(n,m) |
| ge(BIT1(n),BIT1(m)) | → | ge(n,m) |
| gt(NUMERAL(n),NUMERAL(m)) | → | gt(n,m) |
| gt(0,0) | → | F |
| gt(0,BIT0(n)) | → | F |
| gt(0,BIT1(n)) | → | F |
| gt(BIT0(n),0) | → | gt(n,0) |
| gt(BIT1(n),0) | → | T |
| gt(BIT0(n),BIT0(m)) | → | gt(n,m) |
| gt(BIT1(n),BIT0(m)) | → | ge(n,m) |
| gt(BIT0(n),BIT1(m)) | → | gt(n,m) |
| gt(BIT1(n),BIT1(m)) | → | gt(n,m) |
| minus(NUMERAL(m),NUMERAL(n)) | → | NUMERAL(minus(m,n)) |
| minus(0,0) | → | 0 |
| minus(0,BIT0(n)) | → | 0 |
| minus(0,BIT1(n)) | → | 0 |
| minus(BIT0(n),0) | → | BIT0(n) |
| minus(BIT1(n),0) | → | BIT1(n) |
| minus(BIT0(m),BIT0(n)) | → | BIT0(minus(m,n)) |
| minus(BIT0(m),BIT1(n)) | → | PRE(BIT0(minus(m,n))) |
| minus(BIT1(m),BIT0(n)) | → | if(le(n,m),BIT1(minus(m,n)),0) |
| minus(BIT1(m),BIT1(n)) | → | BIT0(minus(m,n)) |
| t0 | = | plus(NUMERAL(0),NUMERAL(y2)) |
| →1 | plus(0,NUMERAL(y2)) | |
| = | t1 |
| t0 | = | plus(NUMERAL(0),NUMERAL(y2)) |
| →ε | NUMERAL(plus(0,y2)) | |
| = | t1 |
Hakusan