NO

1 decompositions
 #0 -----------
   1: NUMERAL(0()) -> 0()
   2: BIT0(0()) -> 0()
   3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
   4: SUC(0()) -> BIT1(0())
   5: SUC(BIT0(n)) -> BIT1(n)
   6: SUC(BIT1(n)) -> BIT0(SUC(n))
   7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
   8: PRE(0()) -> 0()
   9: PRE(BIT0(n)) -> if(eq(n,0()),0(),BIT1(PRE(n)))
  10: PRE(BIT1(n)) -> BIT0(n)
  11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
  12: plus(0(),0()) -> 0()
  13: plus(0(),BIT0(n)) -> BIT0(n)
  14: plus(0(),BIT1(n)) -> BIT1(n)
  15: plus(BIT0(n),0()) -> BIT0(n)
  16: plus(BIT1(n),0()) -> BIT1(n)
  17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
  18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
  19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
  20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
  21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
  22: mult(0(),0()) -> 0()
  23: mult(0(),BIT0(n)) -> 0()
  24: mult(0(),BIT1(n)) -> 0()
  25: mult(BIT0(n),0()) -> 0()
  26: mult(BIT1(n),0()) -> 0()
  27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
  28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
  29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
  30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
  31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
  32: exp(0(),0()) -> BIT1(0())
  33: exp(BIT0(m),0()) -> BIT1(0())
  34: exp(BIT1(m),0()) -> BIT1(0())
  35: exp(0(),BIT0(n)) -> mult(exp(0(),n),exp(0(),n))
  36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
  37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
  38: exp(0(),BIT1(n)) -> 0()
  39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
  40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
  41: EVEN(NUMERAL(n)) -> EVEN(n)
  42: EVEN(0()) -> T()
  43: EVEN(BIT0(n)) -> T()
  44: EVEN(BIT1(n)) -> F()
  45: ODD(NUMERAL(n)) -> ODD(n)
  46: ODD(0()) -> F()
  47: ODD(BIT0(n)) -> F()
  48: ODD(BIT1(n)) -> T()
  49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
  50: eq(0(),0()) -> T()
  51: eq(BIT0(n),0()) -> eq(n,0())
  52: eq(BIT1(n),0()) -> F()
  53: eq(0(),BIT0(n)) -> eq(0(),n)
  54: eq(0(),BIT1(n)) -> F()
  55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
  56: eq(BIT0(m),BIT1(n)) -> F()
  57: eq(BIT1(m),BIT0(n)) -> F()
  58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
  59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
  60: le(0(),0()) -> T()
  61: le(BIT0(n),0()) -> le(n,0())
  62: le(BIT1(n),0()) -> F()
  63: le(0(),BIT0(n)) -> T()
  64: le(0(),BIT1(n)) -> T()
  65: le(BIT0(m),BIT0(n)) -> le(m,n)
  66: le(BIT0(m),BIT1(n)) -> le(m,n)
  67: le(BIT1(m),BIT0(n)) -> lt(m,n)
  68: le(BIT1(m),BIT1(n)) -> le(m,n)
  69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
  70: lt(0(),0()) -> F()
  71: lt(BIT0(n),0()) -> F()
  72: lt(BIT1(n),0()) -> F()
  73: lt(0(),BIT0(n)) -> lt(0(),n)
  74: lt(0(),BIT1(n)) -> T()
  75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
  76: lt(BIT0(m),BIT1(n)) -> le(m,n)
  77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
  78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
  79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
  80: ge(0(),0()) -> T()
  81: ge(0(),BIT0(n)) -> ge(0(),n)
  82: ge(0(),BIT1(n)) -> F()
  83: ge(BIT0(n),0()) -> T()
  84: ge(BIT1(n),0()) -> T()
  85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
  86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
  87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
  88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
  89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
  90: gt(0(),0()) -> F()
  91: gt(0(),BIT0(n)) -> F()
  92: gt(0(),BIT1(n)) -> F()
  93: gt(BIT0(n),0()) -> gt(n,0())
  94: gt(BIT1(n),0()) -> T()
  95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
  96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
  97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
  98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
  99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
  100: minus(0(),0()) -> 0()
  101: minus(0(),BIT0(n)) -> 0()
  102: minus(0(),BIT1(n)) -> 0()
  103: minus(BIT0(n),0()) -> BIT0(n)
  104: minus(BIT1(n),0()) -> BIT1(n)
  105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
  106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
  107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),0())
  108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

unjoinable peak
    BIT1(0())
*<- SUC(NUMERAL(0())) ->*
    NUMERAL(BIT1(0()))