(VAR m n)
(RULES
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))
)
(COMMENT
submitted by: Cezary Kaliszyk
)