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: max/plus interpretations on natural numbers: active#_A(x1) = x1 + 8 U11_A(x1,x2) = max{x1 + 12, x2 + 70} tt_A = 5 mark#_A(x1) = x1 + 8 U12_A(x1) = x1 + 5 isNat_A(x1) = x1 + 28 plus_A(x1,x2) = max{x1 + 42, x2 + 42} mark_A(x1) = x1 s_A(x1) = x1 U41_A(x1,x2,x3) = max{x1 + 13, x2 + 42, x3 + 42} |0|_A = 5 U31_A(x1,x2) = max{x1, x2 + 34} U42_A(x1,x2,x3) = max{x1, x2 + 42, x3 + 42} U21_A(x1) = x1 active_A(x1) = x1 precedence: active# = mark# = isNat = |0| = U31 > U42 > plus > U41 > U11 = tt = U12 = mark = s = U21 = active 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) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = 384 U11_A(x1,x2) = 385 tt_A = 0 mark#_A(x1) = 384 U12_A(x1) = 379 isNat_A(x1) = 385 plus_A(x1,x2) = 388 mark_A(x1) = 372 s_A(x1) = 382 U41_A(x1,x2,x3) = 387 |0|_A = 7 U31_A(x1,x2) = 361 U42_A(x1,x2,x3) = 555 U21_A(x1) = 383 active_A(x1) = 372 precedence: |0| = U42 > plus > U41 > U12 > active# = mark# = U31 = U21 > mark = s = active > tt > U11 = isNat 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: p1 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#(plus(X1,X2)) -> mark#(X1) p3: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p4: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p5: mark#(s(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(mark(X))) p7: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p8: mark#(U42(X1,X2,X3)) -> mark#(X1) p9: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p10: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p11: mark#(U41(X1,X2,X3)) -> 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#(U31(X1,X2)) -> mark#(X1) p15: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p16: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p17: mark#(U21(X)) -> mark#(X) p18: mark#(U21(X)) -> active#(U21(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: mark#(plus(X1,X2)) -> mark#(X2) 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)) -> active#(U21(mark(X))) p11: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p12: mark#(U21(X)) -> mark#(X) p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p14: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p15: mark#(U31(X1,X2)) -> mark#(X1) p16: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p17: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N)) p18: mark#(U41(X1,X2,X3)) -> mark#(X1) p19: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p20: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p21: mark#(U42(X1,X2,X3)) -> mark#(X1) p22: mark#(s(X)) -> active#(s(mark(X))) p23: mark#(s(X)) -> mark#(X) p24: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p25: mark#(plus(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 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: max/plus interpretations on natural numbers: mark#_A(x1) = max{37, x1 - 92} plus_A(x1,x2) = max{157, x1 + 131, x2 + 91} U11_A(x1,x2) = max{x1 + 87, x2 + 113} active#_A(x1) = max{11, x1 - 92} mark_A(x1) = max{26, x1} U31_A(x1,x2) = max{x1 + 94, x2 + 130} tt_A = 7 U12_A(x1) = max{93, x1 + 12} U41_A(x1,x2,x3) = max{159, x1 + 68, x2 + 91, x3 + 131} U42_A(x1,x2,x3) = max{158, x1, x2 + 91, x3 + 131} isNat_A(x1) = x1 + 23 s_A(x1) = max{119, x1} U21_A(x1) = max{99, x1} |0|_A = 3 active_A(x1) = x1 precedence: mark# = plus = U11 = active# = mark = U31 = tt = U12 = U41 = U42 = isNat = s = U21 = |0| = active partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(U31) = [] pi(tt) = [] pi(U12) = [] pi(U41) = [] pi(U42) = [] pi(isNat) = [] pi(s) = [] pi(U21) = [] pi(|0|) = [] pi(active) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 324 plus_A(x1,x2) = 379 U11_A(x1,x2) = 0 active#_A(x1) = 324 mark_A(x1) = 83 U31_A(x1,x2) = 52 tt_A = 22 U12_A(x1) = 91 U41_A(x1,x2,x3) = 231 U42_A(x1,x2,x3) = 256 isNat_A(x1) = 87 s_A(x1) = 223 U21_A(x1) = 91 |0|_A = 23 active_A(x1) = 83 precedence: U11 > mark# = plus = active# = U31 = U12 = U41 = U42 = isNat = s = U21 > mark = |0| = active > tt partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(U31) = [] pi(tt) = [] pi(U12) = [] pi(U41) = [] pi(U42) = [] pi(isNat) = [] pi(s) = [] pi(U21) = [] pi(|0|) = [] pi(active) = [] The next rules are strictly ordered: p3, p17 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#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U12(X)) -> active#(U12(mark(X))) p5: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p6: mark#(U12(X)) -> mark#(X) p7: mark#(isNat(X)) -> active#(isNat(X)) p8: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p9: mark#(U21(X)) -> active#(U21(mark(X))) p10: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p11: mark#(U21(X)) -> mark#(X) p12: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p13: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p14: mark#(U31(X1,X2)) -> mark#(X1) p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p16: mark#(U41(X1,X2,X3)) -> mark#(X1) p17: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p18: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p19: mark#(U42(X1,X2,X3)) -> mark#(X1) p20: mark#(s(X)) -> active#(s(mark(X))) p21: mark#(s(X)) -> mark#(X) p22: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p23: mark#(plus(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, 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: mark#(plus(X1,X2)) -> mark#(X2) p2: mark#(plus(X1,X2)) -> mark#(X1) p3: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p4: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p5: mark#(s(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(mark(X))) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U42(X1,X2,X3)) -> mark#(X1) p9: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p10: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2)) p11: mark#(U41(X1,X2,X3)) -> mark#(X1) p12: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p13: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p14: mark#(U31(X1,X2)) -> mark#(X1) p15: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p16: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p17: mark#(U21(X)) -> mark#(X) p18: mark#(U21(X)) -> active#(U21(mark(X))) p19: mark#(isNat(X)) -> active#(isNat(X)) p20: mark#(U12(X)) -> mark#(X) p21: mark#(U12(X)) -> active#(U12(mark(X))) p22: mark#(U11(X1,X2)) -> mark#(X1) p23: 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: max/plus interpretations on natural numbers: mark#_A(x1) = max{87, x1 + 41} plus_A(x1,x2) = max{66, x1 + 53, x2 + 65} active#_A(x1) = max{87, x1 + 41} mark_A(x1) = max{1, x1} s_A(x1) = max{58, x1} U41_A(x1,x2,x3) = max{x1 + 10, x2 + 65, x3 + 53} isNat_A(x1) = max{67, x1 + 9} U21_A(x1) = max{8, x1} U42_A(x1,x2,x3) = max{86, x1 + 2, x2 + 65, x3 + 53} U11_A(x1,x2) = max{x1, x2 + 64} tt_A = 76 U31_A(x1,x2) = max{x1 + 44, x2 + 46} U12_A(x1) = max{64, x1 + 8} active_A(x1) = max{7, x1} |0|_A = 67 precedence: isNat > mark# = plus = active# = U11 = |0| > U41 = U31 > U21 > tt > U42 > mark = U12 > s = active partial status: pi(mark#) = [] pi(plus) = [] pi(active#) = [] pi(mark) = [1] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [] pi(U11) = [] pi(tt) = [] pi(U31) = [2] pi(U12) = [] pi(active) = [1] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 285 plus_A(x1,x2) = 320 active#_A(x1) = 285 mark_A(x1) = max{179, x1 + 9} s_A(x1) = 291 U41_A(x1,x2,x3) = 310 isNat_A(x1) = 290 U21_A(x1) = 281 U42_A(x1,x2,x3) = 300 U11_A(x1,x2) = 179 tt_A = 180 U31_A(x1,x2) = 284 U12_A(x1) = 102 active_A(x1) = max{103, x1} |0|_A = 189 precedence: U41 > mark# = plus = active# = s = active > U31 = U12 = |0| > mark = tt > isNat = U21 = U42 = U11 partial status: pi(mark#) = [] pi(plus) = [] pi(active#) = [] pi(mark) = [1] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [] pi(U11) = [] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p8, p10 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#(plus(X1,X2)) -> mark#(X1) p3: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p4: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p5: mark#(s(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(mark(X))) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: mark#(U41(X1,X2,X3)) -> mark#(X1) p10: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p11: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p12: mark#(U31(X1,X2)) -> mark#(X1) p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p14: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p15: mark#(U21(X)) -> mark#(X) p16: mark#(U21(X)) -> active#(U21(mark(X))) p17: mark#(isNat(X)) -> active#(isNat(X)) p18: mark#(U12(X)) -> mark#(X) p19: mark#(U12(X)) -> active#(U12(mark(X))) p20: mark#(U11(X1,X2)) -> mark#(X1) p21: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> active#(U12(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U12(X)) -> mark#(X) p8: mark#(isNat(X)) -> active#(isNat(X)) p9: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p10: mark#(U21(X)) -> active#(U21(mark(X))) p11: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p12: mark#(U21(X)) -> mark#(X) p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p14: mark#(U31(X1,X2)) -> mark#(X1) p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p16: mark#(U41(X1,X2,X3)) -> mark#(X1) p17: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p18: mark#(s(X)) -> active#(s(mark(X))) p19: mark#(s(X)) -> mark#(X) p20: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p21: mark#(plus(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 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: max/plus interpretations on natural numbers: mark#_A(x1) = max{18, x1 - 7} plus_A(x1,x2) = max{x1 + 82, x2 + 37} U11_A(x1,x2) = max{66, x1} active#_A(x1) = max{19, x1 - 7} mark_A(x1) = x1 U41_A(x1,x2,x3) = max{x1 + 16, x2 + 37, x3 + 82} tt_A = 2 U42_A(x1,x2,x3) = max{x2 + 37, x3 + 82} isNat_A(x1) = 66 U12_A(x1) = max{27, x1} s_A(x1) = max{39, x1} U21_A(x1) = max{40, x1} U31_A(x1,x2) = max{x1 + 27, x2 + 29} active_A(x1) = max{1, x1} |0|_A = 57 precedence: plus = |0| > U41 = isNat > U11 = U42 = U21 = U31 > U12 > mark# = active# = mark = tt = s = active partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [1] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(isNat) = [] pi(U12) = [] pi(s) = [] pi(U21) = [] pi(U31) = [2] pi(active) = [1] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 52 plus_A(x1,x2) = 46 U11_A(x1,x2) = 6 active#_A(x1) = 52 mark_A(x1) = x1 + 4 U41_A(x1,x2,x3) = 6 tt_A = 27 U42_A(x1,x2,x3) = 6 isNat_A(x1) = 10 U12_A(x1) = 6 s_A(x1) = 51 U21_A(x1) = 7 U31_A(x1,x2) = 42 active_A(x1) = max{10, x1 + 4} |0|_A = 10 precedence: s = U21 > plus = tt = U42 = U31 = |0| > mark# = active# = mark = isNat = active > U11 > U12 > U41 partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [1] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(isNat) = [] pi(U12) = [] pi(s) = [] pi(U21) = [] pi(U31) = [] pi(active) = [1] pi(|0|) = [] The next rules are strictly ordered: p14 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#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> active#(U12(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U12(X)) -> mark#(X) p8: mark#(isNat(X)) -> active#(isNat(X)) p9: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p10: mark#(U21(X)) -> active#(U21(mark(X))) p11: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p12: mark#(U21(X)) -> mark#(X) p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p14: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p15: mark#(U41(X1,X2,X3)) -> mark#(X1) p16: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p17: mark#(s(X)) -> active#(s(mark(X))) p18: mark#(s(X)) -> mark#(X) p19: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p20: mark#(plus(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, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) p2: mark#(plus(X1,X2)) -> mark#(X1) p3: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p4: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p5: mark#(s(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(mark(X))) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p10: mark#(U41(X1,X2,X3)) -> mark#(X1) p11: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p12: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p14: mark#(U21(X)) -> mark#(X) p15: mark#(U21(X)) -> active#(U21(mark(X))) p16: mark#(isNat(X)) -> active#(isNat(X)) p17: mark#(U12(X)) -> mark#(X) p18: mark#(U12(X)) -> active#(U12(mark(X))) p19: mark#(U11(X1,X2)) -> mark#(X1) p20: 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: max/plus interpretations on natural numbers: mark#_A(x1) = max{0, x1 - 18} plus_A(x1,x2) = max{x1 + 45, x2 + 25} active#_A(x1) = max{0, x1 - 18} mark_A(x1) = x1 s_A(x1) = x1 U41_A(x1,x2,x3) = max{x1 + 19, x2 + 25, x3 + 45} isNat_A(x1) = x1 U21_A(x1) = x1 U42_A(x1,x2,x3) = max{x1 + 29, x2 + 25, x3 + 45} tt_A = 11 U31_A(x1,x2) = max{x1 + 19, x2 + 45} U12_A(x1) = max{40, x1 + 23} U11_A(x1,x2) = max{45, x1 + 28, x2 + 24} active_A(x1) = x1 |0|_A = 12 precedence: plus = mark = U41 = U11 = active = |0| > tt > mark# = active# = s = isNat = U21 = U42 = U31 = U12 partial status: pi(mark#) = [] pi(plus) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [2] pi(tt) = [] pi(U31) = [] pi(U12) = [1] pi(U11) = [] pi(active) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 59 plus_A(x1,x2) = 773 active#_A(x1) = 59 mark_A(x1) = 152 s_A(x1) = 318 U41_A(x1,x2,x3) = 60 isNat_A(x1) = 390 U21_A(x1) = 1 U42_A(x1,x2,x3) = 95 tt_A = 96 U31_A(x1,x2) = 45 U12_A(x1) = 492 U11_A(x1,x2) = 152 active_A(x1) = 152 |0|_A = 97 precedence: mark# = plus = active# = mark = s = U41 = isNat = U21 = U42 = tt = U31 = U12 = U11 = active = |0| partial status: pi(mark#) = [] pi(plus) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(U11) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p2, p10, p17 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#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p4: mark#(s(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(mark(X))) p6: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p7: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p8: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p11: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p12: mark#(U21(X)) -> mark#(X) p13: mark#(U21(X)) -> active#(U21(mark(X))) p14: mark#(isNat(X)) -> active#(isNat(X)) p15: mark#(U12(X)) -> active#(U12(mark(X))) p16: mark#(U11(X1,X2)) -> mark#(X1) p17: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> mark#(X2) p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U11(X1,X2)) -> mark#(X1) p5: mark#(U12(X)) -> active#(U12(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(isNat(X)) -> active#(isNat(X)) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p9: mark#(U21(X)) -> active#(U21(mark(X))) p10: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p11: mark#(U21(X)) -> mark#(X) p12: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p13: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p14: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p15: mark#(s(X)) -> active#(s(mark(X))) p16: mark#(s(X)) -> mark#(X) p17: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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: max/plus interpretations on natural numbers: mark#_A(x1) = max{0, x1 - 4} plus_A(x1,x2) = max{31, x1 + 26, x2 + 25} U11_A(x1,x2) = max{37, x1 + 16, x2 + 36} active#_A(x1) = max{7, x1 - 4} mark_A(x1) = x1 U41_A(x1,x2,x3) = max{31, x1 + 13, x2 + 25, x3 + 26} tt_A = 10 U42_A(x1,x2,x3) = max{31, x1 + 14, x2 + 25, x3 + 26} isNat_A(x1) = x1 + 12 U12_A(x1) = max{20, x1 + 17} s_A(x1) = max{11, x1} U21_A(x1) = max{11, x1} U31_A(x1,x2) = max{x1 + 13, x2 + 12} active_A(x1) = x1 |0|_A = 1 precedence: U11 > mark# = active# = U41 = s = |0| > plus = U21 > U42 = U31 > mark = tt = isNat = U12 = active partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(isNat) = [] pi(U12) = [] pi(s) = [] pi(U21) = [] pi(U31) = [] pi(active) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 149 plus_A(x1,x2) = 170 U11_A(x1,x2) = 153 active#_A(x1) = 149 mark_A(x1) = 115 U41_A(x1,x2,x3) = 149 tt_A = 88 U42_A(x1,x2,x3) = 73 isNat_A(x1) = 115 U12_A(x1) = 152 s_A(x1) = 262 U21_A(x1) = 241 U31_A(x1,x2) = 57 active_A(x1) = 115 |0|_A = 89 precedence: plus = mark = tt = U42 = isNat = U12 = U31 = active = |0| > U21 > mark# = U11 = active# = U41 = s partial status: pi(mark#) = [] pi(plus) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(U41) = [] pi(tt) = [] pi(U42) = [] pi(isNat) = [] pi(U12) = [] pi(s) = [] pi(U21) = [] pi(U31) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p3: mark#(U11(X1,X2)) -> mark#(X1) p4: mark#(U12(X)) -> active#(U12(mark(X))) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p6: mark#(isNat(X)) -> active#(isNat(X)) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U21(X)) -> active#(U21(mark(X))) p9: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p10: mark#(U21(X)) -> mark#(X) p11: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p12: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p13: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p14: mark#(s(X)) -> active#(s(mark(X))) p15: mark#(s(X)) -> mark#(X) p16: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) p2: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p3: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p4: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p5: mark#(s(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(mark(X))) p7: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p10: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p11: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p12: mark#(U21(X)) -> mark#(X) p13: mark#(U21(X)) -> active#(U21(mark(X))) p14: mark#(isNat(X)) -> active#(isNat(X)) p15: mark#(U12(X)) -> active#(U12(mark(X))) p16: mark#(U11(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 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: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 23 U11_A(x1,x2) = max{27, x1, x2 + 10} active#_A(x1) = x1 + 23 mark_A(x1) = x1 plus_A(x1,x2) = max{30, x1 + 28, x2 + 13} s_A(x1) = max{17, x1} U41_A(x1,x2,x3) = max{x1 + 16, x2 + 13, x3 + 28} isNat_A(x1) = max{14, x1 - 3} U21_A(x1) = max{9, x1} U42_A(x1,x2,x3) = max{29, x1 + 16, x2 + 13, x3 + 28} tt_A = 14 U31_A(x1,x2) = max{x1 + 4, x2 + 28} U12_A(x1) = max{14, x1 + 13} active_A(x1) = max{9, x1} |0|_A = 15 precedence: mark# = U11 = active# = mark = plus = s = U41 = isNat = U21 = U42 = tt = U31 = U12 = active = |0| partial status: pi(mark#) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(plus) = [] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(active) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = 146 U11_A(x1,x2) = 145 active#_A(x1) = max{16, x1 - 2} mark_A(x1) = 183 plus_A(x1,x2) = 148 s_A(x1) = 148 U41_A(x1,x2,x3) = 148 isNat_A(x1) = 148 U21_A(x1) = 145 U42_A(x1,x2,x3) = 148 tt_A = 143 U31_A(x1,x2) = 145 U12_A(x1) = 144 active_A(x1) = 183 |0|_A = 222 precedence: U11 > U41 > U42 > mark# = active# = mark = U12 = active > plus = s = isNat = U21 = tt = U31 = |0| partial status: pi(mark#) = [] pi(U11) = [] pi(active#) = [] pi(mark) = [] pi(plus) = [] pi(s) = [] pi(U41) = [] pi(isNat) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(active) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p11: mark#(U21(X)) -> mark#(X) p12: mark#(U21(X)) -> active#(U21(mark(X))) p13: mark#(isNat(X)) -> active#(isNat(X)) p14: mark#(U12(X)) -> active#(U12(mark(X))) p15: mark#(U11(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, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(U11(X1,X2)) -> mark#(X1) p3: mark#(U12(X)) -> active#(U12(mark(X))) p4: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p5: mark#(isNat(X)) -> active#(isNat(X)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U21(X)) -> active#(U21(mark(X))) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p9: mark#(U21(X)) -> mark#(X) p10: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p11: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p12: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p13: mark#(s(X)) -> active#(s(mark(X))) p14: mark#(s(X)) -> mark#(X) p15: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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: max/plus interpretations on natural numbers: active#_A(x1) = max{34, x1 - 9} plus_A(x1,x2) = max{43, x1 + 41} s_A(x1) = max{12, x1} mark#_A(x1) = max{34, x1 - 9} U41_A(x1,x2,x3) = x3 + 41 isNat_A(x1) = x1 + 45 U11_A(x1,x2) = max{85, x1 + 3} U12_A(x1) = 48 mark_A(x1) = max{2, x1} tt_A = 47 U42_A(x1,x2,x3) = max{x1 - 4, x3 + 41} U21_A(x1) = max{44, x1} U31_A(x1,x2) = max{43, x2 + 35} active_A(x1) = max{12, x1} |0|_A = 48 precedence: isNat > plus = U21 = |0| > active# = mark# = U41 = tt = U42 > mark > active > s = U11 = U12 = U31 partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [3] pi(isNat) = [] pi(U11) = [1] pi(U12) = [] pi(mark) = [1] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(U31) = [2] pi(active) = [1] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = 3 plus_A(x1,x2) = 22 s_A(x1) = 1 mark#_A(x1) = 3 U41_A(x1,x2,x3) = x3 + 21 isNat_A(x1) = 8 U11_A(x1,x2) = x1 + 14 U12_A(x1) = 2 mark_A(x1) = 0 tt_A = 1 U42_A(x1,x2,x3) = 2 U21_A(x1) = 9 U31_A(x1,x2) = 2 active_A(x1) = max{0, x1 - 16} |0|_A = 148 precedence: active# = plus = s = mark# > U41 = isNat > U11 = U12 = mark = active = |0| > tt = U42 = U21 = U31 partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(U11) = [] pi(U12) = [] pi(mark) = [] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(U31) = [] pi(active) = [] pi(|0|) = [] 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: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(U12(X)) -> active#(U12(mark(X))) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(isNat(X)) -> active#(isNat(X)) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p6: mark#(U21(X)) -> active#(U21(mark(X))) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U21(X)) -> mark#(X) p9: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p10: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p11: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p12: mark#(s(X)) -> active#(s(mark(X))) p13: mark#(s(X)) -> mark#(X) p14: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p11: mark#(U21(X)) -> mark#(X) p12: mark#(U21(X)) -> active#(U21(mark(X))) p13: mark#(isNat(X)) -> active#(isNat(X)) p14: mark#(U12(X)) -> active#(U12(mark(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 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: max/plus interpretations on natural numbers: active#_A(x1) = max{0, x1 - 13} plus_A(x1,x2) = max{40, x1 + 29, x2 - 1} s_A(x1) = max{10, x1} mark#_A(x1) = max{10, x1 - 13} U41_A(x1,x2,x3) = max{40, x1 + 9, x2 - 1, x3 + 29} isNat_A(x1) = 29 mark_A(x1) = x1 U21_A(x1) = max{29, x1} U42_A(x1,x2,x3) = max{40, x1 + 11, x2 - 1, x3 + 29} tt_A = 21 U31_A(x1,x2) = max{28, x2 + 14} U12_A(x1) = 22 active_A(x1) = x1 U11_A(x1,x2) = max{29, x1 - 31} |0|_A = 31 precedence: isNat > plus > U41 > s = U42 > mark = tt = U12 = U11 = |0| > active# = mark# = U21 = U31 = active partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(mark) = [1] pi(U21) = [] pi(U42) = [3] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(active) = [1] pi(U11) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = 0 plus_A(x1,x2) = 236 s_A(x1) = 0 mark#_A(x1) = 0 U41_A(x1,x2,x3) = 157 isNat_A(x1) = 156 mark_A(x1) = 0 U21_A(x1) = 160 U42_A(x1,x2,x3) = 140 tt_A = 143 U31_A(x1,x2) = 0 U12_A(x1) = 160 active_A(x1) = 0 U11_A(x1,x2) = 32 |0|_A = 143 precedence: |0| > active# = s = mark# = U41 = isNat = mark = U21 = tt = U12 = active = U11 > plus = U31 > U42 partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(mark) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(U12) = [] pi(active) = [] pi(U11) = [] pi(|0|) = [] The next rules are strictly ordered: p14 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(mark(X))) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p11: mark#(U21(X)) -> mark#(X) p12: mark#(U21(X)) -> active#(U21(mark(X))) p13: mark#(isNat(X)) -> active#(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 estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U21(X)) -> active#(U21(mark(X))) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p6: mark#(U21(X)) -> mark#(X) p7: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p11: mark#(s(X)) -> active#(s(mark(X))) p12: mark#(s(X)) -> mark#(X) p13: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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: max/plus interpretations on natural numbers: active#_A(x1) = max{30, x1 + 18} plus_A(x1,x2) = x1 + 36 s_A(x1) = max{36, x1} mark#_A(x1) = max{31, x1 + 18} U41_A(x1,x2,x3) = max{x1 - 24, x3 + 36} isNat_A(x1) = 16 tt_A = 15 U42_A(x1,x2,x3) = x3 + 36 U21_A(x1) = max{12, x1} mark_A(x1) = x1 U31_A(x1,x2) = max{x1 + 17, x2} active_A(x1) = max{9, x1} U11_A(x1,x2) = 16 U12_A(x1) = max{16, x1 - 1} |0|_A = 17 precedence: plus = s = U41 = isNat = U42 = U21 > U11 > active# = mark# = tt = mark = U31 = active = U12 = |0| partial status: pi(active#) = [1] pi(plus) = [] pi(s) = [] pi(mark#) = [1] pi(U41) = [] pi(isNat) = [] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(mark) = [] pi(U31) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = x1 + 93 plus_A(x1,x2) = 49 s_A(x1) = 36 mark#_A(x1) = 142 U41_A(x1,x2,x3) = 49 isNat_A(x1) = 49 tt_A = 1 U42_A(x1,x2,x3) = 49 U21_A(x1) = 2 mark_A(x1) = 0 U31_A(x1,x2) = 0 active_A(x1) = 0 U11_A(x1,x2) = 50 U12_A(x1) = 2 |0|_A = 131 precedence: plus = s = U21 = U11 > active# = mark# = U41 = tt = U42 = mark = U31 = active = U12 = |0| > isNat partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(mark) = [] pi(U31) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(|0|) = [] The next rules are strictly ordered: p11 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U21(X)) -> active#(U21(mark(X))) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p6: mark#(U21(X)) -> mark#(X) p7: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p10: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p11: mark#(s(X)) -> mark#(X) p12: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2)) p10: mark#(U21(X)) -> mark#(X) p11: mark#(U21(X)) -> active#(U21(mark(X))) p12: mark#(isNat(X)) -> active#(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 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: max/plus interpretations on natural numbers: active#_A(x1) = x1 plus_A(x1,x2) = x1 + 13 s_A(x1) = x1 mark#_A(x1) = x1 U41_A(x1,x2,x3) = x3 + 13 isNat_A(x1) = 0 mark_A(x1) = x1 U21_A(x1) = x1 U42_A(x1,x2,x3) = max{x1 + 12, x3 + 13} tt_A = 0 U31_A(x1,x2) = max{x1 + 3, x2 + 4} active_A(x1) = x1 U11_A(x1,x2) = 0 U12_A(x1) = x1 |0|_A = 0 precedence: active# = plus = s = mark# = U41 = isNat = mark = U21 = U42 = tt = U31 = active = U11 = U12 = |0| partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(mark) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{6, x1 - 77} plus_A(x1,x2) = 159 s_A(x1) = 157 mark#_A(x1) = 82 U41_A(x1,x2,x3) = 159 isNat_A(x1) = 159 mark_A(x1) = 246 U21_A(x1) = 159 U42_A(x1,x2,x3) = 159 tt_A = 54 U31_A(x1,x2) = 157 active_A(x1) = 246 U11_A(x1,x2) = 246 U12_A(x1) = 0 |0|_A = 150 precedence: U41 > U42 = U31 > active# = plus = mark# = tt = U11 = U12 = |0| > s = isNat = mark = U21 = active partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(mark) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(U31) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(|0|) = [] The next rules are strictly ordered: p9 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U21(X)) -> mark#(X) p10: mark#(U21(X)) -> active#(U21(mark(X))) p11: mark#(isNat(X)) -> active#(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 estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: mark#(U21(X)) -> active#(U21(mark(X))) p5: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p6: mark#(U21(X)) -> mark#(X) p7: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p8: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p9: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p10: mark#(s(X)) -> mark#(X) p11: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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: max/plus interpretations on natural numbers: active#_A(x1) = x1 + 15 plus_A(x1,x2) = max{41, x1 + 39, x2 + 39} s_A(x1) = max{27, x1} mark#_A(x1) = max{26, x1 + 15} U41_A(x1,x2,x3) = max{46, x1 + 28, x2 + 39, x3 + 39} isNat_A(x1) = x1 + 11 tt_A = 8 U42_A(x1,x2,x3) = max{41, x1 + 25, x2 + 39, x3 + 39} U21_A(x1) = max{7, x1} mark_A(x1) = max{2, x1} active_A(x1) = max{6, x1} U11_A(x1,x2) = x2 + 9 U12_A(x1) = max{9, x1 - 11} U31_A(x1,x2) = max{x1 + 28, x2 + 30} |0|_A = 6 precedence: plus = s = U41 = isNat = U42 = U21 = mark = active = U11 = U12 = |0| > U31 > active# = mark# > tt partial status: pi(active#) = [1] pi(plus) = [] pi(s) = [] pi(mark#) = [1] pi(U41) = [] pi(isNat) = [] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(mark) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(U31) = [1] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{50, x1 + 3} plus_A(x1,x2) = 175 s_A(x1) = 54 mark#_A(x1) = 178 U41_A(x1,x2,x3) = 175 isNat_A(x1) = 175 tt_A = 45 U42_A(x1,x2,x3) = 175 U21_A(x1) = 140 mark_A(x1) = 163 active_A(x1) = 163 U11_A(x1,x2) = 176 U12_A(x1) = 0 U31_A(x1,x2) = 1 |0|_A = 75 precedence: plus = U31 > tt = U42 > isNat > s = U21 = mark = active = |0| > active# = mark# > U11 > U41 = U12 partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [] pi(U41) = [] pi(isNat) = [] pi(tt) = [] pi(U42) = [] pi(U21) = [] pi(mark) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(U31) = [] pi(|0|) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(isNat(X)) -> active#(isNat(X)) p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p4: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p5: mark#(U21(X)) -> mark#(X) p6: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p7: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p8: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p9: mark#(s(X)) -> mark#(X) p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N)) p2: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p3: active#(isNat(s(V1))) -> mark#(U21(isNat(V1))) p4: mark#(s(X)) -> mark#(X) p5: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3)) p6: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M))) p7: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3)) p8: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N)) p9: mark#(U21(X)) -> mark#(X) p10: mark#(isNat(X)) -> active#(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 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: standard order interpretations: active#_A(x1) = x1 plus_A(x1,x2) = ((1,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (7,1) s_A(x1) = x1 + (7,18) mark#_A(x1) = x1 + (3,0) U41_A(x1,x2,x3) = ((0,1),(0,1)) x2 + ((1,1),(0,1)) x3 + (21,19) isNat_A(x1) = ((1,0),(0,0)) x1 + (26,2) mark_A(x1) = x1 + (2,0) U21_A(x1) = ((1,1),(0,1)) x1 + (1,0) U42_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((0,1),(0,1)) x2 + ((1,1),(0,1)) x3 + (18,17) tt_A() = (25,2) active_A(x1) = x1 U11_A(x1,x2) = ((0,1),(0,1)) x1 + (28,0) U12_A(x1) = (27,2) U31_A(x1,x2) = ((1,1),(0,1)) x2 + (3,0) |0|_A() = (1,0) precedence: tt > isNat > U31 > |0| > U41 = U12 > mark > plus = U11 > U42 > mark# > s > active# = U21 = active partial status: pi(active#) = [1] pi(plus) = [1] pi(s) = [1] pi(mark#) = [1] pi(U41) = [3] pi(isNat) = [] pi(mark) = [] pi(U21) = [1] pi(U42) = [] pi(tt) = [] pi(active) = [1] pi(U11) = [] pi(U12) = [] pi(U31) = [2] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((0,1),(0,0)) x1 + (1,18) plus_A(x1,x2) = ((1,1),(0,0)) x1 + (0,18) s_A(x1) = (3,2) mark#_A(x1) = ((1,1),(1,1)) x1 + (7,8) U41_A(x1,x2,x3) = (47,45) isNat_A(x1) = (5,3) mark_A(x1) = (5,3) U21_A(x1) = (6,4) U42_A(x1,x2,x3) = (20,18) tt_A() = (4,1) active_A(x1) = x1 U11_A(x1,x2) = (4,0) U12_A(x1) = (5,3) U31_A(x1,x2) = (1,2) |0|_A() = (0,3) precedence: U21 > isNat > s = mark = active = U11 = U12 > U31 > tt > |0| > active# = plus = mark# = U41 = U42 partial status: pi(active#) = [] pi(plus) = [] pi(s) = [] pi(mark#) = [1] pi(U41) = [] pi(isNat) = [] pi(mark) = [] pi(U21) = [] pi(U42) = [] pi(tt) = [] pi(active) = [1] pi(U11) = [] pi(U12) = [] pi(U31) = [] pi(|0|) = [] The next rules are strictly ordered: p1, p3, p4, p5, p7, p8, p9, p10 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) p2: 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 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)) -> active#(plus(mark(X1),mark(X2))) p2: 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 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: max/plus interpretations on natural numbers: mark#_A(x1) = max{5, x1} plus_A(x1,x2) = max{84, x1 + 68, x2 + 63} active#_A(x1) = max{67, x1} mark_A(x1) = max{6, x1} U42_A(x1,x2,x3) = max{66, x2 + 44, x3 + 49} tt_A = 27 s_A(x1) = max{66, x1 - 19} active_A(x1) = max{21, x1} U11_A(x1,x2) = max{69, x2 + 14} U12_A(x1) = max{21, x1 + 14} isNat_A(x1) = max{21, x1} U21_A(x1) = max{65, x1 - 20} U31_A(x1,x2) = max{91, x2 + 68} U41_A(x1,x2,x3) = max{x1 + 22, x2 + 44, x3 + 66} |0|_A = 28 precedence: plus > U11 = U41 > U42 = |0| > mark > mark# = active = U12 = U21 = U31 > active# = tt = isNat > s partial status: pi(mark#) = [1] pi(plus) = [] pi(active#) = [1] pi(mark) = [1] pi(U42) = [] pi(tt) = [] pi(s) = [] pi(active) = [1] pi(U11) = [2] pi(U12) = [] pi(isNat) = [1] pi(U21) = [] pi(U31) = [2] pi(U41) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{608, x1 + 594} plus_A(x1,x2) = 214 active#_A(x1) = x1 + 419 mark_A(x1) = max{174, x1 + 10} U42_A(x1,x2,x3) = 188 tt_A = 206 s_A(x1) = 175 active_A(x1) = max{121, x1 - 3} U11_A(x1,x2) = 178 U12_A(x1) = 120 isNat_A(x1) = max{215, x1 - 49} U21_A(x1) = 112 U31_A(x1,x2) = max{215, x2 + 41} U41_A(x1,x2,x3) = 201 |0|_A = 268 precedence: isNat > mark# = plus = active# = U42 = tt = s = active = U12 = U21 = U31 = U41 = |0| > mark = U11 partial status: pi(mark#) = [1] pi(plus) = [] pi(active#) = [1] pi(mark) = [1] pi(U42) = [] pi(tt) = [] pi(s) = [] pi(active) = [] pi(U11) = [] pi(U12) = [] pi(isNat) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] 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: 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U12#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: U12# = mark = active partial status: pi(U12#) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: U12#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: U12# = mark = active partial status: pi(U12#) = [1] pi(mark) = [1] pi(active) = [1] 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isNat#_A(x1) = x1 + 2 mark_A(x1) = x1 active_A(x1) = x1 + 2 precedence: mark > active > isNat# partial status: pi(isNat#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: isNat#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: isNat# = mark = active partial status: pi(isNat#) = [1] pi(mark) = [1] pi(active) = [1] 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: max/plus interpretations on natural numbers: U42#_A(x1,x2,x3) = max{x1 + 1, x2 + 3, x3 + 1} mark_A(x1) = max{1, x1} active_A(x1) = max{1, x1} precedence: U42# = mark = active partial status: pi(U42#) = [1, 2, 3] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: U42#_A(x1,x2,x3) = max{0, x1 - 2} mark_A(x1) = max{3, x1 + 1} active_A(x1) = max{3, x1 + 1} precedence: U42# = mark = active partial status: pi(U42#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1, p2, p3, p4, p5, p6 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: s#_A(x1) = max{6, x1 + 4} mark_A(x1) = max{4, x1 + 3} active_A(x1) = max{2, x1 + 1} precedence: s# = mark = active partial status: pi(s#) = [1] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: s#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: s# = mark = active partial status: pi(s#) = [1] pi(mark) = [1] pi(active) = [1] 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: plus#_A(x1,x2) = max{4, x1 + 1, x2 + 3} mark_A(x1) = max{3, x1 + 2} active_A(x1) = max{1, x1} precedence: plus# = mark = active partial status: pi(plus#) = [1, 2] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: plus#_A(x1,x2) = max{x1 + 1, x2 + 1} mark_A(x1) = x1 active_A(x1) = x1 precedence: plus# = mark = active partial status: pi(plus#) = [1, 2] pi(mark) = [1] pi(active) = [1] 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U11#_A(x1,x2) = max{3, x1 + 1, x2 + 1} mark_A(x1) = max{2, x1 + 1} active_A(x1) = max{1, x1} precedence: U11# = mark = active partial status: pi(U11#) = [1, 2] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: U11#_A(x1,x2) = max{x1 + 1, x2 + 1} mark_A(x1) = x1 active_A(x1) = x1 precedence: U11# = mark = active partial status: pi(U11#) = [1, 2] pi(mark) = [1] pi(active) = [1] 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U21#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: U21# = mark = active partial status: pi(U21#) = [] pi(mark) = [] pi(active) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: U21#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: U21# = mark = active partial status: pi(U21#) = [1] pi(mark) = [1] pi(active) = [1] 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 monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U31#_A(x1,x2) = max{3, x1 + 1, x2 + 1} mark_A(x1) = max{2, x1 + 1} active_A(x1) = max{1, x1} precedence: U31# = mark = active partial status: pi(U31#) = [1, 2] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: U31#_A(x1,x2) = max{x1 + 1, x2 + 1} mark_A(x1) = x1 active_A(x1) = x1 precedence: U31# = mark = active partial status: pi(U31#) = [1, 2] pi(mark) = [1] pi(active) = [1] 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: max/plus interpretations on natural numbers: U41#_A(x1,x2,x3) = max{x1 + 1, x2 + 3, x3 + 1} mark_A(x1) = max{1, x1} active_A(x1) = max{1, x1} precedence: U41# = mark = active partial status: pi(U41#) = [1, 2, 3] pi(mark) = [1] pi(active) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: U41#_A(x1,x2,x3) = max{0, x1 - 2} mark_A(x1) = max{3, x1 + 1} active_A(x1) = max{3, x1 + 1} precedence: U41# = mark = active partial status: pi(U41#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1, p2, p3, p4, p5, p6 We remove them from the problem. Then no dependency pair remains.