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, 9}
  NUMERAL#_A(x1) = max{1, 1}
  0_A = 8
  0#_A = 8
  BIT0_A(x1) = max{9, -10}
  BIT0#_A(x1) = max{5, 12}
  SUC_A(x1) = max{9, -11}
  SUC#_A(x1) = max{23, 14}
  BIT1_A(x1) = max{8, -29}
  BIT1#_A(x1) = max{1, -1}
  PRE_A(x1) = max{9, -10}
  PRE#_A(x1) = max{2, 12}
  if_A(x1,x2,x3) = max{9, -12 + x1, 1 + x2, -10}
  if#_A(x1,x2,x3) = max{12, 12, 1, 12}
  eq_A(x1,x2) = max{1, 2, 1}
  eq#_A(x1,x2) = max{7, 1, 12}
  plus_A(x1,x2) = max{1, -29, 9}
  plus#_A(x1,x2) = max{13, -1, 24}
  mult_A(x1,x2) = max{9, 30, 8}
  mult#_A(x1,x2) = max{33, 0, 11}
  exp_A(x1,x2) = max{1, -30, 30}
  exp#_A(x1,x2) = max{2, 34, 32}
  EVEN_A(x1) = max{1, 2}
  EVEN#_A(x1) = max{10, 1}
  T_A = 2
  T#_A = 0
  F_A = 2
  F#_A = 6
  ODD_A(x1) = max{2, 1}
  ODD#_A(x1) = max{3, 2}
  le_A(x1,x2) = max{4, -16, -18}
  le#_A(x1,x2) = max{11, 9, -2}
  lt_A(x1,x2) = max{4, -18, -18}
  lt#_A(x1,x2) = max{11, 7, 10}
  ge_A(x1,x2) = max{2, 2, 2}
  ge#_A(x1,x2) = max{16, -1, 13}
  gt_A(x1,x2) = max{1, 1, 2}
  gt#_A(x1,x2) = max{16, 14, 15}
  minus_A(x1,x2) = max{9, -30, -18 + x2}
  minus#_A(x1,x2) = max{4, 12, 3}

precedence:

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