YES

TRS:

  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))

max/plus interpretations on N:

  NUMERAL_A(x1) = max{0, x1}
  NUMERAL#_A(x1) = max{0, x1}
  0_A = 0
  0#_A = 0
  BIT0_A(x1) = max{0, x1}
  BIT0#_A(x1) = max{0, x1}
  SUC_A(x1) = max{0, x1}
  SUC#_A(x1) = max{0, x1}
  BIT1_A(x1) = max{0, x1}
  BIT1#_A(x1) = max{0, x1}
  PRE_A(x1) = max{0, x1}
  PRE#_A(x1) = max{0, x1}
  if_A(x1,x2,x3) = max{0, x1, x2, x3}
  if#_A(x1,x2,x3) = max{0, x1, x2, x3}
  eq_A(x1,x2) = max{0, x1, x2}
  eq#_A(x1,x2) = max{0, x1, x2}
  plus_A(x1,x2) = max{0, x1, x2}
  plus#_A(x1,x2) = max{0, x1, x2}
  mult_A(x1,x2) = max{0, x1, x2}
  mult#_A(x1,x2) = max{0, x1, x2}
  exp_A(x1,x2) = max{0, x1, x2}
  exp#_A(x1,x2) = max{0, x1, x2}
  EVEN_A(x1) = max{0, x1}
  EVEN#_A(x1) = max{0, x1}
  T_A = 0
  T#_A = 0
  F_A = 0
  F#_A = 0
  ODD_A(x1) = max{0, x1}
  ODD#_A(x1) = max{0, x1}
  le_A(x1,x2) = max{0, x1, x2}
  le#_A(x1,x2) = max{0, x1, x2}
  lt_A(x1,x2) = max{0, x1, x2}
  lt#_A(x1,x2) = max{0, x1, x2}
  ge_A(x1,x2) = max{0, x1, x2}
  ge#_A(x1,x2) = max{0, x1, x2}
  gt_A(x1,x2) = max{0, x1, x2}
  gt#_A(x1,x2) = max{0, x1, x2}
  minus_A(x1,x2) = max{0, x1, x2}
  minus#_A(x1,x2) = max{0, x1, x2}

precedence:

  exp > mult > plus > SUC = minus > BIT0 = PRE > if = eq > 0 > NUMERAL = BIT1 = T = F > EVEN = ODD = le = lt = ge = gt