YES We show the termination of the TRS R: active(U11(tt(),N)) -> mark(N) active(U21(tt(),M,N)) -> mark(s(plus(N,M))) active(and(tt(),X)) -> mark(X) active(isNat(|0|())) -> mark(tt()) active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) active(isNat(s(V1))) -> mark(isNat(V1)) active(plus(N,|0|())) -> mark(U11(isNat(N),N)) active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) mark(s(X)) -> active(s(mark(X))) mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) mark(and(X1,X2)) -> active(and(mark(X1),X2)) mark(isNat(X)) -> active(isNat(X)) mark(|0|()) -> active(|0|()) U11(mark(X1),X2) -> U11(X1,X2) U11(X1,mark(X2)) -> U11(X1,X2) U11(active(X1),X2) -> U11(X1,X2) U11(X1,active(X2)) -> U11(X1,X2) U21(mark(X1),X2,X3) -> U21(X1,X2,X3) U21(X1,mark(X2),X3) -> U21(X1,X2,X3) U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) U21(active(X1),X2,X3) -> U21(X1,X2,X3) U21(X1,active(X2),X3) -> U21(X1,X2,X3) U21(X1,X2,active(X3)) -> U21(X1,X2,X3) s(mark(X)) -> s(X) s(active(X)) -> s(X) plus(mark(X1),X2) -> plus(X1,X2) plus(X1,mark(X2)) -> plus(X1,X2) plus(active(X1),X2) -> plus(X1,X2) plus(X1,active(X2)) -> plus(X1,X2) and(mark(X1),X2) -> and(X1,X2) and(X1,mark(X2)) -> and(X1,X2) and(active(X1),X2) -> and(X1,X2) and(X1,active(X2)) -> and(X1,X2) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),N)) -> mark#(N) p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M))) p3: active#(U21(tt(),M,N)) -> s#(plus(N,M)) p4: active#(U21(tt(),M,N)) -> plus#(N,M) p5: active#(and(tt(),X)) -> mark#(X) p6: active#(isNat(|0|())) -> mark#(tt()) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p8: active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2)) p9: active#(isNat(plus(V1,V2))) -> isNat#(V1) p10: active#(isNat(plus(V1,V2))) -> isNat#(V2) p11: active#(isNat(s(V1))) -> mark#(isNat(V1)) p12: active#(isNat(s(V1))) -> isNat#(V1) p13: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p14: active#(plus(N,|0|())) -> U11#(isNat(N),N) p15: active#(plus(N,|0|())) -> isNat#(N) p16: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p17: active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N) p18: active#(plus(N,s(M))) -> and#(isNat(M),isNat(N)) p19: active#(plus(N,s(M))) -> isNat#(M) p20: active#(plus(N,s(M))) -> isNat#(N) p21: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p22: mark#(U11(X1,X2)) -> U11#(mark(X1),X2) p23: mark#(U11(X1,X2)) -> mark#(X1) p24: mark#(tt()) -> active#(tt()) p25: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p26: mark#(U21(X1,X2,X3)) -> U21#(mark(X1),X2,X3) p27: mark#(U21(X1,X2,X3)) -> mark#(X1) p28: mark#(s(X)) -> active#(s(mark(X))) p29: mark#(s(X)) -> s#(mark(X)) p30: mark#(s(X)) -> mark#(X) p31: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p32: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) p33: mark#(plus(X1,X2)) -> mark#(X1) p34: mark#(plus(X1,X2)) -> mark#(X2) p35: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p36: mark#(and(X1,X2)) -> and#(mark(X1),X2) p37: mark#(and(X1,X2)) -> mark#(X1) p38: mark#(isNat(X)) -> active#(isNat(X)) p39: mark#(|0|()) -> active#(|0|()) p40: U11#(mark(X1),X2) -> U11#(X1,X2) p41: U11#(X1,mark(X2)) -> U11#(X1,X2) p42: U11#(active(X1),X2) -> U11#(X1,X2) p43: U11#(X1,active(X2)) -> U11#(X1,X2) p44: U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3) p45: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) p46: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p47: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p48: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p49: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3) p50: s#(mark(X)) -> s#(X) p51: s#(active(X)) -> s#(X) p52: plus#(mark(X1),X2) -> plus#(X1,X2) p53: plus#(X1,mark(X2)) -> plus#(X1,X2) p54: plus#(active(X1),X2) -> plus#(X1,X2) p55: plus#(X1,active(X2)) -> plus#(X1,X2) p56: and#(mark(X1),X2) -> and#(X1,X2) p57: and#(X1,mark(X2)) -> and#(X1,X2) p58: and#(active(X1),X2) -> and#(X1,X2) p59: and#(X1,active(X2)) -> and#(X1,X2) p60: isNat#(mark(X)) -> isNat#(X) p61: isNat#(active(X)) -> isNat#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p5, p7, p11, p13, p16, p21, p23, p25, p27, p28, p30, p31, p33, p34, p35, p37, p38} {p50, p51} {p52, p53, p54, p55} {p56, p57, p58, p59} {p60, p61} {p40, p41, p42, p43} {p44, p45, p46, p47, p48, p49} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),N)) -> mark#(N) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p4: mark#(and(X1,X2)) -> mark#(X1) p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p6: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p7: mark#(plus(X1,X2)) -> mark#(X2) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p10: active#(isNat(s(V1))) -> mark#(isNat(V1)) p11: mark#(s(X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(mark(X))) p13: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p14: mark#(U21(X1,X2,X3)) -> mark#(X1) p15: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p16: active#(and(tt(),X)) -> mark#(X) p17: mark#(U11(X1,X2)) -> mark#(X1) p18: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p19: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M))) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 + (1,1) U11_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (10,8) tt_A() = (9,0) mark#_A(x1) = ((0,1),(0,1)) x1 + (1,1) isNat_A(x1) = ((1,1),(0,0)) x1 + (2,0) plus_A(x1,x2) = x1 + ((0,1),(1,1)) x2 + (5,5) s_A(x1) = x1 + (3,4) U21_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((0,1),(1,1)) x2 + x3 + (8,10) and_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (2,0) mark_A(x1) = x1 |0|_A() = (10,6) active_A(x1) = x1 precedence: active# = U11 = tt = mark# = isNat = plus = s = U21 = and = mark = |0| = active partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(isNat) = [] pi(plus) = [] pi(s) = [] pi(U21) = [] pi(and) = [] pi(mark) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p19 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),N)) -> mark#(N) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p4: mark#(and(X1,X2)) -> mark#(X1) p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p6: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p7: mark#(plus(X1,X2)) -> mark#(X2) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p10: active#(isNat(s(V1))) -> mark#(isNat(V1)) p11: mark#(s(X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(mark(X))) p13: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p14: mark#(U21(X1,X2,X3)) -> mark#(X1) p15: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p16: active#(and(tt(),X)) -> mark#(X) p17: mark#(U11(X1,X2)) -> mark#(X1) p18: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),N)) -> mark#(N) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(and(tt(),X)) -> mark#(X) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p6: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p7: mark#(U21(X1,X2,X3)) -> mark#(X1) p8: mark#(s(X)) -> active#(s(mark(X))) p9: active#(isNat(s(V1))) -> mark#(isNat(V1)) p10: mark#(s(X)) -> mark#(X) p11: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p12: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p13: mark#(plus(X1,X2)) -> mark#(X1) p14: mark#(plus(X1,X2)) -> mark#(X2) p15: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p16: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p17: mark#(and(X1,X2)) -> mark#(X1) p18: mark#(isNat(X)) -> active#(isNat(X)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((0,1),(0,0)) x1 U11_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + (3,3) tt_A() = (0,0) mark#_A(x1) = ((1,0),(0,0)) x1 mark_A(x1) = ((0,0),(1,1)) x1 and_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 U21_A(x1,x2,x3) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (6,2) isNat_A(x1) = (0,0) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 s_A(x1) = ((1,1),(0,0)) x1 + (4,3) |0|_A() = (4,1) active_A(x1) = ((0,0),(1,1)) x1 precedence: active# = U11 = tt = mark# = mark = and = U21 = isNat = plus = s = |0| = active partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(mark) = [] pi(and) = [] pi(U21) = [] pi(isNat) = [] pi(plus) = [] pi(s) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(U21(X1,X2,X3)) -> mark#(X1) p7: mark#(s(X)) -> active#(s(mark(X))) p8: active#(isNat(s(V1))) -> mark#(isNat(V1)) p9: mark#(s(X)) -> mark#(X) p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p11: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p12: mark#(plus(X1,X2)) -> mark#(X1) p13: mark#(plus(X1,X2)) -> mark#(X2) p14: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p15: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p16: mark#(and(X1,X2)) -> mark#(X1) p17: mark#(isNat(X)) -> active#(isNat(X)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p3: mark#(isNat(X)) -> active#(isNat(X)) p4: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p7: active#(isNat(s(V1))) -> mark#(isNat(V1)) p8: mark#(plus(X1,X2)) -> mark#(X2) p9: mark#(plus(X1,X2)) -> mark#(X1) p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p11: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p12: mark#(s(X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(mark(X))) p14: active#(and(tt(),X)) -> mark#(X) p15: mark#(U21(X1,X2,X3)) -> mark#(X1) p16: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p17: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = (4,2) U11_A(x1,x2) = ((0,0),(1,1)) x2 + (1,1) active#_A(x1) = ((1,0),(0,0)) x1 + (1,2) mark_A(x1) = ((1,1),(0,0)) x1 plus_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (3,13) s_A(x1) = ((0,0),(1,1)) x1 + (1,0) U21_A(x1,x2,x3) = ((0,0),(1,1)) x2 + ((0,0),(1,1)) x3 + (0,17) and_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (3,1) isNat_A(x1) = ((0,0),(1,1)) x1 + (3,3) |0|_A() = (0,0) tt_A() = (0,0) active_A(x1) = ((1,1),(0,0)) x1 precedence: mark# = active# = U21 > plus = and > U11 > |0| > tt > mark = s = isNat = active partial status: pi(mark#) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(plus) = [] pi(s) = [] pi(U21) = [] pi(and) = [] pi(isNat) = [] pi(|0|) = [] pi(tt) = [] pi(active) = [] The next rules are strictly ordered: p13 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p3: mark#(isNat(X)) -> active#(isNat(X)) p4: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p7: active#(isNat(s(V1))) -> mark#(isNat(V1)) p8: mark#(plus(X1,X2)) -> mark#(X2) p9: mark#(plus(X1,X2)) -> mark#(X1) p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p11: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p12: mark#(s(X)) -> mark#(X) p13: active#(and(tt(),X)) -> mark#(X) p14: mark#(U21(X1,X2,X3)) -> mark#(X1) p15: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p16: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(U21(X1,X2,X3)) -> mark#(X1) p7: mark#(s(X)) -> mark#(X) p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p9: active#(isNat(s(V1))) -> mark#(isNat(V1)) p10: mark#(plus(X1,X2)) -> mark#(X1) p11: mark#(plus(X1,X2)) -> mark#(X2) p12: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p13: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N)) p14: mark#(and(X1,X2)) -> mark#(X1) p15: mark#(isNat(X)) -> active#(isNat(X)) p16: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,1)) x1 + (3,3) U11_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,0)) x2 + (0,1) active#_A(x1) = ((0,1),(0,1)) x1 + (3,3) mark_A(x1) = ((1,1),(0,0)) x1 and_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 tt_A() = (0,0) U21_A(x1,x2,x3) = ((0,0),(1,1)) x1 + ((1,1),(0,0)) x2 + ((1,1),(1,1)) x3 + (1,2) isNat_A(x1) = (0,0) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 s_A(x1) = ((0,0),(1,1)) x1 + (2,1) |0|_A() = (4,4) active_A(x1) = ((1,1),(0,0)) x1 precedence: s > and > |0| > mark# = active# = isNat > plus > U11 = mark = active > tt > U21 partial status: pi(mark#) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(and) = [] pi(tt) = [] pi(U21) = [] pi(isNat) = [] pi(plus) = [] pi(s) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p13 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(U21(X1,X2,X3)) -> mark#(X1) p7: mark#(s(X)) -> mark#(X) p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p9: active#(isNat(s(V1))) -> mark#(isNat(V1)) p10: mark#(plus(X1,X2)) -> mark#(X1) p11: mark#(plus(X1,X2)) -> mark#(X2) p12: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p13: mark#(and(X1,X2)) -> mark#(X1) p14: mark#(isNat(X)) -> active#(isNat(X)) p15: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p3: mark#(isNat(X)) -> active#(isNat(X)) p4: active#(isNat(s(V1))) -> mark#(isNat(V1)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p8: mark#(plus(X1,X2)) -> mark#(X2) p9: mark#(plus(X1,X2)) -> mark#(X1) p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p11: active#(and(tt(),X)) -> mark#(X) p12: mark#(s(X)) -> mark#(X) p13: mark#(U21(X1,X2,X3)) -> mark#(X1) p14: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p15: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = (6,0) U11_A(x1,x2) = (2,4) active#_A(x1) = ((1,0),(0,0)) x1 + (1,0) mark_A(x1) = (3,3) plus_A(x1,x2) = (5,0) s_A(x1) = (3,1) U21_A(x1,x2,x3) = (4,3) and_A(x1,x2) = (5,2) isNat_A(x1) = (5,3) tt_A() = (7,4) active_A(x1) = (3,3) |0|_A() = (1,3) precedence: mark# = active# = mark = s = U21 = tt = active > U11 > isNat > plus > and > |0| partial status: pi(mark#) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(plus) = [] pi(s) = [] pi(U21) = [] pi(and) = [] pi(isNat) = [] pi(tt) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(isNat(s(V1))) -> mark#(isNat(V1)) p4: mark#(and(X1,X2)) -> mark#(X1) p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p6: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p7: mark#(plus(X1,X2)) -> mark#(X2) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p10: active#(and(tt(),X)) -> mark#(X) p11: mark#(s(X)) -> mark#(X) p12: mark#(U21(X1,X2,X3)) -> mark#(X1) p13: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p14: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p2: mark#(U11(X1,X2)) -> mark#(X1) p3: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3)) p4: active#(and(tt(),X)) -> mark#(X) p5: mark#(U21(X1,X2,X3)) -> mark#(X1) p6: mark#(s(X)) -> mark#(X) p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p8: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p9: mark#(plus(X1,X2)) -> mark#(X1) p10: mark#(plus(X1,X2)) -> mark#(X2) p11: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p12: active#(isNat(s(V1))) -> mark#(isNat(V1)) p13: mark#(and(X1,X2)) -> mark#(X1) p14: mark#(isNat(X)) -> active#(isNat(X)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 plus_A(x1,x2) = (7,5) s_A(x1) = (9,1) mark#_A(x1) = (5,5) U21_A(x1,x2,x3) = (8,2) and_A(x1,x2) = (10,5) isNat_A(x1) = (6,5) U11_A(x1,x2) = (11,2) mark_A(x1) = (8,2) tt_A() = (10,4) active_A(x1) = (8,2) |0|_A() = (11,3) precedence: U21 > tt > and > U11 = mark = active > |0| > active# = plus = mark# = isNat > s partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U21) = [] pi(and) = [] pi(isNat) = [] pi(U11) = [] pi(mark) = [] pi(tt) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p2: mark#(U11(X1,X2)) -> mark#(X1) p3: active#(and(tt(),X)) -> mark#(X) p4: mark#(U21(X1,X2,X3)) -> mark#(X1) p5: mark#(s(X)) -> mark#(X) p6: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> mark#(X2) p10: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p11: active#(isNat(s(V1))) -> mark#(isNat(V1)) p12: mark#(and(X1,X2)) -> mark#(X1) p13: mark#(isNat(X)) -> active#(isNat(X)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(isNat(s(V1))) -> mark#(isNat(V1)) p4: mark#(and(X1,X2)) -> mark#(X1) p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p6: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p7: mark#(plus(X1,X2)) -> mark#(X2) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p10: active#(and(tt(),X)) -> mark#(X) p11: mark#(s(X)) -> mark#(X) p12: mark#(U21(X1,X2,X3)) -> mark#(X1) p13: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((1,1),(0,0)) x1 + (2,5) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,2) s_A(x1) = ((0,1),(1,0)) x1 + (1,1) mark#_A(x1) = ((1,1),(0,0)) x1 + (2,5) U21_A(x1,x2,x3) = x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (4,4) and_A(x1,x2) = x1 + ((1,1),(1,1)) x2 isNat_A(x1) = (0,0) mark_A(x1) = x1 tt_A() = (0,0) U11_A(x1,x2) = x1 + x2 + (3,4) active_A(x1) = x1 |0|_A() = (1,1) precedence: U11 > active# = plus = mark# = U21 = isNat = mark = active = |0| > s > tt > and partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U21) = [] pi(and) = [] pi(isNat) = [] pi(mark) = [] pi(tt) = [] pi(U11) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p9: active#(and(tt(),X)) -> mark#(X) p10: mark#(s(X)) -> mark#(X) p11: mark#(U21(X1,X2,X3)) -> mark#(X1) p12: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> mark#(X1) p5: mark#(s(X)) -> mark#(X) p6: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p8: mark#(plus(X1,X2)) -> mark#(X1) p9: mark#(plus(X1,X2)) -> mark#(X2) p10: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p11: active#(isNat(s(V1))) -> mark#(isNat(V1)) p12: mark#(and(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(1,1)) x1 + (2,6) isNat_A(x1) = (0,0) active#_A(x1) = x1 + (2,6) and_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,1),(1,1)) x2 tt_A() = (0,0) U11_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,1)) x2 + (6,2) U21_A(x1,x2,x3) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (9,7) s_A(x1) = ((0,0),(1,1)) x1 + (1,6) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,6) mark_A(x1) = ((0,0),(1,1)) x1 active_A(x1) = ((0,0),(1,1)) x1 |0|_A() = (1,1) precedence: isNat = tt = U11 = U21 = plus = mark = active > |0| > mark# = active# = and > s partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(and) = [] pi(tt) = [] pi(U11) = [] pi(U21) = [] pi(s) = [] pi(plus) = [] pi(mark) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> mark#(X1) p5: mark#(s(X)) -> mark#(X) p6: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(plus(X1,X2)) -> mark#(X2) p9: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p10: active#(isNat(s(V1))) -> mark#(isNat(V1)) p11: mark#(and(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(s(X)) -> mark#(X) p9: mark#(U21(X1,X2,X3)) -> mark#(X1) p10: mark#(U11(X1,X2)) -> mark#(X1) p11: active#(and(tt(),X)) -> mark#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 + (1,2) isNat_A(x1) = (0,1) active#_A(x1) = x1 + (1,1) s_A(x1) = ((1,0),(0,0)) x1 + (2,2) and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (0,1) mark_A(x1) = ((1,0),(0,0)) x1 + (0,4) plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (2,2) U21_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (4,3) U11_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (3,3) tt_A() = (0,0) active_A(x1) = ((1,0),(0,0)) x1 + (0,4) |0|_A() = (2,4) precedence: mark# = active# = U21 = U11 > and = plus > tt = |0| > isNat = s = mark = active partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(and) = [] pi(mark) = [] pi(plus) = [] pi(U21) = [] pi(U11) = [] pi(tt) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p8 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(U21(X1,X2,X3)) -> mark#(X1) p9: mark#(U11(X1,X2)) -> mark#(X1) p10: active#(and(tt(),X)) -> mark#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U21(X1,X2,X3)) -> mark#(X1) p5: mark#(plus(X1,X2)) -> mark#(X1) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p8: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p9: mark#(and(X1,X2)) -> mark#(X1) p10: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 + (0,4) isNat_A(x1) = (0,0) active#_A(x1) = ((1,0),(0,0)) x1 + (0,4) and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (0,4) tt_A() = (0,3) U11_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (1,4) U21_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x3 + (2,2) plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,1) mark_A(x1) = ((1,0),(0,0)) x1 + (0,2) s_A(x1) = (1,1) active_A(x1) = ((1,0),(0,0)) x1 + (0,2) |0|_A() = (2,1) precedence: U21 = s > and = U11 = mark = active > mark# = active# > isNat = tt = plus > |0| partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(and) = [] pi(tt) = [] pi(U11) = [] pi(U21) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(and(tt(),X)) -> mark#(X) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X1) p5: mark#(plus(X1,X2)) -> mark#(X2) p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p8: mark#(and(X1,X2)) -> mark#(X1) p9: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(U11(X1,X2)) -> mark#(X1) p9: active#(and(tt(),X)) -> mark#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,1),(1,1)) x1 + (2,0) isNat_A(x1) = x1 + (7,2) active#_A(x1) = ((1,1),(1,1)) x1 + (1,0) s_A(x1) = x1 + (21,12) and_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,1)) x2 + (2,1) mark_A(x1) = x1 plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,1)) x2 + (35,32) U11_A(x1,x2) = ((0,1),(1,0)) x1 + x2 + (3,1) tt_A() = (0,0) active_A(x1) = x1 U21_A(x1,x2,x3) = ((1,1),(0,1)) x2 + ((1,1),(1,1)) x3 + (57,44) |0|_A() = (6,1) precedence: and = plus > mark# = isNat = active# = U11 = U21 > mark = tt = active = |0| > s partial status: pi(mark#) = [1] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(and) = [] pi(mark) = [] pi(plus) = [] pi(U11) = [] pi(tt) = [] pi(active) = [] pi(U21) = [] pi(|0|) = [] The next rules are strictly ordered: p9 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p6: mark#(plus(X1,X2)) -> mark#(X2) p7: mark#(plus(X1,X2)) -> mark#(X1) p8: mark#(U11(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X1) p5: mark#(plus(X1,X2)) -> mark#(X2) p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) p7: active#(isNat(s(V1))) -> mark#(isNat(V1)) p8: mark#(and(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = (3,0) isNat_A(x1) = (7,2) active#_A(x1) = ((0,1),(0,0)) x1 + (1,0) plus_A(x1,x2) = (7,4) and_A(x1,x2) = (7,1) U11_A(x1,x2) = (7,3) mark_A(x1) = (15,3) s_A(x1) = (4,2) active_A(x1) = ((1,0),(0,0)) x1 + (8,3) tt_A() = (5,3) U21_A(x1,x2,x3) = (7,0) |0|_A() = (6,2) precedence: plus = U11 > and = U21 > s > mark = active = tt > mark# = isNat = active# > |0| partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(plus) = [] pi(and) = [] pi(U11) = [] pi(mark) = [] pi(s) = [] pi(active) = [] pi(tt) = [] pi(U21) = [] pi(|0|) = [] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X1) p5: mark#(plus(X1,X2)) -> mark#(X2) p6: active#(isNat(s(V1))) -> mark#(isNat(V1)) p7: mark#(and(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X2) p5: mark#(plus(X1,X2)) -> mark#(X1) p6: mark#(U11(X1,X2)) -> mark#(X1) p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 isNat_A(x1) = ((1,0),(0,0)) x1 + (0,1) active#_A(x1) = ((1,0),(0,0)) x1 s_A(x1) = ((1,1),(1,1)) x1 + (1,1) and_A(x1,x2) = ((1,0),(0,0)) x1 + (2,2) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,0)) x2 + (3,2) U11_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,1),(1,1)) x2 + (1,1) mark_A(x1) = ((1,0),(1,1)) x1 + (1,0) active_A(x1) = ((1,1),(1,1)) x1 + (3,0) precedence: s > isNat > mark = active > mark# = active# = and = plus = U11 partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(and) = [] pi(plus) = [1] pi(U11) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X2) p5: mark#(plus(X1,X2)) -> mark#(X1) p6: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X2) p5: mark#(and(X1,X2)) -> mark#(X1) p6: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,0)) x1 + (1,2) isNat_A(x1) = (5,2) active#_A(x1) = (3,2) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 + (4,2) and_A(x1,x2) = ((0,0),(0,1)) x1 + (2,0) s_A(x1) = ((1,0),(0,0)) x1 + (1,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(0,1)) x1 + (5,1) precedence: plus > and = s = mark > isNat > active > mark# = active# partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(plus) = [] pi(and) = [] pi(s) = [] pi(mark) = [] pi(active) = [1] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) p3: mark#(plus(X1,X2)) -> mark#(X2) p4: mark#(and(X1,X2)) -> mark#(X1) p5: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X2) p5: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2))) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r33, r34, r35, r36, r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 + (4,1) isNat_A(x1) = ((1,0),(1,0)) x1 + (0,2) active#_A(x1) = ((0,1),(0,0)) x1 + (1,1) s_A(x1) = ((1,0),(1,1)) x1 + (5,1) and_A(x1,x2) = ((1,0),(0,0)) x1 + (1,6) plus_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,0)) x2 + (3,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: mark# = isNat = active# = s = and = plus > mark = active partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(and) = [] pi(plus) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(plus(X1,X2)) -> mark#(X2) p4: mark#(and(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,1)) x1 + (3,3) isNat_A(x1) = ((1,1),(1,1)) x1 + (2,2) active#_A(x1) = ((0,1),(1,0)) x1 + (2,1) s_A(x1) = x1 + (1,1) plus_A(x1,x2) = ((1,1),(0,0)) x1 + ((0,0),(0,1)) x2 + (1,0) and_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(0,0)) x2 + (4,3) mark_A(x1) = ((0,0),(1,1)) x1 + (3,2) active_A(x1) = ((0,0),(1,1)) x1 + (3,2) precedence: isNat = s = mark > active > plus > mark# = active# > and partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(plus) = [] pi(and) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) p3: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = x1 + (3,3) isNat_A(x1) = ((1,1),(0,1)) x1 + (6,5) active#_A(x1) = ((0,1),(0,1)) x1 + (2,1) s_A(x1) = ((0,0),(1,1)) x1 + (4,3) plus_A(x1,x2) = ((0,1),(1,1)) x1 + x2 + (1,3) mark_A(x1) = ((0,0),(1,1)) x1 + (1,1) active_A(x1) = ((0,0),(1,1)) x1 + (7,5) precedence: s > mark# = active# > plus = active > isNat > mark partial status: pi(mark#) = [] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(plus) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) p2: active#(isNat(s(V1))) -> mark#(isNat(V1)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of r37, r38 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = x1 + (2,0) isNat_A(x1) = ((1,0),(1,0)) x1 + (4,2) active#_A(x1) = ((0,1),(0,1)) x1 + (1,0) s_A(x1) = ((1,0),(0,0)) x1 + (5,1) mark_A(x1) = ((1,0),(0,0)) x1 + (0,1) active_A(x1) = ((1,0),(0,0)) x1 + (0,1) precedence: active# > mark# = isNat = s > active > mark partial status: pi(mark#) = [1] pi(isNat) = [] pi(active#) = [] pi(s) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isNat(X)) -> active#(isNat(X)) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: s#(mark(X)) -> s#(X) p2: s#(active(X)) -> s#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: s#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: s# = mark = active partial status: pi(s#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: s#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: s# = active partial status: pi(s#) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: plus#(mark(X1),X2) -> plus#(X1,X2) p2: plus#(X1,active(X2)) -> plus#(X1,X2) p3: plus#(active(X1),X2) -> plus#(X1,X2) p4: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: plus#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: plus# = mark = active partial status: pi(plus#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,active(X2)) -> plus#(X1,X2) p2: plus#(active(X1),X2) -> plus#(X1,X2) p3: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,active(X2)) -> plus#(X1,X2) p2: plus#(X1,mark(X2)) -> plus#(X1,X2) p3: plus#(active(X1),X2) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: plus#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: plus# > active = mark partial status: pi(plus#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,active(X2)) -> plus#(X1,X2) p2: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,active(X2)) -> plus#(X1,X2) p2: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: plus#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: plus# = active = mark partial status: pi(plus#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: plus#(X1,mark(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: plus#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: plus# = mark partial status: pi(plus#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: and#(mark(X1),X2) -> and#(X1,X2) p2: and#(X1,active(X2)) -> and#(X1,X2) p3: and#(active(X1),X2) -> and#(X1,X2) p4: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: and#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: and# = mark = active partial status: pi(and#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,active(X2)) -> and#(X1,X2) p2: and#(active(X1),X2) -> and#(X1,X2) p3: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,active(X2)) -> and#(X1,X2) p2: and#(X1,mark(X2)) -> and#(X1,X2) p3: and#(active(X1),X2) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: and#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: and# > active = mark partial status: pi(and#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,active(X2)) -> and#(X1,X2) p2: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,active(X2)) -> and#(X1,X2) p2: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: and#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: and# = active = mark partial status: pi(and#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: and#(X1,mark(X2)) -> and#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: and#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: and# = mark partial status: pi(and#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNat#(mark(X)) -> isNat#(X) p2: isNat#(active(X)) -> isNat#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNat#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: isNat# = mark = active partial status: pi(isNat#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNat#(active(X)) -> isNat#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNat#(active(X)) -> isNat#(X) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNat#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: isNat# = active partial status: pi(isNat#) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(mark(X1),X2) -> U11#(X1,X2) p2: U11#(X1,active(X2)) -> U11#(X1,X2) p3: U11#(active(X1),X2) -> U11#(X1,X2) p4: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: U11# = mark = active partial status: pi(U11#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,active(X2)) -> U11#(X1,X2) p2: U11#(active(X1),X2) -> U11#(X1,X2) p3: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,active(X2)) -> U11#(X1,X2) p2: U11#(X1,mark(X2)) -> U11#(X1,X2) p3: U11#(active(X1),X2) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: U11# > active = mark partial status: pi(U11#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,active(X2)) -> U11#(X1,X2) p2: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,active(X2)) -> U11#(X1,X2) p2: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: U11# = active = mark partial status: pi(U11#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(X1,mark(X2)) -> U11#(X1,X2) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: U11# = mark partial status: pi(U11#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3) p2: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3) p3: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p4: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p5: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p6: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: U21# = mark = active partial status: pi(U21#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3) p2: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p3: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p4: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p5: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3) p2: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) p3: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p4: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p5: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: U21# = active = mark partial status: pi(U21#) = [] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) p2: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p3: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p4: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3) p2: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p3: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p4: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(0,1)) x2 + ((1,1),(1,1)) x3 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: U21# = mark = active partial status: pi(U21#) = [3] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p2: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) p3: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3) p2: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p3: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) mark_A(x1) = (1,1) precedence: U21# = active > mark partial status: pi(U21#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p2: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3) p2: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = x2 + ((1,0),(1,1)) x3 + (2,2) mark_A(x1) = ((1,1),(0,0)) x1 + (1,1) active_A(x1) = (1,1) precedence: U21# = mark = active partial status: pi(U21#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3) and R consists of: r1: active(U11(tt(),N)) -> mark(N) r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M))) r3: active(and(tt(),X)) -> mark(X) r4: active(isNat(|0|())) -> mark(tt()) r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2))) r6: active(isNat(s(V1))) -> mark(isNat(V1)) r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N)) r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N)) r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r10: mark(tt()) -> active(tt()) r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) r12: mark(s(X)) -> active(s(mark(X))) r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r14: mark(and(X1,X2)) -> active(and(mark(X1),X2)) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(|0|()) -> active(|0|()) r17: U11(mark(X1),X2) -> U11(X1,X2) r18: U11(X1,mark(X2)) -> U11(X1,X2) r19: U11(active(X1),X2) -> U11(X1,X2) r20: U11(X1,active(X2)) -> U11(X1,X2) r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3) r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3) r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) r27: s(mark(X)) -> s(X) r28: s(active(X)) -> s(X) r29: plus(mark(X1),X2) -> plus(X1,X2) r30: plus(X1,mark(X2)) -> plus(X1,X2) r31: plus(active(X1),X2) -> plus(X1,X2) r32: plus(X1,active(X2)) -> plus(X1,X2) r33: and(mark(X1),X2) -> and(X1,X2) r34: and(X1,mark(X2)) -> and(X1,X2) r35: and(active(X1),X2) -> and(X1,X2) r36: and(X1,active(X2)) -> and(X1,X2) r37: isNat(mark(X)) -> isNat(X) r38: isNat(active(X)) -> isNat(X) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2,x3) = ((1,1),(0,1)) x1 + (0,1) active_A(x1) = ((1,1),(0,1)) x1 + (1,1) precedence: U21# = active partial status: pi(U21#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.