NO
(ignored inputs)COMMENT submitted by: Cezary Kaliszyk
Rewrite 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)) ]
Apply Direct Methods...
Inner CPs:
   [ SUC(0) = NUMERAL(SUC(0)),
     SUC(0) = BIT1(0),
     PRE(0) = NUMERAL(PRE(0)),
     PRE(0) = if(eq(0,0),0,BIT1(PRE(0))),
     plus(0,NUMERAL(?n_6)) = NUMERAL(plus(0,?n_6)),
     plus(NUMERAL(?m_6),0) = NUMERAL(plus(?m_6,0)),
     plus(0,0) = BIT0(0),
     plus(0,0) = BIT0(0),
     plus(0,BIT0(?n_11)) = BIT0(plus(0,?n_11)),
     plus(BIT0(?m_11),0) = BIT0(plus(?m_11,0)),
     plus(0,BIT1(?n_12)) = BIT1(plus(0,?n_12)),
     plus(BIT1(?m_13),0) = BIT1(plus(?m_13,0)),
     mult(0,NUMERAL(?n_15)) = NUMERAL(mult(0,?n_15)),
     mult(NUMERAL(?m_15),0) = NUMERAL(mult(?m_15,0)),
     mult(0,0) = 0,
     mult(0,0) = 0,
     mult(0,BIT0(?n_20)) = BIT0(BIT0(mult(0,?n_20))),
     mult(BIT0(?m_20),0) = BIT0(BIT0(mult(?m_20,0))),
     mult(0,BIT1(?n_21)) = plus(BIT0(0),BIT0(BIT0(mult(0,?n_21)))),
     mult(BIT1(?m_22),0) = plus(BIT0(0),BIT0(BIT0(mult(?m_22,0)))),
     exp(0,NUMERAL(?n_24)) = NUMERAL(exp(0,?n_24)),
     exp(NUMERAL(?m_24),0) = NUMERAL(exp(?m_24,0)),
     exp(0,0) = BIT1(0),
     exp(0,0) = mult(exp(0,0),exp(0,0)),
     exp(0,BIT0(?n_28)) = mult(exp(BIT0(0),?n_28),exp(BIT0(0),?n_28)),
     exp(BIT0(?m_28),0) = mult(exp(BIT0(?m_28),0),exp(BIT0(?m_28),0)),
     exp(BIT1(?m_29),0) = mult(exp(BIT1(?m_29),0),exp(BIT1(?m_29),0)),
     exp(0,BIT1(?n_31)) = mult(mult(BIT0(0),exp(BIT0(0),?n_31)),exp(BIT0(0),?n_31)),
     EVEN(0) = EVEN(0),
     EVEN(0) = T,
     ODD(0) = ODD(0),
     ODD(0) = F,
     eq(0,NUMERAL(?n_39)) = eq(0,?n_39),
     eq(NUMERAL(?m_39),0) = eq(?m_39,0),
     eq(0,0) = eq(0,0),
     eq(0,0) = eq(0,0),
     eq(0,BIT0(?n_44)) = eq(0,?n_44),
     eq(BIT0(?m_44),0) = eq(?m_44,0),
     eq(0,BIT1(?n_45)) = F,
     eq(BIT1(?m_46),0) = F,
     le(0,NUMERAL(?n_48)) = le(0,?n_48),
     le(NUMERAL(?m_48),0) = le(?m_48,0),
     le(0,0) = le(0,0),
     le(0,0) = T,
     le(0,BIT0(?n_53)) = le(0,?n_53),
     le(BIT0(?m_53),0) = le(?m_53,0),
     le(0,BIT1(?n_54)) = le(0,?n_54),
     le(BIT1(?m_55),0) = lt(?m_55,0),
     lt(0,NUMERAL(?n_57)) = lt(0,?n_57),
     lt(NUMERAL(?m_57),0) = lt(?m_57,0),
     lt(0,0) = F,
     lt(0,0) = lt(0,0),
     lt(0,BIT0(?n_62)) = lt(0,?n_62),
     lt(BIT0(?m_62),0) = lt(?m_62,0),
     lt(0,BIT1(?n_63)) = le(0,?n_63),
     lt(BIT1(?m_64),0) = lt(?m_64,0),
     ge(0,NUMERAL(?m_66)) = ge(0,?m_66),
     ge(NUMERAL(?n_66),0) = ge(?n_66,0),
     ge(0,0) = ge(0,0),
     ge(0,0) = T,
     ge(0,BIT0(?m_71)) = ge(0,?m_71),
     ge(BIT0(?n_71),0) = ge(?n_71,0),
     ge(BIT1(?n_72),0) = ge(?n_72,0),
     ge(0,BIT1(?m_73)) = gt(0,?m_73),
     gt(0,NUMERAL(?m_75)) = gt(0,?m_75),
     gt(NUMERAL(?n_75),0) = gt(?n_75,0),
     gt(0,0) = F,
     gt(0,0) = gt(0,0),
     gt(0,BIT0(?m_80)) = gt(0,?m_80),
     gt(BIT0(?n_80),0) = gt(?n_80,0),
     gt(BIT1(?n_81),0) = ge(?n_81,0),
     gt(0,BIT1(?m_82)) = gt(0,?m_82),
     minus(0,NUMERAL(?n_84)) = NUMERAL(minus(0,?n_84)),
     minus(NUMERAL(?m_84),0) = NUMERAL(minus(?m_84,0)),
     minus(0,0) = 0,
     minus(0,0) = BIT0(0),
     minus(0,BIT0(?n_89)) = BIT0(minus(0,?n_89)),
     minus(BIT0(?m_89),0) = BIT0(minus(?m_89,0)),
     minus(0,BIT1(?n_90)) = PRE(BIT0(minus(0,?n_90))),
     minus(BIT1(?m_91),0) = if(le(0,?m_91),BIT1(minus(?m_91,0)),0) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Combined result: not CR
1124.trs: Success(not CR)
(39 msec.)