YES We show the termination of the TRS R: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) active(U12(tt())) -> mark(tt()) active(U21(tt())) -> mark(tt()) active(U31(tt(),N)) -> mark(N) active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) active(U42(tt(),M,N)) -> mark(s(plus(N,M))) active(isNat(|0|())) -> mark(tt()) active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) active(isNat(s(V1))) -> mark(U21(isNat(V1))) active(plus(N,|0|())) -> mark(U31(isNat(N),N)) active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) mark(tt()) -> active(tt()) mark(U12(X)) -> active(U12(mark(X))) mark(isNat(X)) -> active(isNat(X)) mark(U21(X)) -> active(U21(mark(X))) mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) mark(s(X)) -> active(s(mark(X))) mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) 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) U12(mark(X)) -> U12(X) U12(active(X)) -> U12(X) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) U21(mark(X)) -> U21(X) U21(active(X)) -> U21(X) U31(mark(X1),X2) -> U31(X1,X2) U31(X1,mark(X2)) -> U31(X1,X2) U31(active(X1),X2) -> U31(X1,X2) U31(X1,active(X2)) -> U31(X1,X2) U41(mark(X1),X2,X3) -> U41(X1,X2,X3) U41(X1,mark(X2),X3) -> U41(X1,X2,X3) U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) U41(active(X1),X2,X3) -> U41(X1,X2,X3) U41(X1,active(X2),X3) -> U41(X1,X2,X3) U41(X1,X2,active(X3)) -> U41(X1,X2,X3) U42(mark(X1),X2,X3) -> U42(X1,X2,X3) U42(X1,mark(X2),X3) -> U42(X1,X2,X3) U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) U42(active(X1),X2,X3) -> U42(X1,X2,X3) U42(X1,active(X2),X3) -> U42(X1,X2,X3) U42(X1,X2,active(X3)) -> U42(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) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: active#(U11(tt(),V2)) -> U12#(isNat(V2)) p3: active#(U11(tt(),V2)) -> isNat#(V2) p4: active#(U12(tt())) -> mark#(tt()) p5: active#(U21(tt())) -> mark#(tt()) p6: active#(U31(tt(),N)) -> mark#(N) p7: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p8: active#(U41(tt(),M,N)) -> U42#(isNat(N),M,N) p9: active#(U41(tt(),M,N)) -> isNat#(N) p10: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p11: active#(U42(tt(),M,N)) -> s#(plus(N,M)) p12: active#(U42(tt(),M,N)) -> plus#(N,M) p13: active#(isNat(|0|())) -> mark#(tt()) p14: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p15: active#(isNat(plus(V1,V2))) -> U11#(isNat(V1),V2) p16: active#(isNat(plus(V1,V2))) -> isNat#(V1) p17: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p18: active#(isNat(s(V1))) -> U21#(isNat(V1)) p19: active#(isNat(s(V1))) -> isNat#(V1) p20: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p21: active#(plus(N,|0|())) -> U31#(isNat(N),N) p22: active#(plus(N,|0|())) -> isNat#(N) p23: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p24: active#(plus(N,s(M))) -> U41#(isNat(M),M,N) p25: active#(plus(N,s(M))) -> isNat#(M) p26: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p27: mark#(U11(X1,X2)) -> U11#(mark(X1),X2) p28: mark#(U11(X1,X2)) -> mark#(X1) p29: mark#(tt()) -> active#(tt()) p30: mark#(U12(X)) -> active#(U12(mark(X))) p31: mark#(U12(X)) -> U12#(mark(X)) p32: mark#(U12(X)) -> mark#(X) p33: mark#(isNat(X)) -> active#(isNat(X)) p34: mark#(U21(X)) -> active#(U21(mark(X))) p35: mark#(U21(X)) -> U21#(mark(X)) p36: mark#(U21(X)) -> mark#(X) p37: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p38: mark#(U31(X1,X2)) -> U31#(mark(X1),X2) p39: mark#(U31(X1,X2)) -> mark#(X1) p40: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p41: mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3) p42: mark#(U41(X1,X2,X3)) -> mark#(X1) p43: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p44: mark#(U42(X1,X2,X3)) -> U42#(mark(X1),X2,X3) p45: mark#(U42(X1,X2,X3)) -> mark#(X1) p46: mark#(s(X)) -> active#(s(mark(X))) p47: mark#(s(X)) -> s#(mark(X)) p48: mark#(s(X)) -> mark#(X) p49: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p50: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) p51: mark#(plus(X1,X2)) -> mark#(X1) p52: mark#(plus(X1,X2)) -> mark#(X2) p53: mark#(|0|()) -> active#(|0|()) p54: U11#(mark(X1),X2) -> U11#(X1,X2) p55: U11#(X1,mark(X2)) -> U11#(X1,X2) p56: U11#(active(X1),X2) -> U11#(X1,X2) p57: U11#(X1,active(X2)) -> U11#(X1,X2) p58: U12#(mark(X)) -> U12#(X) p59: U12#(active(X)) -> U12#(X) p60: isNat#(mark(X)) -> isNat#(X) p61: isNat#(active(X)) -> isNat#(X) p62: U21#(mark(X)) -> U21#(X) p63: U21#(active(X)) -> U21#(X) p64: U31#(mark(X1),X2) -> U31#(X1,X2) p65: U31#(X1,mark(X2)) -> U31#(X1,X2) p66: U31#(active(X1),X2) -> U31#(X1,X2) p67: U31#(X1,active(X2)) -> U31#(X1,X2) p68: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3) p69: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3) p70: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3) p71: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3) p72: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3) p73: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3) p74: U42#(mark(X1),X2,X3) -> U42#(X1,X2,X3) p75: U42#(X1,mark(X2),X3) -> U42#(X1,X2,X3) p76: U42#(X1,X2,mark(X3)) -> U42#(X1,X2,X3) p77: U42#(active(X1),X2,X3) -> U42#(X1,X2,X3) p78: U42#(X1,active(X2),X3) -> U42#(X1,X2,X3) p79: U42#(X1,X2,active(X3)) -> U42#(X1,X2,X3) p80: s#(mark(X)) -> s#(X) p81: s#(active(X)) -> s#(X) p82: plus#(mark(X1),X2) -> plus#(X1,X2) p83: plus#(X1,mark(X2)) -> plus#(X1,X2) p84: plus#(active(X1),X2) -> plus#(X1,X2) p85: plus#(X1,active(X2)) -> plus#(X1,X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p6, p7, p10, p14, p17, p20, p23, p26, p28, p30, p32, p33, p34, p36, p37, p39, p40, p42, p43, p45, p46, p48, p49, p51, p52} {p58, p59} {p60, p61} {p74, p75, p76, p77, p78, p79} {p80, p81} {p82, p83, p84, p85} {p54, p55, p56, p57} {p62, p63} {p64, p65, p66, p67} {p68, p69, p70, p71, p72, p73} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p5: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p6: mark#(s(X)) -> mark#(X) p7: mark#(s(X)) -> active#(s(mark(X))) p8: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p9: mark#(U42(X1,X2,X3)) -> mark#(X1) p10: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p11: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p12: mark#(U41(X1,X2,X3)) -> mark#(X1) p13: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p14: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p15: mark#(U31(X1,X2)) -> mark#(X1) p16: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p17: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p18: mark#(U21(X)) -> mark#(X) p19: mark#(U21(X)) -> active#(U21(mark(X))) p20: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p21: mark#(isNat(X)) -> active#(isNat(X)) p22: active#(U31(tt(),N)) -> mark#(N) p23: mark#(U12(X)) -> mark#(X) p24: mark#(U12(X)) -> active#(U12(mark(X))) p25: mark#(U11(X1,X2)) -> mark#(X1) p26: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(1,1)) x1 U11_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (0,1) tt_A() = (2,93) mark#_A(x1) = ((1,0),(1,1)) x1 + (0,3) U12_A(x1) = ((1,0),(1,1)) x1 + (0,1) isNat_A(x1) = ((0,0),(1,0)) x1 + (2,47) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (7,1) mark_A(x1) = x1 + (0,2) s_A(x1) = ((1,0),(1,0)) x1 + (12,59) U41_A(x1,x2,x3) = x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (17,0) |0|_A() = (49,1) U31_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (53,1) U42_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (17,68) U21_A(x1) = ((1,0),(1,1)) x1 + (0,4) active_A(x1) = x1 precedence: mark = s > U41 = U42 > U31 > active# = U11 = U12 = isNat = plus = active > tt = mark# = |0| = U21 partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [1] pi(U12) = [1] pi(isNat) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(U41) = [1] pi(|0|) = [] pi(U31) = [] pi(U42) = [] pi(U21) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (3,5) U11_A(x1,x2) = (0,0) tt_A() = (2,2) mark#_A(x1) = (3,5) U12_A(x1) = (1,1) isNat_A(x1) = (3,6) plus_A(x1,x2) = (0,2) mark_A(x1) = (2,3) s_A(x1) = (0,4) U41_A(x1,x2,x3) = (0,0) |0|_A() = (0,1) U31_A(x1,x2) = (0,0) U42_A(x1,x2,x3) = (0,0) U21_A(x1) = (0,1) active_A(x1) = (2,3) precedence: U12 = U31 > |0| > U41 > tt = mark = active > U42 > U21 > active# = mark# = isNat = plus > U11 = s partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(|0|) = [] pi(U31) = [] pi(U42) = [] pi(U21) = [] 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(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p5: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p6: mark#(s(X)) -> mark#(X) p7: mark#(s(X)) -> active#(s(mark(X))) p8: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p9: mark#(U42(X1,X2,X3)) -> mark#(X1) p10: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p11: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p12: mark#(U41(X1,X2,X3)) -> mark#(X1) p13: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p14: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p15: mark#(U31(X1,X2)) -> mark#(X1) p16: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p17: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p18: mark#(U21(X)) -> mark#(X) p19: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p20: mark#(isNat(X)) -> active#(isNat(X)) p21: active#(U31(tt(),N)) -> mark#(N) p22: mark#(U12(X)) -> mark#(X) p23: mark#(U12(X)) -> active#(U12(mark(X))) p24: mark#(U11(X1,X2)) -> mark#(X1) p25: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, p19, p20, p21, p22, p23, p24, p25} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U31(tt(),N)) -> mark#(N) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> active#(U12(mark(X))) p6: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p7: mark#(U12(X)) -> mark#(X) p8: mark#(isNat(X)) -> active#(isNat(X)) p9: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p10: mark#(U21(X)) -> mark#(X) p11: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p12: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p13: mark#(U31(X1,X2)) -> mark#(X1) p14: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p15: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p16: mark#(U41(X1,X2,X3)) -> mark#(X1) p17: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p18: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p19: mark#(U42(X1,X2,X3)) -> mark#(X1) p20: mark#(s(X)) -> active#(s(mark(X))) p21: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p22: mark#(s(X)) -> mark#(X) p23: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p24: mark#(plus(X1,X2)) -> mark#(X1) p25: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (2,1) U11_A(x1,x2) = (3,6) tt_A() = (6,8) mark#_A(x1) = (2,4) U12_A(x1) = (1,7) isNat_A(x1) = (3,10) mark_A(x1) = (4,5) U31_A(x1,x2) = (3,3) U41_A(x1,x2,x3) = (3,0) U42_A(x1,x2,x3) = (3,3) s_A(x1) = (1,10) plus_A(x1,x2) = (3,2) U21_A(x1) = (5,7) |0|_A() = (7,9) active_A(x1) = (4,5) precedence: U31 > active# = tt = mark# = U12 = isNat = mark = U42 = s = plus = |0| = active > U11 = U41 = U21 partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(mark) = [] pi(U31) = [] pi(U41) = [] pi(U42) = [] pi(s) = [] pi(plus) = [] pi(U21) = [] pi(|0|) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (2,4) U11_A(x1,x2) = (4,7) tt_A() = (6,7) mark#_A(x1) = (2,4) U12_A(x1) = (0,8) isNat_A(x1) = (0,1) mark_A(x1) = (3,6) U31_A(x1,x2) = (4,7) U41_A(x1,x2,x3) = (1,3) U42_A(x1,x2,x3) = (2,4) s_A(x1) = (0,2) plus_A(x1,x2) = (5,5) U21_A(x1) = (7,8) |0|_A() = (7,8) active_A(x1) = (3,6) precedence: U21 > tt = isNat > U31 > U12 = mark = active > U41 > plus > active# = mark# = |0| > U11 > U42 > s partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(mark) = [] pi(U31) = [] pi(U41) = [] pi(U42) = [] pi(s) = [] pi(plus) = [] pi(U21) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p20 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U31(tt(),N)) -> mark#(N) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> active#(U12(mark(X))) p6: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p7: mark#(U12(X)) -> mark#(X) p8: mark#(isNat(X)) -> active#(isNat(X)) p9: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p10: mark#(U21(X)) -> mark#(X) p11: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p12: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p13: mark#(U31(X1,X2)) -> mark#(X1) p14: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p15: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p16: mark#(U41(X1,X2,X3)) -> mark#(X1) p17: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p18: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p19: mark#(U42(X1,X2,X3)) -> mark#(X1) p20: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p21: mark#(s(X)) -> mark#(X) p22: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p23: mark#(plus(X1,X2)) -> mark#(X1) p24: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, p19, p20, p21, p22, p23, p24} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p5: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p6: mark#(s(X)) -> mark#(X) p7: mark#(U42(X1,X2,X3)) -> mark#(X1) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p10: mark#(U41(X1,X2,X3)) -> mark#(X1) p11: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p12: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p13: mark#(U31(X1,X2)) -> mark#(X1) p14: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p15: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p16: mark#(U21(X)) -> mark#(X) p17: mark#(isNat(X)) -> active#(isNat(X)) p18: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p19: mark#(U12(X)) -> mark#(X) p20: mark#(U12(X)) -> active#(U12(mark(X))) p21: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p22: mark#(U11(X1,X2)) -> mark#(X1) p23: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p24: active#(U31(tt(),N)) -> mark#(N) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (2,1) U11_A(x1,x2) = (3,7) tt_A() = (4,0) mark#_A(x1) = (2,4) U12_A(x1) = (1,6) isNat_A(x1) = (3,0) plus_A(x1,x2) = (3,0) mark_A(x1) = (7,5) s_A(x1) = (6,0) U41_A(x1,x2,x3) = (3,0) U42_A(x1,x2,x3) = (3,4) |0|_A() = (5,0) U31_A(x1,x2) = (3,0) U21_A(x1) = (5,0) active_A(x1) = (7,5) precedence: U11 = plus = mark = U41 = |0| = U21 = active > active# = mark# = isNat = U42 > U31 > tt = U12 = s partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(U42) = [] pi(|0|) = [] pi(U31) = [] pi(U21) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (2,3) U11_A(x1,x2) = (4,4) tt_A() = (6,7) mark#_A(x1) = (2,3) U12_A(x1) = (7,6) isNat_A(x1) = (1,2) plus_A(x1,x2) = (7,0) mark_A(x1) = (4,5) s_A(x1) = (0,8) U41_A(x1,x2,x3) = (3,1) U42_A(x1,x2,x3) = (0,5) |0|_A() = (5,5) U31_A(x1,x2) = (1,0) U21_A(x1) = (5,0) active_A(x1) = (4,5) precedence: U11 = isNat = plus = mark = s = U41 = U42 = U21 = active > active# = tt = mark# = U12 = |0| = U31 partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(U42) = [] pi(|0|) = [] pi(U31) = [] pi(U21) = [] pi(active) = [] The next rules are strictly ordered: p20 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p5: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p6: mark#(s(X)) -> mark#(X) p7: mark#(U42(X1,X2,X3)) -> mark#(X1) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p10: mark#(U41(X1,X2,X3)) -> mark#(X1) p11: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p12: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p13: mark#(U31(X1,X2)) -> mark#(X1) p14: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p15: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p16: mark#(U21(X)) -> mark#(X) p17: mark#(isNat(X)) -> active#(isNat(X)) p18: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p19: mark#(U12(X)) -> mark#(X) p20: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p21: mark#(U11(X1,X2)) -> mark#(X1) p22: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p23: active#(U31(tt(),N)) -> mark#(N) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, p19, p20, p21, p22, p23} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U31(tt(),N)) -> mark#(N) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> mark#(X) p6: mark#(isNat(X)) -> active#(isNat(X)) p7: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p8: mark#(U21(X)) -> mark#(X) p9: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p10: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p11: mark#(U31(X1,X2)) -> mark#(X1) p12: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p13: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p14: mark#(U41(X1,X2,X3)) -> mark#(X1) p15: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p16: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p17: mark#(U42(X1,X2,X3)) -> mark#(X1) p18: mark#(s(X)) -> mark#(X) p19: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p20: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p21: mark#(plus(X1,X2)) -> mark#(X1) p22: mark#(plus(X1,X2)) -> mark#(X2) p23: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (1,3) U11_A(x1,x2) = ((1,0),(1,0)) x1 + (0,9) tt_A() = (3,0) mark#_A(x1) = ((0,0),(1,0)) x1 + (1,3) U12_A(x1) = ((1,0),(0,0)) x1 + (0,7) isNat_A(x1) = (3,23) mark_A(x1) = x1 + (0,2) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (2,4) U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (18,31) U42_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (18,28) U21_A(x1) = ((1,0),(1,0)) x1 + (0,3) s_A(x1) = ((1,0),(0,0)) x1 + (19,25) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (2,15) |0|_A() = (6,7) active_A(x1) = x1 + (0,1) precedence: mark = s = plus = |0| > tt = U42 > U11 > U31 > active# = mark# = U12 = U21 = active > isNat = U41 partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(mark) = [1] pi(U31) = [] pi(U41) = [] pi(U42) = [] pi(U21) = [] pi(s) = [] pi(plus) = [] pi(|0|) = [] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (0,5) U11_A(x1,x2) = (0,6) tt_A() = (2,24) mark#_A(x1) = (0,5) U12_A(x1) = (8,25) isNat_A(x1) = (9,10) mark_A(x1) = ((0,0),(1,0)) x1 + (1,7) U31_A(x1,x2) = (0,1) U41_A(x1,x2,x3) = (22,4) U42_A(x1,x2,x3) = (16,0) U21_A(x1) = (0,6) s_A(x1) = (10,0) plus_A(x1,x2) = (28,3) |0|_A() = (22,25) active_A(x1) = ((0,0),(1,0)) x1 + (1,2) precedence: tt > U12 = U31 = active > U11 = mark > U42 > U21 > active# = mark# = isNat = U41 = s = plus = |0| partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(mark) = [] pi(U31) = [] pi(U41) = [] pi(U42) = [] pi(U21) = [] pi(s) = [] pi(plus) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p20 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U31(tt(),N)) -> mark#(N) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> mark#(X) p6: mark#(isNat(X)) -> active#(isNat(X)) p7: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p8: mark#(U21(X)) -> mark#(X) p9: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p10: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p11: mark#(U31(X1,X2)) -> mark#(X1) p12: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p13: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p14: mark#(U41(X1,X2,X3)) -> mark#(X1) p15: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p16: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p17: mark#(U42(X1,X2,X3)) -> mark#(X1) p18: mark#(s(X)) -> mark#(X) p19: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p20: mark#(plus(X1,X2)) -> mark#(X1) p21: mark#(plus(X1,X2)) -> mark#(X2) p22: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, p19, p20, p21, p22} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(plus(X1,X2)) -> mark#(X1) p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p5: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p6: mark#(s(X)) -> mark#(X) p7: mark#(U42(X1,X2,X3)) -> mark#(X1) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p10: mark#(U41(X1,X2,X3)) -> mark#(X1) p11: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p12: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p13: mark#(U31(X1,X2)) -> mark#(X1) p14: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p15: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p16: mark#(U21(X)) -> mark#(X) p17: mark#(isNat(X)) -> active#(isNat(X)) p18: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p19: mark#(U12(X)) -> mark#(X) p20: mark#(U11(X1,X2)) -> mark#(X1) p21: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p22: active#(U31(tt(),N)) -> mark#(N) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = x1 U11_A(x1,x2) = x1 + ((0,0),(1,0)) x2 tt_A() = (6,18) mark#_A(x1) = x1 + (0,4) U12_A(x1) = x1 + (0,5) isNat_A(x1) = ((0,0),(1,0)) x1 + (6,1) plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (5,17) mark_A(x1) = x1 + (0,2) s_A(x1) = ((1,0),(0,0)) x1 + (8,0) U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (7,12) U42_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,0) U21_A(x1) = x1 + (0,3) U31_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,1) active_A(x1) = x1 |0|_A() = (20,0) precedence: |0| > s > active# = isNat > mark# > mark = U21 = U31 > U11 > U42 > tt = U12 = active > plus > U41 partial status: pi(active#) = [] pi(U11) = [1] pi(tt) = [] pi(mark#) = [1] pi(U12) = [1] pi(isNat) = [] pi(plus) = [2] pi(mark) = [1] pi(s) = [] pi(U41) = [] pi(U42) = [1] pi(U21) = [] pi(U31) = [1, 2] pi(active) = [1] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (24,17) U11_A(x1,x2) = ((1,0),(1,1)) x1 + (37,18) tt_A() = (22,15) mark#_A(x1) = ((1,0),(1,0)) x1 + (10,2) U12_A(x1) = (0,0) isNat_A(x1) = (22,15) plus_A(x1,x2) = ((1,0),(0,0)) x2 + (0,19) mark_A(x1) = ((1,0),(0,0)) x1 + (2,18) s_A(x1) = (0,18) U41_A(x1,x2,x3) = (23,21) U42_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (11,0) U21_A(x1) = (14,21) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (0,1) active_A(x1) = ((0,0),(1,0)) x1 + (26,20) |0|_A() = (25,0) precedence: active# = mark# > U11 > U31 = active = |0| > tt = U12 = plus = mark = s = U42 = U21 > isNat = U41 partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(U42) = [] pi(U21) = [] pi(U31) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p3, p4, p5, p6, p7, p8, p10, p12, p14, p16, p19, p20, p21, p22 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p5: mark#(U31(X1,X2)) -> mark#(X1) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(isNat(X)) -> active#(isNat(X)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U31(X1,X2)) -> mark#(X1) p5: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(plus(X1,X2)) -> mark#(X2) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (16,110) U11_A(x1,x2) = ((1,0),(1,0)) x1 + (0,65) tt_A() = (6,1) mark#_A(x1) = ((1,0),(0,0)) x1 + (8,126) U12_A(x1) = (6,36) isNat_A(x1) = (15,124) U41_A(x1,x2,x3) = (9,44) U42_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (1,26) U31_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (9,107) mark_A(x1) = ((1,0),(1,1)) x1 + (0,28) s_A(x1) = (1,29) plus_A(x1,x2) = x1 + x2 + (56,26) U21_A(x1) = (7,26) active_A(x1) = x1 + (0,27) |0|_A() = (0,70) precedence: U11 > s = plus = U21 > tt = U12 = |0| > mark# = isNat = U31 = mark > active# = U42 > U41 > active partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(U41) = [] pi(U42) = [] pi(U31) = [] pi(mark) = [1] pi(s) = [] pi(plus) = [] pi(U21) = [] pi(active) = [1] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = (20,27) U11_A(x1,x2) = (7,11) tt_A() = (1,1) mark#_A(x1) = (20,27) U12_A(x1) = (4,0) isNat_A(x1) = (21,1) U41_A(x1,x2,x3) = (42,0) U42_A(x1,x2,x3) = (28,35) U31_A(x1,x2) = (106,3) mark_A(x1) = ((1,0),(1,0)) x1 + (8,15) s_A(x1) = (19,26) plus_A(x1,x2) = (52,66) U21_A(x1) = (10,17) active_A(x1) = ((1,0),(1,1)) x1 + (6,2) |0|_A() = (20,17) precedence: plus > isNat > U41 > U31 = |0| > active# = mark# = U42 > tt = U12 > mark = U21 > U11 = s = active partial status: pi(active#) = [] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(U41) = [] pi(U42) = [] pi(U31) = [] pi(mark) = [] pi(s) = [] pi(plus) = [] pi(U21) = [] pi(active) = [1] 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: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U31(X1,X2)) -> mark#(X1) p5: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2))) p2: mark#(plus(X1,X2)) -> mark#(X2) p3: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p4: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p5: mark#(U31(X1,X2)) -> mark#(X1) p6: mark#(isNat(X)) -> active#(isNat(X)) p7: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(1,1)) x1 + (5,9) U11_A(x1,x2) = (4,5) tt_A() = (1,0) mark#_A(x1) = ((1,0),(0,0)) x1 + (6,34) U12_A(x1) = (2,0) isNat_A(x1) = (4,19) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (31,33) U41_A(x1,x2,x3) = x3 + (32,0) mark_A(x1) = ((1,0),(1,1)) x1 + (0,6) U42_A(x1,x2,x3) = ((0,0),(1,0)) x2 + x3 + (9,47) s_A(x1) = (2,39) U31_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (5,2) active_A(x1) = x1 + (0,4) U21_A(x1) = ((1,0),(0,0)) x1 + (0,8) |0|_A() = (5,37) precedence: U42 > active# = mark# = U12 > isNat > U11 > plus = U21 > tt = mark = s = |0| > U31 = active > U41 partial status: pi(active#) = [1] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(U41) = [3] pi(mark) = [] pi(U42) = [] pi(s) = [] pi(U31) = [1] pi(active) = [1] pi(U21) = [] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = x1 U11_A(x1,x2) = (0,0) tt_A() = (4,0) mark#_A(x1) = (0,0) U12_A(x1) = (0,0) isNat_A(x1) = (0,0) plus_A(x1,x2) = (0,1) U41_A(x1,x2,x3) = (2,0) mark_A(x1) = (5,3) U42_A(x1,x2,x3) = (1,0) s_A(x1) = (3,1) U31_A(x1,x2) = (0,2) active_A(x1) = (5,3) U21_A(x1) = (0,0) |0|_A() = (4,1) precedence: U31 > |0| > U41 > plus > U11 > tt = U12 = mark = active > U21 > mark# > active# = U42 > isNat = s partial status: pi(active#) = [1] pi(U11) = [] pi(tt) = [] pi(mark#) = [] pi(U12) = [] pi(isNat) = [] pi(plus) = [] pi(U41) = [] pi(mark) = [] pi(U42) = [] pi(s) = [] pi(U31) = [] pi(active) = [] pi(U21) = [] pi(|0|) = [] The next rules are strictly ordered: p1, p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) p2: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p3: mark#(U31(X1,X2)) -> mark#(X1) p4: mark#(isNat(X)) -> active#(isNat(X)) p5: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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#(plus(X1,X2)) -> mark#(X2) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U31(X1,X2)) -> mark#(X1) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of r29, r30, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(1,0)) x1 + (2,0) plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (8,0) isNat_A(x1) = (6,2) active#_A(x1) = (7,5) U41_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (3,1) tt_A() = (7,3) U42_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (4,0) U31_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (3,1) s_A(x1) = ((0,0),(1,0)) x1 mark_A(x1) = ((1,0),(1,1)) x1 + (4,0) active_A(x1) = ((1,0),(1,1)) x1 + (4,3) precedence: mark# = plus = isNat = active# = U41 = tt = U42 = U31 = s = mark = active partial status: pi(mark#) = [] pi(plus) = [] pi(isNat) = [] pi(active#) = [] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(U31) = [] pi(s) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (0,0) plus_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (0,4) isNat_A(x1) = (0,0) active#_A(x1) = (0,0) U41_A(x1,x2,x3) = (1,1) tt_A() = (2,1) U42_A(x1,x2,x3) = (0,0) U31_A(x1,x2) = x2 + (1,1) s_A(x1) = (1,2) mark_A(x1) = ((1,0),(1,1)) x1 active_A(x1) = ((1,0),(1,1)) x1 + (2,3) precedence: isNat = U41 = tt = s = mark > mark# = plus = active# = U42 = U31 = active partial status: pi(mark#) = [] pi(plus) = [] pi(isNat) = [] pi(active#) = [] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(U31) = [] pi(s) = [] 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#(plus(X1,X2)) -> mark#(X2) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U31(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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#(plus(X1,X2)) -> mark#(X2) p2: mark#(U31(X1,X2)) -> mark#(X1) p3: mark#(isNat(X)) -> active#(isNat(X)) p4: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of r29, r30, r43, r44, r45, r46, r47, r48 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (4,2) plus_A(x1,x2) = x1 + (1,1) U31_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (5,1) isNat_A(x1) = ((0,0),(1,0)) x1 + (2,3) active#_A(x1) = x1 + (1,1) U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + x3 tt_A() = (5,1) U42_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 mark_A(x1) = ((1,0),(1,1)) x1 active_A(x1) = ((1,0),(1,1)) x1 + (3,4) precedence: mark# = plus = U31 = isNat = active# = U41 = mark = active > tt > U42 partial status: pi(mark#) = [] pi(plus) = [] pi(U31) = [2] pi(isNat) = [] pi(active#) = [] pi(U41) = [2, 3] pi(tt) = [] pi(U42) = [2, 3] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (1,2) plus_A(x1,x2) = (2,3) U31_A(x1,x2) = (2,3) isNat_A(x1) = (0,1) active#_A(x1) = (2,3) U41_A(x1,x2,x3) = (2,3) tt_A() = (4,3) U42_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (3,4) mark_A(x1) = ((1,0),(0,0)) x1 + (4,2) active_A(x1) = ((1,0),(0,0)) x1 + (4,2) precedence: U31 = isNat = active# = tt = U42 = mark = active > plus = U41 > mark# partial status: pi(mark#) = [] pi(plus) = [] pi(U31) = [] pi(isNat) = [] pi(active#) = [] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p3, p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) p2: mark#(U31(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) 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#(plus(X1,X2)) -> mark#(X2) p2: mark#(U31(X1,X2)) -> mark#(X1) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = x1 + (1,1) plus_A(x1,x2) = x1 + x2 + (2,2) U31_A(x1,x2) = x1 + x2 + (2,2) precedence: plus > mark# = U31 partial status: pi(mark#) = [1] pi(plus) = [1, 2] pi(U31) = [1, 2] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (0,0) plus_A(x1,x2) = x1 + x2 + (1,1) U31_A(x1,x2) = (1,1) precedence: plus > U31 > mark# partial status: pi(mark#) = [] pi(plus) = [1] pi(U31) = [] 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#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = x1 + (1,2) plus_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,1) precedence: mark# > plus partial status: pi(mark#) = [1] pi(plus) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (0,0) plus_A(x1,x2) = (1,1) precedence: mark# > plus partial status: pi(mark#) = [] pi(plus) = [] 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: U12#(mark(X)) -> U12#(X) p2: U12#(active(X)) -> U12#(X) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U12#_A(x1) = x1 + (1,2) mark_A(x1) = x1 + (2,1) active_A(x1) = ((1,0),(1,1)) x1 + (2,1) precedence: U12# = mark = active partial status: pi(U12#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U12#_A(x1) = ((1,0),(1,0)) x1 + (0,2) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: U12# = mark = active partial status: pi(U12#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2 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(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isNat#_A(x1) = x1 + (1,2) mark_A(x1) = x1 + (2,1) active_A(x1) = ((1,0),(1,1)) x1 + (2,1) precedence: isNat# = mark > active partial status: pi(isNat#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isNat#_A(x1) = ((1,0),(1,0)) x1 + (0,2) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: isNat# = mark = active partial status: pi(isNat#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2 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: U42#(mark(X1),X2,X3) -> U42#(X1,X2,X3) p2: U42#(X1,X2,active(X3)) -> U42#(X1,X2,X3) p3: U42#(X1,active(X2),X3) -> U42#(X1,X2,X3) p4: U42#(active(X1),X2,X3) -> U42#(X1,X2,X3) p5: U42#(X1,X2,mark(X3)) -> U42#(X1,X2,X3) p6: U42#(X1,mark(X2),X3) -> U42#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U42#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (2,2) mark_A(x1) = ((1,0),(1,1)) x1 + (1,1) active_A(x1) = ((1,0),(1,1)) x1 + (1,1) precedence: active > mark > U42# partial status: pi(U42#) = [2] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U42#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: U42# = mark = active partial status: pi(U42#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p3, p4, p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U42#(X1,X2,active(X3)) -> U42#(X1,X2,X3) p2: U42#(X1,X2,mark(X3)) -> U42#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U42#(X1,X2,active(X3)) -> U42#(X1,X2,X3) p2: U42#(X1,X2,mark(X3)) -> U42#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U42#_A(x1,x2,x3) = x1 + x3 + (1,1) active_A(x1) = ((1,0),(1,1)) x1 mark_A(x1) = x1 precedence: active > U42# = mark partial status: pi(U42#) = [3] pi(active) = [1] pi(mark) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U42#_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: U42# = active = mark partial status: pi(U42#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p1, p2 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: s#(mark(X)) -> s#(X) p2: s#(active(X)) -> s#(X) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: s#_A(x1) = x1 + (1,2) mark_A(x1) = x1 + (2,1) active_A(x1) = ((1,0),(1,1)) x1 + (2,1) precedence: s# = mark > active partial status: pi(s#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: s#_A(x1) = ((1,0),(1,0)) x1 + (0,2) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: s# = mark = active partial status: pi(s#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2 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(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: plus#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (2,2) mark_A(x1) = ((1,0),(0,0)) x1 + (1,3) active_A(x1) = ((1,0),(0,0)) x1 + (3,1) precedence: plus# = mark = active partial status: pi(plus#) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: plus#_A(x1,x2) = (0,0) mark_A(x1) = (1,1) active_A(x1) = (1,1) precedence: mark > plus# = active partial status: pi(plus#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2, p3, p4 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(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U11#_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (2,2) mark_A(x1) = ((1,0),(1,1)) x1 + (3,1) active_A(x1) = x1 + (1,3) precedence: U11# = mark = active partial status: pi(U11#) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U11#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: U11# = mark = active partial status: pi(U11#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2, p3, p4 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(X)) -> U21#(X) p2: U21#(active(X)) -> U21#(X) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U21#_A(x1) = x1 + (1,2) mark_A(x1) = x1 + (2,1) active_A(x1) = ((1,0),(1,1)) x1 + (2,1) precedence: U21# = mark = active partial status: pi(U21#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U21#_A(x1) = ((1,0),(1,0)) x1 + (0,2) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: U21# = mark = active partial status: pi(U21#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2 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: U31#(mark(X1),X2) -> U31#(X1,X2) p2: U31#(X1,active(X2)) -> U31#(X1,X2) p3: U31#(active(X1),X2) -> U31#(X1,X2) p4: U31#(X1,mark(X2)) -> U31#(X1,X2) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U31#_A(x1,x2) = x1 + x2 + (2,2) mark_A(x1) = ((1,0),(1,1)) x1 + (1,1) active_A(x1) = ((1,0),(1,1)) x1 + (1,3) precedence: U31# = mark = active partial status: pi(U31#) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U31#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: mark = active > U31# partial status: pi(U31#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p2, p3, p4 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: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3) p2: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3) p3: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3) p4: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3) p5: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3) p6: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U41#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (2,2) mark_A(x1) = ((1,0),(1,1)) x1 + (1,1) active_A(x1) = ((1,0),(1,1)) x1 + (1,1) precedence: active > mark > U41# partial status: pi(U41#) = [2] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U41#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: U41# = mark = active partial status: pi(U41#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1, p3, p4, p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3) p2: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3) p2: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3) and R consists of: r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2))) r2: active(U12(tt())) -> mark(tt()) r3: active(U21(tt())) -> mark(tt()) r4: active(U31(tt(),N)) -> mark(N) r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N)) r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M))) r7: active(isNat(|0|())) -> mark(tt()) r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2)) r9: active(isNat(s(V1))) -> mark(U21(isNat(V1))) r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N)) r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N)) r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) r13: mark(tt()) -> active(tt()) r14: mark(U12(X)) -> active(U12(mark(X))) r15: mark(isNat(X)) -> active(isNat(X)) r16: mark(U21(X)) -> active(U21(mark(X))) r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3)) r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3)) r20: mark(s(X)) -> active(s(mark(X))) r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) r22: mark(|0|()) -> active(|0|()) r23: U11(mark(X1),X2) -> U11(X1,X2) r24: U11(X1,mark(X2)) -> U11(X1,X2) r25: U11(active(X1),X2) -> U11(X1,X2) r26: U11(X1,active(X2)) -> U11(X1,X2) r27: U12(mark(X)) -> U12(X) r28: U12(active(X)) -> U12(X) r29: isNat(mark(X)) -> isNat(X) r30: isNat(active(X)) -> isNat(X) r31: U21(mark(X)) -> U21(X) r32: U21(active(X)) -> U21(X) r33: U31(mark(X1),X2) -> U31(X1,X2) r34: U31(X1,mark(X2)) -> U31(X1,X2) r35: U31(active(X1),X2) -> U31(X1,X2) r36: U31(X1,active(X2)) -> U31(X1,X2) r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3) r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3) r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3) r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3) r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3) r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3) r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3) r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3) r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3) r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3) r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3) r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3) r49: s(mark(X)) -> s(X) r50: s(active(X)) -> s(X) r51: plus(mark(X1),X2) -> plus(X1,X2) r52: plus(X1,mark(X2)) -> plus(X1,X2) r53: plus(active(X1),X2) -> plus(X1,X2) r54: plus(X1,active(X2)) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U41#_A(x1,x2,x3) = x1 + x3 + (1,1) active_A(x1) = ((1,0),(1,1)) x1 mark_A(x1) = x1 precedence: active > U41# = mark partial status: pi(U41#) = [3] pi(active) = [1] pi(mark) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U41#_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: U41# = active = mark partial status: pi(U41#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains.