NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty m n) (REPLACEMENT-MAP (BIT0 1) (EVEN 1) (NUMERAL 1) (ODD 1) (PRE 1) (SUC 1) (eq 1, 2) (exp 1, 2) (ge 1, 2) (gt 1, 2) (le 1, 2) (lt 1, 2) (minus 1, 2) (mult 1, 2) (plus 1, 2) (0) (BIT1 1) (F) (T) (fSNonEmpty) (if 1, 2, 3) ) (RULES BIT0(0) -> 0 EVEN(BIT0(n)) -> T EVEN(NUMERAL(n)) -> EVEN(n) EVEN(0) -> T EVEN(BIT1(n)) -> F NUMERAL(0) -> 0 ODD(BIT0(n)) -> F ODD(NUMERAL(n)) -> ODD(n) ODD(0) -> F ODD(BIT1(n)) -> T PRE(BIT0(n)) -> if(eq(n,0),0,BIT1(PRE(n))) PRE(NUMERAL(n)) -> NUMERAL(PRE(n)) PRE(0) -> 0 PRE(BIT1(n)) -> BIT0(n) SUC(BIT0(n)) -> BIT1(n) SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT1(n)) -> BIT0(SUC(n)) eq(BIT0(m),BIT0(n)) -> eq(m,n) eq(BIT0(m),BIT1(n)) -> F eq(BIT0(n),0) -> eq(n,0) eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n) eq(0,BIT0(n)) -> eq(0,n) eq(0,0) -> T eq(0,BIT1(n)) -> F eq(BIT1(m),BIT0(n)) -> F eq(BIT1(m),BIT1(n)) -> eq(m,n) eq(BIT1(n),0) -> F exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n)) exp(BIT0(m),0) -> BIT1(0) exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)) exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n)) exp(0,BIT0(n)) -> mult(exp(0,n),exp(0,n)) exp(0,0) -> BIT1(0) exp(0,BIT1(n)) -> 0 exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n)) exp(BIT1(m),0) -> BIT1(0) exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n)) ge(BIT0(n),BIT0(m)) -> ge(n,m) ge(BIT0(n),0) -> T ge(BIT0(n),BIT1(m)) -> gt(n,m) ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m) ge(0,BIT0(n)) -> ge(0,n) ge(0,0) -> T ge(0,BIT1(n)) -> F ge(BIT1(n),BIT0(m)) -> ge(n,m) ge(BIT1(n),0) -> T ge(BIT1(n),BIT1(m)) -> ge(n,m) gt(BIT0(n),BIT0(m)) -> gt(n,m) gt(BIT0(n),0) -> gt(n,0) gt(BIT0(n),BIT1(m)) -> gt(n,m) gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m) gt(0,BIT0(n)) -> F gt(0,0) -> F gt(0,BIT1(n)) -> F gt(BIT1(n),BIT0(m)) -> ge(n,m) gt(BIT1(n),0) -> T gt(BIT1(n),BIT1(m)) -> gt(n,m) le(BIT0(m),BIT0(n)) -> le(m,n) le(BIT0(m),BIT1(n)) -> le(m,n) le(BIT0(n),0) -> le(n,0) le(NUMERAL(m),NUMERAL(n)) -> le(m,n) le(0,BIT0(n)) -> T le(0,0) -> T le(0,BIT1(n)) -> T le(BIT1(m),BIT0(n)) -> lt(m,n) le(BIT1(m),BIT1(n)) -> le(m,n) le(BIT1(n),0) -> F lt(BIT0(m),BIT0(n)) -> lt(m,n) lt(BIT0(m),BIT1(n)) -> le(m,n) lt(BIT0(n),0) -> F lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n) lt(0,BIT0(n)) -> lt(0,n) lt(0,0) -> F lt(0,BIT1(n)) -> T lt(BIT1(m),BIT0(n)) -> lt(m,n) lt(BIT1(m),BIT1(n)) -> lt(m,n) lt(BIT1(n),0) -> F minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n)) minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n))) minus(BIT0(n),0) -> BIT0(n) minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n)) minus(0,BIT0(n)) -> 0 minus(0,0) -> 0 minus(0,BIT1(n)) -> 0 minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),0) minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n)) minus(BIT1(n),0) -> BIT1(n) mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n))) mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n)))) mult(BIT0(n),0) -> 0 mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n)) mult(0,BIT0(n)) -> 0 mult(0,0) -> 0 mult(0,BIT1(n)) -> 0 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)))) mult(BIT1(n),0) -> 0 plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n)) plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n)) plus(BIT0(n),0) -> BIT0(n) plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n)) plus(0,BIT0(n)) -> BIT0(n) plus(0,0) -> 0 plus(0,BIT1(n)) -> BIT1(n) plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n)) plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n))) plus(BIT1(n),0) -> BIT1(n) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty m n) (REPLACEMENT-MAP (BIT0 1) (EVEN 1) (NUMERAL 1) (ODD 1) (PRE 1) (SUC 1) (eq 1, 2) (exp 1, 2) (ge 1, 2) (gt 1, 2) (le 1, 2) (lt 1, 2) (minus 1, 2) (mult 1, 2) (plus 1, 2) (0) (BIT1 1) (F) (T) (fSNonEmpty) (if 1, 2, 3) ) (RULES BIT0(0) -> 0 EVEN(BIT0(n)) -> T EVEN(NUMERAL(n)) -> EVEN(n) EVEN(0) -> T EVEN(BIT1(n)) -> F NUMERAL(0) -> 0 ODD(BIT0(n)) -> F ODD(NUMERAL(n)) -> ODD(n) ODD(0) -> F ODD(BIT1(n)) -> T PRE(BIT0(n)) -> if(eq(n,0),0,BIT1(PRE(n))) PRE(NUMERAL(n)) -> NUMERAL(PRE(n)) PRE(0) -> 0 PRE(BIT1(n)) -> BIT0(n) SUC(BIT0(n)) -> BIT1(n) SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT1(n)) -> BIT0(SUC(n)) eq(BIT0(m),BIT0(n)) -> eq(m,n) eq(BIT0(m),BIT1(n)) -> F eq(BIT0(n),0) -> eq(n,0) eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n) eq(0,BIT0(n)) -> eq(0,n) eq(0,0) -> T eq(0,BIT1(n)) -> F eq(BIT1(m),BIT0(n)) -> F eq(BIT1(m),BIT1(n)) -> eq(m,n) eq(BIT1(n),0) -> F exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n)) exp(BIT0(m),0) -> BIT1(0) exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)) exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n)) exp(0,BIT0(n)) -> mult(exp(0,n),exp(0,n)) exp(0,0) -> BIT1(0) exp(0,BIT1(n)) -> 0 exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n)) exp(BIT1(m),0) -> BIT1(0) exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n)) ge(BIT0(n),BIT0(m)) -> ge(n,m) ge(BIT0(n),0) -> T ge(BIT0(n),BIT1(m)) -> gt(n,m) ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m) ge(0,BIT0(n)) -> ge(0,n) ge(0,0) -> T ge(0,BIT1(n)) -> F ge(BIT1(n),BIT0(m)) -> ge(n,m) ge(BIT1(n),0) -> T ge(BIT1(n),BIT1(m)) -> ge(n,m) gt(BIT0(n),BIT0(m)) -> gt(n,m) gt(BIT0(n),0) -> gt(n,0) gt(BIT0(n),BIT1(m)) -> gt(n,m) gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m) gt(0,BIT0(n)) -> F gt(0,0) -> F gt(0,BIT1(n)) -> F gt(BIT1(n),BIT0(m)) -> ge(n,m) gt(BIT1(n),0) -> T gt(BIT1(n),BIT1(m)) -> gt(n,m) le(BIT0(m),BIT0(n)) -> le(m,n) le(BIT0(m),BIT1(n)) -> le(m,n) le(BIT0(n),0) -> le(n,0) le(NUMERAL(m),NUMERAL(n)) -> le(m,n) le(0,BIT0(n)) -> T le(0,0) -> T le(0,BIT1(n)) -> T le(BIT1(m),BIT0(n)) -> lt(m,n) le(BIT1(m),BIT1(n)) -> le(m,n) le(BIT1(n),0) -> F lt(BIT0(m),BIT0(n)) -> lt(m,n) lt(BIT0(m),BIT1(n)) -> le(m,n) lt(BIT0(n),0) -> F lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n) lt(0,BIT0(n)) -> lt(0,n) lt(0,0) -> F lt(0,BIT1(n)) -> T lt(BIT1(m),BIT0(n)) -> lt(m,n) lt(BIT1(m),BIT1(n)) -> lt(m,n) lt(BIT1(n),0) -> F minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n)) minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n))) minus(BIT0(n),0) -> BIT0(n) minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n)) minus(0,BIT0(n)) -> 0 minus(0,0) -> 0 minus(0,BIT1(n)) -> 0 minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),0) minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n)) minus(BIT1(n),0) -> BIT1(n) mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n))) mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n)))) mult(BIT0(n),0) -> 0 mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n)) mult(0,BIT0(n)) -> 0 mult(0,0) -> 0 mult(0,BIT1(n)) -> 0 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)))) mult(BIT1(n),0) -> 0 plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n)) plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n)) plus(BIT0(n),0) -> BIT0(n) plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n)) plus(0,BIT0(n)) -> BIT0(n) plus(0,0) -> 0 plus(0,BIT1(n)) -> BIT1(n) plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n)) plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n))) plus(BIT1(n),0) -> BIT1(n) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: BIT0(0) -> 0 EVEN(BIT0(n)) -> T EVEN(NUMERAL(n)) -> EVEN(n) EVEN(0) -> T EVEN(BIT1(n)) -> F NUMERAL(0) -> 0 ODD(BIT0(n)) -> F ODD(NUMERAL(n)) -> ODD(n) ODD(0) -> F ODD(BIT1(n)) -> T PRE(BIT0(n)) -> if(eq(n,0),0,BIT1(PRE(n))) PRE(NUMERAL(n)) -> NUMERAL(PRE(n)) PRE(0) -> 0 PRE(BIT1(n)) -> BIT0(n) SUC(BIT0(n)) -> BIT1(n) SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT1(n)) -> BIT0(SUC(n)) eq(BIT0(m),BIT0(n)) -> eq(m,n) eq(BIT0(m),BIT1(n)) -> F eq(BIT0(n),0) -> eq(n,0) eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n) eq(0,BIT0(n)) -> eq(0,n) eq(0,0) -> T eq(0,BIT1(n)) -> F eq(BIT1(m),BIT0(n)) -> F eq(BIT1(m),BIT1(n)) -> eq(m,n) eq(BIT1(n),0) -> F exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n)) exp(BIT0(m),0) -> BIT1(0) exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)) exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n)) exp(0,BIT0(n)) -> mult(exp(0,n),exp(0,n)) exp(0,0) -> BIT1(0) exp(0,BIT1(n)) -> 0 exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n)) exp(BIT1(m),0) -> BIT1(0) exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n)) ge(BIT0(n),BIT0(m)) -> ge(n,m) ge(BIT0(n),0) -> T ge(BIT0(n),BIT1(m)) -> gt(n,m) ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m) ge(0,BIT0(n)) -> ge(0,n) ge(0,0) -> T ge(0,BIT1(n)) -> F ge(BIT1(n),BIT0(m)) -> ge(n,m) ge(BIT1(n),0) -> T ge(BIT1(n),BIT1(m)) -> ge(n,m) gt(BIT0(n),BIT0(m)) -> gt(n,m) gt(BIT0(n),0) -> gt(n,0) gt(BIT0(n),BIT1(m)) -> gt(n,m) gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m) gt(0,BIT0(n)) -> F gt(0,0) -> F gt(0,BIT1(n)) -> F gt(BIT1(n),BIT0(m)) -> ge(n,m) gt(BIT1(n),0) -> T gt(BIT1(n),BIT1(m)) -> gt(n,m) le(BIT0(m),BIT0(n)) -> le(m,n) le(BIT0(m),BIT1(n)) -> le(m,n) le(BIT0(n),0) -> le(n,0) le(NUMERAL(m),NUMERAL(n)) -> le(m,n) le(0,BIT0(n)) -> T le(0,0) -> T le(0,BIT1(n)) -> T le(BIT1(m),BIT0(n)) -> lt(m,n) le(BIT1(m),BIT1(n)) -> le(m,n) le(BIT1(n),0) -> F lt(BIT0(m),BIT0(n)) -> lt(m,n) lt(BIT0(m),BIT1(n)) -> le(m,n) lt(BIT0(n),0) -> F lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n) lt(0,BIT0(n)) -> lt(0,n) lt(0,0) -> F lt(0,BIT1(n)) -> T lt(BIT1(m),BIT0(n)) -> lt(m,n) lt(BIT1(m),BIT1(n)) -> lt(m,n) lt(BIT1(n),0) -> F minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n)) minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n))) minus(BIT0(n),0) -> BIT0(n) minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n)) minus(0,BIT0(n)) -> 0 minus(0,0) -> 0 minus(0,BIT1(n)) -> 0 minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),0) minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n)) minus(BIT1(n),0) -> BIT1(n) mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n))) mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n)))) mult(BIT0(n),0) -> 0 mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n)) mult(0,BIT0(n)) -> 0 mult(0,0) -> 0 mult(0,BIT1(n)) -> 0 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)))) mult(BIT1(n),0) -> 0 plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n)) plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n)) plus(BIT0(n),0) -> BIT0(n) plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n)) plus(0,BIT0(n)) -> BIT0(n) plus(0,0) -> 0 plus(0,BIT1(n)) -> BIT1(n) plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n)) plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n))) plus(BIT1(n),0) -> BIT1(n) -> Vars: n, n, n, n, n, n, n, n, n, n, n, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n, m, n, m, m, n, m, n, n, n, m, n, m, m, n, m, n, n, m, n, m, n, n, n, m, n, n, m, n, m, n, n, m, n, m, n, n, n, m, n, n, m, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n, m, n, m, n, n, m, n, n, n, m, n, m, n, n -> Rlps: (rule: BIT0(0) -> 0, id: 1, possubterms: BIT0(0)->[], 0->[1]) (rule: EVEN(BIT0(n)) -> T, id: 2, possubterms: EVEN(BIT0(n))->[], BIT0(n)->[1]) (rule: EVEN(NUMERAL(n)) -> EVEN(n), id: 3, possubterms: EVEN(NUMERAL(n))->[], NUMERAL(n)->[1]) (rule: EVEN(0) -> T, id: 4, possubterms: EVEN(0)->[], 0->[1]) (rule: EVEN(BIT1(n)) -> F, id: 5, possubterms: EVEN(BIT1(n))->[], BIT1(n)->[1]) (rule: NUMERAL(0) -> 0, id: 6, possubterms: NUMERAL(0)->[], 0->[1]) (rule: ODD(BIT0(n)) -> F, id: 7, possubterms: ODD(BIT0(n))->[], BIT0(n)->[1]) (rule: ODD(NUMERAL(n)) -> ODD(n), id: 8, possubterms: ODD(NUMERAL(n))->[], NUMERAL(n)->[1]) (rule: ODD(0) -> F, id: 9, possubterms: ODD(0)->[], 0->[1]) (rule: ODD(BIT1(n)) -> T, id: 10, possubterms: ODD(BIT1(n))->[], BIT1(n)->[1]) (rule: PRE(BIT0(n)) -> if(eq(n,0),0,BIT1(PRE(n))), id: 11, possubterms: PRE(BIT0(n))->[], BIT0(n)->[1]) (rule: PRE(NUMERAL(n)) -> NUMERAL(PRE(n)), id: 12, possubterms: PRE(NUMERAL(n))->[], NUMERAL(n)->[1]) (rule: PRE(0) -> 0, id: 13, possubterms: PRE(0)->[], 0->[1]) (rule: PRE(BIT1(n)) -> BIT0(n), id: 14, possubterms: PRE(BIT1(n))->[], BIT1(n)->[1]) (rule: SUC(BIT0(n)) -> BIT1(n), id: 15, possubterms: SUC(BIT0(n))->[], BIT0(n)->[1]) (rule: SUC(NUMERAL(n)) -> NUMERAL(SUC(n)), id: 16, possubterms: SUC(NUMERAL(n))->[], NUMERAL(n)->[1]) (rule: SUC(0) -> BIT1(0), id: 17, possubterms: SUC(0)->[], 0->[1]) (rule: SUC(BIT1(n)) -> BIT0(SUC(n)), id: 18, possubterms: SUC(BIT1(n))->[], BIT1(n)->[1]) (rule: eq(BIT0(m),BIT0(n)) -> eq(m,n), id: 19, possubterms: eq(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: eq(BIT0(m),BIT1(n)) -> F, id: 20, possubterms: eq(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: eq(BIT0(n),0) -> eq(n,0), id: 21, possubterms: eq(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n), id: 22, possubterms: eq(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: eq(0,BIT0(n)) -> eq(0,n), id: 23, possubterms: eq(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: eq(0,0) -> T, id: 24, possubterms: eq(0,0)->[], 0->[1], 0->[2]) (rule: eq(0,BIT1(n)) -> F, id: 25, possubterms: eq(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: eq(BIT1(m),BIT0(n)) -> F, id: 26, possubterms: eq(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: eq(BIT1(m),BIT1(n)) -> eq(m,n), id: 27, possubterms: eq(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: eq(BIT1(n),0) -> F, id: 28, possubterms: eq(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n)), id: 29, possubterms: exp(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: exp(BIT0(m),0) -> BIT1(0), id: 30, possubterms: exp(BIT0(m),0)->[], BIT0(m)->[1], 0->[2]) (rule: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)), id: 31, possubterms: exp(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n)), id: 32, possubterms: exp(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: exp(0,BIT0(n)) -> mult(exp(0,n),exp(0,n)), id: 33, possubterms: exp(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: exp(0,0) -> BIT1(0), id: 34, possubterms: exp(0,0)->[], 0->[1], 0->[2]) (rule: exp(0,BIT1(n)) -> 0, id: 35, possubterms: exp(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n)), id: 36, possubterms: exp(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: exp(BIT1(m),0) -> BIT1(0), id: 37, possubterms: exp(BIT1(m),0)->[], BIT1(m)->[1], 0->[2]) (rule: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n)), id: 38, possubterms: exp(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: ge(BIT0(n),BIT0(m)) -> ge(n,m), id: 39, possubterms: ge(BIT0(n),BIT0(m))->[], BIT0(n)->[1], BIT0(m)->[2]) (rule: ge(BIT0(n),0) -> T, id: 40, possubterms: ge(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: ge(BIT0(n),BIT1(m)) -> gt(n,m), id: 41, possubterms: ge(BIT0(n),BIT1(m))->[], BIT0(n)->[1], BIT1(m)->[2]) (rule: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m), id: 42, possubterms: ge(NUMERAL(n),NUMERAL(m))->[], NUMERAL(n)->[1], NUMERAL(m)->[2]) (rule: ge(0,BIT0(n)) -> ge(0,n), id: 43, possubterms: ge(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: ge(0,0) -> T, id: 44, possubterms: ge(0,0)->[], 0->[1], 0->[2]) (rule: ge(0,BIT1(n)) -> F, id: 45, possubterms: ge(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: ge(BIT1(n),BIT0(m)) -> ge(n,m), id: 46, possubterms: ge(BIT1(n),BIT0(m))->[], BIT1(n)->[1], BIT0(m)->[2]) (rule: ge(BIT1(n),0) -> T, id: 47, possubterms: ge(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: ge(BIT1(n),BIT1(m)) -> ge(n,m), id: 48, possubterms: ge(BIT1(n),BIT1(m))->[], BIT1(n)->[1], BIT1(m)->[2]) (rule: gt(BIT0(n),BIT0(m)) -> gt(n,m), id: 49, possubterms: gt(BIT0(n),BIT0(m))->[], BIT0(n)->[1], BIT0(m)->[2]) (rule: gt(BIT0(n),0) -> gt(n,0), id: 50, possubterms: gt(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: gt(BIT0(n),BIT1(m)) -> gt(n,m), id: 51, possubterms: gt(BIT0(n),BIT1(m))->[], BIT0(n)->[1], BIT1(m)->[2]) (rule: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m), id: 52, possubterms: gt(NUMERAL(n),NUMERAL(m))->[], NUMERAL(n)->[1], NUMERAL(m)->[2]) (rule: gt(0,BIT0(n)) -> F, id: 53, possubterms: gt(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: gt(0,0) -> F, id: 54, possubterms: gt(0,0)->[], 0->[1], 0->[2]) (rule: gt(0,BIT1(n)) -> F, id: 55, possubterms: gt(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: gt(BIT1(n),BIT0(m)) -> ge(n,m), id: 56, possubterms: gt(BIT1(n),BIT0(m))->[], BIT1(n)->[1], BIT0(m)->[2]) (rule: gt(BIT1(n),0) -> T, id: 57, possubterms: gt(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: gt(BIT1(n),BIT1(m)) -> gt(n,m), id: 58, possubterms: gt(BIT1(n),BIT1(m))->[], BIT1(n)->[1], BIT1(m)->[2]) (rule: le(BIT0(m),BIT0(n)) -> le(m,n), id: 59, possubterms: le(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: le(BIT0(m),BIT1(n)) -> le(m,n), id: 60, possubterms: le(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: le(BIT0(n),0) -> le(n,0), id: 61, possubterms: le(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: le(NUMERAL(m),NUMERAL(n)) -> le(m,n), id: 62, possubterms: le(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: le(0,BIT0(n)) -> T, id: 63, possubterms: le(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: le(0,0) -> T, id: 64, possubterms: le(0,0)->[], 0->[1], 0->[2]) (rule: le(0,BIT1(n)) -> T, id: 65, possubterms: le(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: le(BIT1(m),BIT0(n)) -> lt(m,n), id: 66, possubterms: le(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: le(BIT1(m),BIT1(n)) -> le(m,n), id: 67, possubterms: le(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: le(BIT1(n),0) -> F, id: 68, possubterms: le(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: lt(BIT0(m),BIT0(n)) -> lt(m,n), id: 69, possubterms: lt(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: lt(BIT0(m),BIT1(n)) -> le(m,n), id: 70, possubterms: lt(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: lt(BIT0(n),0) -> F, id: 71, possubterms: lt(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n), id: 72, possubterms: lt(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: lt(0,BIT0(n)) -> lt(0,n), id: 73, possubterms: lt(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: lt(0,0) -> F, id: 74, possubterms: lt(0,0)->[], 0->[1], 0->[2]) (rule: lt(0,BIT1(n)) -> T, id: 75, possubterms: lt(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: lt(BIT1(m),BIT0(n)) -> lt(m,n), id: 76, possubterms: lt(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: lt(BIT1(m),BIT1(n)) -> lt(m,n), id: 77, possubterms: lt(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: lt(BIT1(n),0) -> F, id: 78, possubterms: lt(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n)), id: 79, possubterms: minus(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n))), id: 80, possubterms: minus(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: minus(BIT0(n),0) -> BIT0(n), id: 81, possubterms: minus(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n)), id: 82, possubterms: minus(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: minus(0,BIT0(n)) -> 0, id: 83, possubterms: minus(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: minus(0,0) -> 0, id: 84, possubterms: minus(0,0)->[], 0->[1], 0->[2]) (rule: minus(0,BIT1(n)) -> 0, id: 85, possubterms: minus(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),0), id: 86, possubterms: minus(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n)), id: 87, possubterms: minus(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: minus(BIT1(n),0) -> BIT1(n), id: 88, possubterms: minus(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n))), id: 89, possubterms: mult(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n)))), id: 90, possubterms: mult(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: mult(BIT0(n),0) -> 0, id: 91, possubterms: mult(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n)), id: 92, possubterms: mult(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: mult(0,BIT0(n)) -> 0, id: 93, possubterms: mult(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: mult(0,0) -> 0, id: 94, possubterms: mult(0,0)->[], 0->[1], 0->[2]) (rule: mult(0,BIT1(n)) -> 0, id: 95, possubterms: mult(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n)))), id: 96, possubterms: mult(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n)))), id: 97, possubterms: mult(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: mult(BIT1(n),0) -> 0, id: 98, possubterms: mult(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) (rule: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n)), id: 99, possubterms: plus(BIT0(m),BIT0(n))->[], BIT0(m)->[1], BIT0(n)->[2]) (rule: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n)), id: 100, possubterms: plus(BIT0(m),BIT1(n))->[], BIT0(m)->[1], BIT1(n)->[2]) (rule: plus(BIT0(n),0) -> BIT0(n), id: 101, possubterms: plus(BIT0(n),0)->[], BIT0(n)->[1], 0->[2]) (rule: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n)), id: 102, possubterms: plus(NUMERAL(m),NUMERAL(n))->[], NUMERAL(m)->[1], NUMERAL(n)->[2]) (rule: plus(0,BIT0(n)) -> BIT0(n), id: 103, possubterms: plus(0,BIT0(n))->[], 0->[1], BIT0(n)->[2]) (rule: plus(0,0) -> 0, id: 104, possubterms: plus(0,0)->[], 0->[1], 0->[2]) (rule: plus(0,BIT1(n)) -> BIT1(n), id: 105, possubterms: plus(0,BIT1(n))->[], 0->[1], BIT1(n)->[2]) (rule: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n)), id: 106, possubterms: plus(BIT1(m),BIT0(n))->[], BIT1(m)->[1], BIT0(n)->[2]) (rule: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n))), id: 107, possubterms: plus(BIT1(m),BIT1(n))->[], BIT1(m)->[1], BIT1(n)->[2]) (rule: plus(BIT1(n),0) -> BIT1(n), id: 108, possubterms: plus(BIT1(n),0)->[], BIT1(n)->[1], 0->[2]) -> Unifications: (R2 unifies with R1 at p: [1], l: EVEN(BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: T, r': 0) (R3 unifies with R6 at p: [1], l: EVEN(NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: EVEN(n), r': 0) (R7 unifies with R1 at p: [1], l: ODD(BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: F, r': 0) (R8 unifies with R6 at p: [1], l: ODD(NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: ODD(n), r': 0) (R11 unifies with R1 at p: [1], l: PRE(BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: if(eq(n,0),0,BIT1(PRE(n))), r': 0) (R12 unifies with R6 at p: [1], l: PRE(NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(PRE(n)), r': 0) (R15 unifies with R1 at p: [1], l: SUC(BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT1(n), r': 0) (R16 unifies with R6 at p: [1], l: SUC(NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(SUC(n)), r': 0) (R19 unifies with R1 at p: [1], l: eq(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: eq(m,n), r': 0) (R19 unifies with R1 at p: [2], l: eq(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: eq(m,n), r': 0) (R20 unifies with R1 at p: [1], l: eq(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: F, r': 0) (R21 unifies with R1 at p: [1], l: eq(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: eq(n,0), r': 0) (R22 unifies with R6 at p: [1], l: eq(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: eq(m,n), r': 0) (R22 unifies with R6 at p: [2], l: eq(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: eq(m,n), r': 0) (R23 unifies with R1 at p: [2], l: eq(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: eq(0,n), r': 0) (R26 unifies with R1 at p: [2], l: eq(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: F, r': 0) (R29 unifies with R1 at p: [1], l: exp(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: mult(exp(BIT0(m),n),exp(BIT0(m),n)), r': 0) (R29 unifies with R1 at p: [2], l: exp(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: mult(exp(BIT0(m),n),exp(BIT0(m),n)), r': 0) (R30 unifies with R1 at p: [1], l: exp(BIT0(m),0), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: BIT1(0), r': 0) (R31 unifies with R1 at p: [1], l: exp(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n)), r': 0) (R32 unifies with R6 at p: [1], l: exp(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: NUMERAL(exp(m,n)), r': 0) (R32 unifies with R6 at p: [2], l: exp(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(exp(m,n)), r': 0) (R33 unifies with R1 at p: [2], l: exp(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: mult(exp(0,n),exp(0,n)), r': 0) (R36 unifies with R1 at p: [2], l: exp(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: mult(exp(BIT1(m),n),exp(BIT1(m),n)), r': 0) (R39 unifies with R1 at p: [1], l: ge(BIT0(n),BIT0(m)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: ge(n,m), r': 0) (R39 unifies with R1 at p: [2], l: ge(BIT0(n),BIT0(m)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: ge(n,m), r': 0) (R40 unifies with R1 at p: [1], l: ge(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: T, r': 0) (R41 unifies with R1 at p: [1], l: ge(BIT0(n),BIT1(m)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: gt(n,m), r': 0) (R42 unifies with R6 at p: [1], l: ge(NUMERAL(n),NUMERAL(m)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: ge(n,m), r': 0) (R42 unifies with R6 at p: [2], l: ge(NUMERAL(n),NUMERAL(m)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: ge(n,m), r': 0) (R43 unifies with R1 at p: [2], l: ge(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: ge(0,n), r': 0) (R46 unifies with R1 at p: [2], l: ge(BIT1(n),BIT0(m)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: ge(n,m), r': 0) (R49 unifies with R1 at p: [1], l: gt(BIT0(n),BIT0(m)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: gt(n,m), r': 0) (R49 unifies with R1 at p: [2], l: gt(BIT0(n),BIT0(m)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: gt(n,m), r': 0) (R50 unifies with R1 at p: [1], l: gt(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: gt(n,0), r': 0) (R51 unifies with R1 at p: [1], l: gt(BIT0(n),BIT1(m)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: gt(n,m), r': 0) (R52 unifies with R6 at p: [1], l: gt(NUMERAL(n),NUMERAL(m)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: gt(n,m), r': 0) (R52 unifies with R6 at p: [2], l: gt(NUMERAL(n),NUMERAL(m)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: gt(n,m), r': 0) (R53 unifies with R1 at p: [2], l: gt(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: F, r': 0) (R56 unifies with R1 at p: [2], l: gt(BIT1(n),BIT0(m)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: ge(n,m), r': 0) (R59 unifies with R1 at p: [1], l: le(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: le(m,n), r': 0) (R59 unifies with R1 at p: [2], l: le(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: le(m,n), r': 0) (R60 unifies with R1 at p: [1], l: le(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: le(m,n), r': 0) (R61 unifies with R1 at p: [1], l: le(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: le(n,0), r': 0) (R62 unifies with R6 at p: [1], l: le(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: le(m,n), r': 0) (R62 unifies with R6 at p: [2], l: le(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: le(m,n), r': 0) (R63 unifies with R1 at p: [2], l: le(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: T, r': 0) (R66 unifies with R1 at p: [2], l: le(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: lt(m,n), r': 0) (R69 unifies with R1 at p: [1], l: lt(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: lt(m,n), r': 0) (R69 unifies with R1 at p: [2], l: lt(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: lt(m,n), r': 0) (R70 unifies with R1 at p: [1], l: lt(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: le(m,n), r': 0) (R71 unifies with R1 at p: [1], l: lt(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: F, r': 0) (R72 unifies with R6 at p: [1], l: lt(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: lt(m,n), r': 0) (R72 unifies with R6 at p: [2], l: lt(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: lt(m,n), r': 0) (R73 unifies with R1 at p: [2], l: lt(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: lt(0,n), r': 0) (R76 unifies with R1 at p: [2], l: lt(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: lt(m,n), r': 0) (R79 unifies with R1 at p: [1], l: minus(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: BIT0(minus(m,n)), r': 0) (R79 unifies with R1 at p: [2], l: minus(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(minus(m,n)), r': 0) (R80 unifies with R1 at p: [1], l: minus(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: PRE(BIT0(minus(m,n))), r': 0) (R81 unifies with R1 at p: [1], l: minus(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(n), r': 0) (R82 unifies with R6 at p: [1], l: minus(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: NUMERAL(minus(m,n)), r': 0) (R82 unifies with R6 at p: [2], l: minus(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(minus(m,n)), r': 0) (R83 unifies with R1 at p: [2], l: minus(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: 0, r': 0) (R86 unifies with R1 at p: [2], l: minus(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: if(le(n,m),BIT1(minus(m,n)),0), r': 0) (R89 unifies with R1 at p: [1], l: mult(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: BIT0(BIT0(mult(m,n))), r': 0) (R89 unifies with R1 at p: [2], l: mult(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(BIT0(mult(m,n))), r': 0) (R90 unifies with R1 at p: [1], l: mult(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: plus(BIT0(m),BIT0(BIT0(mult(m,n)))), r': 0) (R91 unifies with R1 at p: [1], l: mult(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: 0, r': 0) (R92 unifies with R6 at p: [1], l: mult(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: NUMERAL(mult(m,n)), r': 0) (R92 unifies with R6 at p: [2], l: mult(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(mult(m,n)), r': 0) (R93 unifies with R1 at p: [2], l: mult(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: 0, r': 0) (R96 unifies with R1 at p: [2], l: mult(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: plus(BIT0(n),BIT0(BIT0(mult(m,n)))), r': 0) (R99 unifies with R1 at p: [1], l: plus(BIT0(m),BIT0(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: BIT0(plus(m,n)), r': 0) (R99 unifies with R1 at p: [2], l: plus(BIT0(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(plus(m,n)), r': 0) (R100 unifies with R1 at p: [1], l: plus(BIT0(m),BIT1(n)), lp: BIT0(m), sig: {m -> 0}, l': BIT0(0), r: BIT1(plus(m,n)), r': 0) (R101 unifies with R1 at p: [1], l: plus(BIT0(n),0), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(n), r': 0) (R102 unifies with R6 at p: [1], l: plus(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(m), sig: {m -> 0}, l': NUMERAL(0), r: NUMERAL(plus(m,n)), r': 0) (R102 unifies with R6 at p: [2], l: plus(NUMERAL(m),NUMERAL(n)), lp: NUMERAL(n), sig: {n -> 0}, l': NUMERAL(0), r: NUMERAL(plus(m,n)), r': 0) (R103 unifies with R1 at p: [2], l: plus(0,BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT0(n), r': 0) (R106 unifies with R1 at p: [2], l: plus(BIT1(m),BIT0(n)), lp: BIT0(n), sig: {n -> 0}, l': BIT0(0), r: BIT1(plus(m,n)), r': 0) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Trivial, Not overlay, Proper, NW0, N7 => Not trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Trivial, Not overlay, Proper, NW0, N16 => Not trivial, Not overlay, Proper, NW0, N17 => Not trivial, Not overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 => Not trivial, Not overlay, Proper, NW0, N21 => Not trivial, Not overlay, Proper, NW0, N22 => Not trivial, Not overlay, Proper, NW0, N23 => Not trivial, Not overlay, Proper, NW0, N24 => Not trivial, Not overlay, Proper, NW0, N25 => Not trivial, Not overlay, Proper, NW0, N26 => Not trivial, Not overlay, Proper, NW0, N27 => Not trivial, Not overlay, Proper, NW0, N28 => Not trivial, Not overlay, Proper, NW0, N29 => Not trivial, Not overlay, Proper, NW0, N30 => Not trivial, Not overlay, Proper, NW0, N31 => Not trivial, Not overlay, Proper, NW0, N32 => Not trivial, Not overlay, Proper, NW0, N33 => Not trivial, Not overlay, Proper, NW0, N34 => Not trivial, Not overlay, Proper, NW0, N35 => Not trivial, Not overlay, Proper, NW0, N36 => Not trivial, Not overlay, Proper, NW0, N37 => Not trivial, Not overlay, Proper, NW0, N38 => Not trivial, Not overlay, Proper, NW0, N39 => Not trivial, Not overlay, Proper, NW0, N40 => Not trivial, Not overlay, Proper, NW0, N41 => Not trivial, Not overlay, Proper, NW0, N42 => Not trivial, Not overlay, Proper, NW0, N43 => Not trivial, Not overlay, Proper, NW0, N44 => Not trivial, Not overlay, Proper, NW0, N45 => Not trivial, Not overlay, Proper, NW0, N46 => Trivial, Not overlay, Proper, NW0, N47 => Trivial, Not overlay, Proper, NW0, N48 => Not trivial, Not overlay, Proper, NW0, N49 => Not trivial, Not overlay, Proper, NW0, N50 => Not trivial, Not overlay, Proper, NW0, N51 => Not trivial, Not overlay, Proper, NW0, N52 => Not trivial, Not overlay, Proper, NW0, N53 => Not trivial, Not overlay, Proper, NW0, N54 => Trivial, Not overlay, Proper, NW0, N55 => Not trivial, Not overlay, Proper, NW0, N56 => Not trivial, Not overlay, Proper, NW0, N57 => Not trivial, Not overlay, Proper, NW0, N58 => Not trivial, Not overlay, Proper, NW0, N59 => Not trivial, Not overlay, Proper, NW0, N60 => Trivial, Not overlay, Proper, NW0, N61 => Not trivial, Not overlay, Proper, NW0, N62 => Not trivial, Not overlay, Proper, NW0, N63 => Not trivial, Not overlay, Proper, NW0, N64 => Not trivial, Not overlay, Proper, NW0, N65 => Not trivial, Not overlay, Proper, NW0, N66 => Not trivial, Not overlay, Proper, NW0, N67 => Not trivial, Not overlay, Proper, NW0, N68 => Not trivial, Not overlay, Proper, NW0, N69 => Not trivial, Not overlay, Proper, NW0, N70 => Trivial, Not overlay, Proper, NW0, N71 => Not trivial, Not overlay, Proper, NW0, N72 => Not trivial, Not overlay, Proper, NW0, N73 => Not trivial, Not overlay, Proper, NW0, N74 => Not trivial, Not overlay, Proper, NW0, N75 => Not trivial, Not overlay, Proper, NW0, N76 => Not trivial, Not overlay, Proper, NW0, N77 => Trivial, Not overlay, Proper, NW0, N78 => Not trivial, Not overlay, Proper, NW0, N79 => Not trivial, Not overlay, Proper, NW0, N80 -> Problem conclusions: Left linear, Not right linear, Not linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: No Convergence Brute Force Procedure: -> Rewritings: s: lt(BIT1(m),0) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('lt(BIT1(m),0)', D0) ID: 1 => ('F', D1, R78, P[], S{x98 -> m}), NR: 'F' t: lt(m,0) Nodes: [0] Edges: [] ID: 0 => ('lt(m,0)', D0) lt(BIT1(m),0) ->* no union *<- lt(m,0) "Not joinable" The problem is not confluent.