NO Problem: 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)) Proof: sorted: (order-sorted) 0: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() 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) 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)) 1: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)) 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) 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)) 2: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)) 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)) ----- sorts [0>3, 1>4, 2>5, 2>6, 2>7, 2>8, 3>9, 4>9, 5>9, 6>9, 7>9, 8>9, 9>10, 9>11, 9>12] sort attachment (non-strict) NUMERAL : 9 -> 9 0 : 12 BIT0 : 9 -> 9 SUC : 9 -> 9 BIT1 : 9 -> 9 PRE : 9 -> 9 if : 9 x 9 x 9 -> 9 eq : 9 x 9 -> 9 plus : 9 x 9 -> 9 mult : 9 x 9 -> 9 exp : 9 x 9 -> 9 EVEN : 3 -> 0 T : 11 F : 10 ODD : 4 -> 1 le : 9 x 9 -> 9 lt : 9 x 9 -> 9 ge : 5 x 6 -> 2 gt : 7 x 8 -> 2 minus : 9 x 9 -> 9 ----- 0: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() 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) 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)) Nonconfluence Processor: terms: plus(0(),NUMERAL(n)) *<- plus(NUMERAL(0()),NUMERAL(n)) ->* NUMERAL(plus(0(),n)) Qed 1: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)) 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) 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)) Open 2: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)) 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)) Open