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

linear polynomial interpretations on N:

  NUMERAL_A(x1) = x1
  NUMERAL#_A(x1) = 1
  0_A = 1
  0#_A = 10
  BIT0_A(x1) = 1
  BIT0#_A(x1) = 5
  SUC_A(x1) = x1 + 2
  SUC#_A(x1) = 6
  BIT1_A(x1) = 3
  BIT1#_A(x1) = 4
  PRE_A(x1) = 1
  PRE#_A(x1) = 11
  if_A(x1,x2,x3) = 0
  if#_A(x1,x2,x3) = x2
  eq_A(x1,x2) = 1
  eq#_A(x1,x2) = 4
  plus_A(x1,x2) = 3
  plus#_A(x1,x2) = 7
  mult_A(x1,x2) = 3
  mult#_A(x1,x2) = 8
  exp_A(x1,x2) = x1 + x2 + 1
  exp#_A(x1,x2) = x1 + 8
  EVEN_A(x1) = 0
  EVEN#_A(x1) = 2
  T_A = 0
  T#_A = 1
  F_A = 0
  F#_A = 3
  ODD_A(x1) = 0
  ODD#_A(x1) = 4
  le_A(x1,x2) = 1
  le#_A(x1,x2) = 0
  lt_A(x1,x2) = 1
  lt#_A(x1,x2) = 0
  ge_A(x1,x2) = 0
  ge#_A(x1,x2) = 0
  gt_A(x1,x2) = 0
  gt#_A(x1,x2) = 0
  minus_A(x1,x2) = x1 + 1
  minus#_A(x1,x2) = 12

precedence:

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