YES We show the termination of the TRS R: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) active(sqr(|0|())) -> mark(|0|()) active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) active(dbl(|0|())) -> mark(|0|()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(add(|0|(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(first(|0|(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) mark(terms(X)) -> active(terms(mark(X))) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(recip(X)) -> active(recip(mark(X))) mark(sqr(X)) -> active(sqr(mark(X))) mark(s(X)) -> active(s(X)) mark(|0|()) -> active(|0|()) mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) mark(dbl(X)) -> active(dbl(mark(X))) mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) mark(nil()) -> active(nil()) terms(mark(X)) -> terms(X) terms(active(X)) -> terms(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) recip(mark(X)) -> recip(X) recip(active(X)) -> recip(X) sqr(mark(X)) -> sqr(X) sqr(active(X)) -> sqr(X) s(mark(X)) -> s(X) s(active(X)) -> s(X) add(mark(X1),X2) -> add(X1,X2) add(X1,mark(X2)) -> add(X1,X2) add(active(X1),X2) -> add(X1,X2) add(X1,active(X2)) -> add(X1,X2) dbl(mark(X)) -> dbl(X) dbl(active(X)) -> dbl(X) first(mark(X1),X2) -> first(X1,X2) first(X1,mark(X2)) -> first(X1,X2) first(active(X1),X2) -> first(X1,X2) first(X1,active(X2)) -> first(X1,X2) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: active#(terms(N)) -> cons#(recip(sqr(N)),terms(s(N))) p3: active#(terms(N)) -> recip#(sqr(N)) p4: active#(terms(N)) -> sqr#(N) p5: active#(terms(N)) -> terms#(s(N)) p6: active#(terms(N)) -> s#(N) p7: active#(sqr(|0|())) -> mark#(|0|()) p8: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p9: active#(sqr(s(X))) -> s#(add(sqr(X),dbl(X))) p10: active#(sqr(s(X))) -> add#(sqr(X),dbl(X)) p11: active#(sqr(s(X))) -> sqr#(X) p12: active#(sqr(s(X))) -> dbl#(X) p13: active#(dbl(|0|())) -> mark#(|0|()) p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p15: active#(dbl(s(X))) -> s#(s(dbl(X))) p16: active#(dbl(s(X))) -> s#(dbl(X)) p17: active#(dbl(s(X))) -> dbl#(X) p18: active#(add(|0|(),X)) -> mark#(X) p19: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p20: active#(add(s(X),Y)) -> s#(add(X,Y)) p21: active#(add(s(X),Y)) -> add#(X,Y) p22: active#(first(|0|(),X)) -> mark#(nil()) p23: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p24: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z)) p25: active#(first(s(X),cons(Y,Z))) -> first#(X,Z) p26: mark#(terms(X)) -> active#(terms(mark(X))) p27: mark#(terms(X)) -> terms#(mark(X)) p28: mark#(terms(X)) -> mark#(X) p29: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p30: mark#(cons(X1,X2)) -> cons#(mark(X1),X2) p31: mark#(cons(X1,X2)) -> mark#(X1) p32: mark#(recip(X)) -> active#(recip(mark(X))) p33: mark#(recip(X)) -> recip#(mark(X)) p34: mark#(recip(X)) -> mark#(X) p35: mark#(sqr(X)) -> active#(sqr(mark(X))) p36: mark#(sqr(X)) -> sqr#(mark(X)) p37: mark#(sqr(X)) -> mark#(X) p38: mark#(s(X)) -> active#(s(X)) p39: mark#(|0|()) -> active#(|0|()) p40: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p41: mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) p42: mark#(add(X1,X2)) -> mark#(X1) p43: mark#(add(X1,X2)) -> mark#(X2) p44: mark#(dbl(X)) -> active#(dbl(mark(X))) p45: mark#(dbl(X)) -> dbl#(mark(X)) p46: mark#(dbl(X)) -> mark#(X) p47: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p48: mark#(first(X1,X2)) -> first#(mark(X1),mark(X2)) p49: mark#(first(X1,X2)) -> mark#(X1) p50: mark#(first(X1,X2)) -> mark#(X2) p51: mark#(nil()) -> active#(nil()) p52: terms#(mark(X)) -> terms#(X) p53: terms#(active(X)) -> terms#(X) p54: cons#(mark(X1),X2) -> cons#(X1,X2) p55: cons#(X1,mark(X2)) -> cons#(X1,X2) p56: cons#(active(X1),X2) -> cons#(X1,X2) p57: cons#(X1,active(X2)) -> cons#(X1,X2) p58: recip#(mark(X)) -> recip#(X) p59: recip#(active(X)) -> recip#(X) p60: sqr#(mark(X)) -> sqr#(X) p61: sqr#(active(X)) -> sqr#(X) p62: s#(mark(X)) -> s#(X) p63: s#(active(X)) -> s#(X) p64: add#(mark(X1),X2) -> add#(X1,X2) p65: add#(X1,mark(X2)) -> add#(X1,X2) p66: add#(active(X1),X2) -> add#(X1,X2) p67: add#(X1,active(X2)) -> add#(X1,X2) p68: dbl#(mark(X)) -> dbl#(X) p69: dbl#(active(X)) -> dbl#(X) p70: first#(mark(X1),X2) -> first#(X1,X2) p71: first#(X1,mark(X2)) -> first#(X1,X2) p72: first#(active(X1),X2) -> first#(X1,X2) p73: first#(X1,active(X2)) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p8, p14, p18, p19, p23, p26, p28, p29, p31, p32, p34, p35, p37, p38, p40, p42, p43, p44, p46, p47, p49, p50} {p54, p55, p56, p57} {p58, p59} {p60, p61} {p52, p53} {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#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(dbl(X)) -> mark#(X) p7: mark#(dbl(X)) -> active#(dbl(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(add(|0|(),X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p15: mark#(sqr(X)) -> mark#(X) p16: mark#(sqr(X)) -> active#(sqr(mark(X))) p17: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p18: mark#(recip(X)) -> mark#(X) p19: mark#(recip(X)) -> active#(recip(mark(X))) p20: mark#(cons(X1,X2)) -> mark#(X1) p21: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p22: mark#(terms(X)) -> mark#(X) p23: mark#(terms(X)) -> active#(terms(mark(X))) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{76, x1 - 40} terms_A(x1) = x1 + 387 mark#_A(x1) = max{18, x1 + 14} cons_A(x1,x2) = x1 + 116 recip_A(x1) = x1 + 76 sqr_A(x1) = max{98, x1 + 59} s_A(x1) = 78 first_A(x1,x2) = max{x1 + 101, x2 + 101} mark_A(x1) = x1 dbl_A(x1) = x1 + 299 add_A(x1,x2) = max{136, x1 + 133, x2 + 133} |0|_A = 99 active_A(x1) = max{60, x1} nil_A = 100 precedence: cons = sqr = mark = active = nil > |0| > active# = mark# = recip = s = first = dbl = add > terms partial status: pi(active#) = [] pi(terms) = [1] pi(mark#) = [1] pi(cons) = [] pi(recip) = [1] pi(sqr) = [] pi(s) = [] pi(first) = [] pi(mark) = [] pi(dbl) = [] pi(add) = [1, 2] pi(|0|) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p17 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(dbl(X)) -> mark#(X) p7: mark#(dbl(X)) -> active#(dbl(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(add(|0|(),X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p15: mark#(sqr(X)) -> mark#(X) p16: mark#(sqr(X)) -> active#(sqr(mark(X))) p17: mark#(recip(X)) -> mark#(X) p18: mark#(recip(X)) -> active#(recip(mark(X))) p19: mark#(cons(X1,X2)) -> mark#(X1) p20: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p21: mark#(terms(X)) -> mark#(X) p22: mark#(terms(X)) -> active#(terms(mark(X))) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> active#(terms(mark(X))) p3: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(add(|0|(),X)) -> mark#(X) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> active#(recip(mark(X))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p10: mark#(recip(X)) -> mark#(X) p11: mark#(sqr(X)) -> active#(sqr(mark(X))) p12: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p13: mark#(sqr(X)) -> mark#(X) p14: mark#(s(X)) -> active#(s(X)) p15: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p16: mark#(add(X1,X2)) -> mark#(X1) p17: mark#(add(X1,X2)) -> mark#(X2) p18: mark#(dbl(X)) -> active#(dbl(mark(X))) p19: mark#(dbl(X)) -> mark#(X) p20: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p21: mark#(first(X1,X2)) -> mark#(X1) p22: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{96, x1 - 127} terms_A(x1) = max{392, x1 + 366} mark#_A(x1) = x1 + 89 cons_A(x1,x2) = max{176, x1} recip_A(x1) = max{45, x1} sqr_A(x1) = x1 + 21 s_A(x1) = 7 mark_A(x1) = x1 + 39 dbl_A(x1) = x1 + 100 add_A(x1,x2) = max{x1, x2 + 216} |0|_A = 7 first_A(x1,x2) = max{x1 + 205, x2 + 216} active_A(x1) = max{46, x1} nil_A = 172 precedence: terms = cons = recip = s = mark = active = nil > first > active# = mark# > sqr = |0| > dbl = add partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(dbl) = [1] pi(add) = [2] pi(|0|) = [] pi(first) = [] pi(active) = [] pi(nil) = [] 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#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p3: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p5: active#(add(|0|(),X)) -> mark#(X) p6: mark#(cons(X1,X2)) -> mark#(X1) p7: mark#(recip(X)) -> active#(recip(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(recip(X)) -> mark#(X) p10: mark#(sqr(X)) -> active#(sqr(mark(X))) p11: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p12: mark#(sqr(X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p15: mark#(add(X1,X2)) -> mark#(X1) p16: mark#(add(X1,X2)) -> mark#(X2) p17: mark#(dbl(X)) -> active#(dbl(mark(X))) p18: mark#(dbl(X)) -> mark#(X) p19: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p20: mark#(first(X1,X2)) -> mark#(X1) p21: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(dbl(X)) -> mark#(X) p7: mark#(dbl(X)) -> active#(dbl(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(add(|0|(),X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p15: mark#(sqr(X)) -> mark#(X) p16: mark#(sqr(X)) -> active#(sqr(mark(X))) p17: mark#(recip(X)) -> mark#(X) p18: mark#(recip(X)) -> active#(recip(mark(X))) p19: mark#(cons(X1,X2)) -> mark#(X1) p20: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p21: mark#(terms(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{20, x1 - 22} terms_A(x1) = max{103, x1 + 63} mark#_A(x1) = x1 + 20 cons_A(x1,x2) = x1 + 21 recip_A(x1) = x1 sqr_A(x1) = max{40, x1} s_A(x1) = 0 first_A(x1,x2) = max{46, x1 + 38, x2 + 42} mark_A(x1) = x1 + 22 dbl_A(x1) = x1 add_A(x1,x2) = max{x1, x2 + 42} |0|_A = 0 active_A(x1) = max{22, x1} nil_A = 23 precedence: s = first > nil > active# = terms = mark# = cons = |0| > recip = sqr = mark = dbl = add = active partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(first) = [] pi(mark) = [] pi(dbl) = [] pi(add) = [] pi(|0|) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(add(|0|(),X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(recip(X)) -> active#(recip(mark(X))) p18: mark#(cons(X1,X2)) -> mark#(X1) p19: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p20: mark#(terms(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> mark#(X) p3: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(cons(X1,X2)) -> mark#(X1) p6: mark#(recip(X)) -> active#(recip(mark(X))) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p15: mark#(add(X1,X2)) -> mark#(X1) p16: mark#(add(X1,X2)) -> mark#(X2) p17: mark#(dbl(X)) -> active#(dbl(mark(X))) p18: mark#(dbl(X)) -> mark#(X) p19: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p20: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: active#_A(x1) = max{14, x1 - 16} terms_A(x1) = x1 + 283 mark#_A(x1) = max{14, x1 - 16} cons_A(x1,x2) = max{x1 + 205, x2 - 140} recip_A(x1) = x1 + 15 sqr_A(x1) = x1 + 62 s_A(x1) = 11 mark_A(x1) = x1 dbl_A(x1) = max{13, x1} add_A(x1,x2) = max{x1, x2 + 31} |0|_A = 12 first_A(x1,x2) = max{550, x2 + 345} active_A(x1) = max{11, x1} nil_A = 344 precedence: active# = terms = mark# = cons = recip = sqr = s = mark = dbl = add = |0| = first = active = nil partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [1] pi(dbl) = [] pi(add) = [] pi(|0|) = [] pi(first) = [] pi(active) = [1] pi(nil) = [] 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#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p3: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p4: mark#(cons(X1,X2)) -> mark#(X1) p5: mark#(recip(X)) -> active#(recip(mark(X))) p6: active#(add(|0|(),X)) -> mark#(X) p7: mark#(recip(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(s(X)) -> active#(s(X)) p12: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p13: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p14: mark#(add(X1,X2)) -> mark#(X1) p15: mark#(add(X1,X2)) -> mark#(X2) p16: mark#(dbl(X)) -> active#(dbl(mark(X))) p17: mark#(dbl(X)) -> mark#(X) p18: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p19: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(add(|0|(),X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(recip(X)) -> active#(recip(mark(X))) p18: mark#(cons(X1,X2)) -> mark#(X1) p19: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 7 terms_A(x1) = x1 + 193 first_A(x1,x2) = max{x1 + 251, x2 + 249} active#_A(x1) = max{6, x1 - 26} mark_A(x1) = x1 + 25 s_A(x1) = 33 cons_A(x1,x2) = x1 + 6 dbl_A(x1) = x1 + 67 add_A(x1,x2) = max{x1 + 1, x2 + 68} |0|_A = 31 sqr_A(x1) = x1 + 161 recip_A(x1) = max{6, x1} active_A(x1) = max{2, x1} nil_A = 242 precedence: terms = mark > mark# = first = active# = s = cons = dbl = add = |0| = sqr = recip = active = nil partial status: pi(mark#) = [1] pi(terms) = [1] pi(first) = [2] pi(active#) = [] pi(mark) = [1] pi(s) = [] pi(cons) = [] pi(dbl) = [] pi(add) = [] pi(|0|) = [] pi(sqr) = [] pi(recip) = [1] pi(active) = [1] pi(nil) = [] The next rules are strictly ordered: p19 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(add(|0|(),X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(recip(X)) -> active#(recip(mark(X))) p18: mark#(cons(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> active#(recip(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(recip(X)) -> mark#(X) p6: mark#(sqr(X)) -> active#(sqr(mark(X))) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(sqr(X)) -> mark#(X) p9: mark#(s(X)) -> active#(s(X)) p10: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p13: mark#(add(X1,X2)) -> mark#(X1) p14: mark#(add(X1,X2)) -> mark#(X2) p15: mark#(dbl(X)) -> active#(dbl(mark(X))) p16: mark#(dbl(X)) -> mark#(X) p17: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p18: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 16 terms_A(x1) = x1 + 195 cons_A(x1,x2) = x1 + 12 recip_A(x1) = max{165, x1} active#_A(x1) = max{9, x1 - 2} mark_A(x1) = x1 + 18 dbl_A(x1) = x1 + 101 s_A(x1) = 0 sqr_A(x1) = x1 + 165 add_A(x1,x2) = max{26, x1 + 11, x2 + 18} |0|_A = 26 first_A(x1,x2) = max{x1 + 26, x2 + 34} active_A(x1) = x1 nil_A = 33 precedence: recip > |0| > cons = s = add > mark# = terms = active# = mark = dbl = sqr = first = active = nil partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(active#) = [] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(sqr) = [] pi(add) = [] pi(|0|) = [] pi(first) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p10 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> active#(recip(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(recip(X)) -> mark#(X) p6: mark#(sqr(X)) -> active#(sqr(mark(X))) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(sqr(X)) -> mark#(X) p9: mark#(s(X)) -> active#(s(X)) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p12: mark#(add(X1,X2)) -> mark#(X1) p13: mark#(add(X1,X2)) -> mark#(X2) p14: mark#(dbl(X)) -> active#(dbl(mark(X))) p15: mark#(dbl(X)) -> mark#(X) p16: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p17: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p12: mark#(s(X)) -> active#(s(X)) p13: mark#(sqr(X)) -> mark#(X) p14: mark#(sqr(X)) -> active#(sqr(mark(X))) p15: mark#(recip(X)) -> mark#(X) p16: mark#(recip(X)) -> active#(recip(mark(X))) p17: mark#(cons(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 5 terms_A(x1) = max{78, x1 + 38} first_A(x1,x2) = max{46, x1 + 40, x2 + 38} active#_A(x1) = max{1, x1 - 4} mark_A(x1) = x1 s_A(x1) = max{6, x1 - 9} cons_A(x1,x2) = x1 + 6 dbl_A(x1) = x1 + 16 add_A(x1,x2) = max{x1, x2 + 9} |0|_A = 11 sqr_A(x1) = x1 + 25 recip_A(x1) = max{71, x1 + 7} active_A(x1) = max{6, x1} nil_A = 37 precedence: first = add = recip > active# = s = dbl > terms > mark# = mark = cons = |0| = sqr = active = nil partial status: pi(mark#) = [1] pi(terms) = [] pi(first) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(cons) = [] pi(dbl) = [] pi(add) = [] pi(|0|) = [] pi(sqr) = [] pi(recip) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p16 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p12: mark#(s(X)) -> active#(s(X)) p13: mark#(sqr(X)) -> mark#(X) p14: mark#(sqr(X)) -> active#(sqr(mark(X))) p15: mark#(recip(X)) -> mark#(X) p16: mark#(cons(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: mark#(sqr(X)) -> active#(sqr(mark(X))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(s(X)) -> active#(s(X)) p8: active#(add(|0|(),X)) -> mark#(X) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p11: mark#(add(X1,X2)) -> mark#(X1) p12: mark#(add(X1,X2)) -> mark#(X2) p13: mark#(dbl(X)) -> active#(dbl(mark(X))) p14: mark#(dbl(X)) -> mark#(X) p15: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p16: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 65 terms_A(x1) = max{86, x1 + 42} cons_A(x1,x2) = max{46, x1} recip_A(x1) = max{45, x1} sqr_A(x1) = max{46, x1 + 14} active#_A(x1) = max{75, x1 + 6} mark_A(x1) = x1 + 28 dbl_A(x1) = x1 + 138 s_A(x1) = 45 add_A(x1,x2) = max{x1 + 12, x2 + 65} |0|_A = 45 first_A(x1,x2) = max{x1 + 98, x2 + 155} active_A(x1) = max{73, x1} nil_A = 46 precedence: mark# = recip = sqr = mark = dbl = |0| = active = nil > first > terms > cons = active# = s = add partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(active#) = [1] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(add) = [1] pi(|0|) = [] pi(first) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p15 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: mark#(sqr(X)) -> active#(sqr(mark(X))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(s(X)) -> active#(s(X)) p8: active#(add(|0|(),X)) -> mark#(X) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p11: mark#(add(X1,X2)) -> mark#(X1) p12: mark#(add(X1,X2)) -> mark#(X2) p13: mark#(dbl(X)) -> active#(dbl(mark(X))) p14: mark#(dbl(X)) -> mark#(X) p15: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(dbl(X)) -> active#(dbl(mark(X))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(add(X1,X2)) -> mark#(X2) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(add(|0|(),X)) -> mark#(X) p10: mark#(s(X)) -> active#(s(X)) p11: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p12: mark#(sqr(X)) -> mark#(X) p13: mark#(sqr(X)) -> active#(sqr(mark(X))) p14: mark#(recip(X)) -> mark#(X) p15: mark#(cons(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{48, x1 + 14} terms_A(x1) = x1 + 348 first_A(x1,x2) = max{x1 + 425, x2 + 428} dbl_A(x1) = x1 + 114 active#_A(x1) = max{49, x1 + 7} mark_A(x1) = x1 + 6 s_A(x1) = 50 cons_A(x1,x2) = max{25, x1 + 18} add_A(x1,x2) = max{x1 + 107, x2 + 98} |0|_A = 11 sqr_A(x1) = x1 + 321 recip_A(x1) = max{47, x1 + 3} active_A(x1) = max{17, x1} nil_A = 400 precedence: s > mark# = first = active# = sqr = recip > terms = mark = cons = add = active > dbl = nil > |0| partial status: pi(mark#) = [] pi(terms) = [] pi(first) = [] pi(dbl) = [] pi(active#) = [1] pi(mark) = [] pi(s) = [] pi(cons) = [] pi(add) = [] pi(|0|) = [] pi(sqr) = [] pi(recip) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(dbl(X)) -> active#(dbl(mark(X))) p5: mark#(add(X1,X2)) -> mark#(X2) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(add(|0|(),X)) -> mark#(X) p9: mark#(s(X)) -> active#(s(X)) p10: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(sqr(X)) -> active#(sqr(mark(X))) p13: mark#(recip(X)) -> mark#(X) p14: mark#(cons(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: mark#(sqr(X)) -> active#(sqr(mark(X))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(s(X)) -> active#(s(X)) p8: active#(add(|0|(),X)) -> mark#(X) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> mark#(X2) p12: mark#(dbl(X)) -> active#(dbl(mark(X))) p13: mark#(dbl(X)) -> mark#(X) p14: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 39 terms_A(x1) = x1 + 18 cons_A(x1,x2) = max{8, x1} recip_A(x1) = x1 + 8 sqr_A(x1) = x1 + 10 active#_A(x1) = x1 + 39 mark_A(x1) = x1 dbl_A(x1) = x1 + 36 s_A(x1) = 9 add_A(x1,x2) = max{x1, x2 + 34} |0|_A = 23 first_A(x1,x2) = max{x1 + 7, x2 + 25} active_A(x1) = max{8, x1} nil_A = 24 precedence: mark# = terms = recip > cons = sqr = active# = mark = dbl = s = add = |0| = first = active = nil partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(active#) = [1] pi(mark) = [1] pi(dbl) = [] pi(s) = [] pi(add) = [] pi(|0|) = [] pi(first) = [] pi(active) = [1] pi(nil) = [] 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#(cons(X1,X2)) -> mark#(X1) p2: mark#(recip(X)) -> mark#(X) p3: mark#(sqr(X)) -> active#(sqr(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(X)) p7: active#(add(|0|(),X)) -> mark#(X) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> mark#(X2) p11: mark#(dbl(X)) -> active#(dbl(mark(X))) p12: mark#(dbl(X)) -> mark#(X) p13: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(dbl(X)) -> active#(dbl(mark(X))) p5: active#(add(|0|(),X)) -> mark#(X) p6: mark#(add(X1,X2)) -> mark#(X2) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p10: mark#(s(X)) -> active#(s(X)) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(sqr(X)) -> active#(sqr(mark(X))) p13: mark#(recip(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 19 cons_A(x1,x2) = max{x1 + 92, x2 - 54} first_A(x1,x2) = max{111, x2 + 19} dbl_A(x1) = max{32, x1 + 19} active#_A(x1) = x1 + 12 mark_A(x1) = x1 add_A(x1,x2) = max{25, x1, x2 + 19} |0|_A = 26 s_A(x1) = max{53, x1 - 29} sqr_A(x1) = x1 + 81 recip_A(x1) = x1 + 27 active_A(x1) = max{25, x1} terms_A(x1) = x1 + 200 nil_A = 27 precedence: add = |0| > first > dbl = s > recip > terms > mark# = active# = nil > cons = mark = sqr = active partial status: pi(mark#) = [1] pi(cons) = [] pi(first) = [] pi(dbl) = [] pi(active#) = [1] pi(mark) = [] pi(add) = [] pi(|0|) = [] pi(s) = [] pi(sqr) = [] pi(recip) = [] pi(active) = [] pi(terms) = [] pi(nil) = [] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(dbl(X)) -> active#(dbl(mark(X))) p5: mark#(add(X1,X2)) -> mark#(X2) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p9: mark#(s(X)) -> active#(s(X)) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(sqr(X)) -> active#(sqr(mark(X))) p12: mark#(recip(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(recip(X)) -> mark#(X) p3: mark#(sqr(X)) -> active#(sqr(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(X)) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(dbl(X)) -> active#(dbl(mark(X))) p11: mark#(dbl(X)) -> mark#(X) p12: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 8 cons_A(x1,x2) = max{x1 + 9, x2} recip_A(x1) = x1 + 9 sqr_A(x1) = max{57, x1 + 56} active#_A(x1) = max{5, x1 - 8} mark_A(x1) = x1 dbl_A(x1) = x1 + 37 s_A(x1) = 0 add_A(x1,x2) = max{x1 + 13, x2 + 20} first_A(x1,x2) = x2 + 20 active_A(x1) = x1 terms_A(x1) = x1 + 77 |0|_A = 18 nil_A = 19 precedence: mark = active = terms > mark# = recip = sqr = active# > cons > add = first = |0| = nil > dbl = s partial status: pi(mark#) = [1] pi(cons) = [1] pi(recip) = [] pi(sqr) = [] pi(active#) = [] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(add) = [1] pi(first) = [2] pi(active) = [] pi(terms) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p10 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(recip(X)) -> mark#(X) p3: mark#(sqr(X)) -> active#(sqr(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(X)) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(dbl(X)) -> mark#(X) p11: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(add(X1,X2)) -> mark#(X2) p5: mark#(add(X1,X2)) -> mark#(X1) p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p7: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p8: mark#(s(X)) -> active#(s(X)) p9: mark#(sqr(X)) -> mark#(X) p10: mark#(sqr(X)) -> active#(sqr(mark(X))) p11: mark#(recip(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 18 cons_A(x1,x2) = x1 + 5 first_A(x1,x2) = max{x1 + 18, x2} dbl_A(x1) = x1 + 6 add_A(x1,x2) = max{x1, x2 + 8} active#_A(x1) = x1 + 18 mark_A(x1) = x1 s_A(x1) = max{4, x1 - 1} sqr_A(x1) = x1 + 14 recip_A(x1) = x1 + 4 active_A(x1) = max{2, x1} terms_A(x1) = x1 + 24 |0|_A = 2 nil_A = 3 precedence: dbl = mark = active = terms = |0| > mark# = cons = first = active# > s > add = sqr = recip = nil partial status: pi(mark#) = [] pi(cons) = [1] pi(first) = [1] pi(dbl) = [] pi(add) = [2] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(sqr) = [1] pi(recip) = [1] pi(active) = [] pi(terms) = [] pi(|0|) = [] pi(nil) = [] 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#(first(X1,X2)) -> mark#(X2) p2: mark#(dbl(X)) -> mark#(X) p3: mark#(add(X1,X2)) -> mark#(X2) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p7: mark#(s(X)) -> active#(s(X)) p8: mark#(sqr(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: mark#(recip(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: mark#(first(X1,X2)) -> mark#(X2) p2: mark#(recip(X)) -> mark#(X) p3: mark#(sqr(X)) -> active#(sqr(mark(X))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(s(X)) -> active#(s(X)) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(dbl(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{0, x1 - 1} first_A(x1,x2) = max{x1 + 7, x2 + 7} recip_A(x1) = x1 + 8 sqr_A(x1) = x1 active#_A(x1) = max{0, x1 - 1} mark_A(x1) = x1 dbl_A(x1) = max{2, x1} s_A(x1) = max{0, x1 - 4} add_A(x1,x2) = max{x1, x2} active_A(x1) = x1 terms_A(x1) = x1 + 10 cons_A(x1,x2) = max{x1 + 2, x2 - 4} |0|_A = 3 nil_A = 0 precedence: |0| > terms = cons > mark# > recip > first = add > sqr = mark = dbl = active = nil > active# = s partial status: pi(mark#) = [] pi(first) = [] pi(recip) = [] pi(sqr) = [] pi(active#) = [] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(add) = [] pi(active) = [] pi(terms) = [] pi(cons) = [] pi(|0|) = [] pi(nil) = [] 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#(recip(X)) -> mark#(X) p2: mark#(sqr(X)) -> active#(sqr(mark(X))) p3: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p4: mark#(sqr(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(X)) p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(dbl(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(recip(X)) -> mark#(X) p2: mark#(dbl(X)) -> mark#(X) p3: mark#(add(X1,X2)) -> mark#(X2) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p7: mark#(s(X)) -> active#(s(X)) p8: mark#(sqr(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{60, x1 + 47} recip_A(x1) = max{66, x1 + 61} dbl_A(x1) = max{16, x1} add_A(x1,x2) = max{23, x1 + 8, x2 + 5} active#_A(x1) = max{61, x1 + 47} mark_A(x1) = max{4, x1} s_A(x1) = 15 sqr_A(x1) = max{22, x1} active_A(x1) = max{4, x1} terms_A(x1) = max{3, x1 - 1} cons_A(x1,x2) = max{2, x2 - 11} |0|_A = 14 first_A(x1,x2) = 16 nil_A = 15 precedence: mark# = recip = dbl = add = active# = mark = s = sqr = active = terms = cons = |0| = first = nil partial status: pi(mark#) = [] pi(recip) = [] pi(dbl) = [] pi(add) = [] pi(active#) = [] pi(mark) = [1] pi(s) = [] pi(sqr) = [] pi(active) = [1] pi(terms) = [] pi(cons) = [] pi(|0|) = [] pi(first) = [] pi(nil) = [] 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#(dbl(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(s(X)) -> active#(s(X)) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(sqr(X)) -> active#(sqr(mark(X))) p3: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p4: mark#(sqr(X)) -> mark#(X) p5: mark#(s(X)) -> active#(s(X)) p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{74, x1 + 63} dbl_A(x1) = max{22, x1 + 12} sqr_A(x1) = max{8, x1} active#_A(x1) = x1 + 51 mark_A(x1) = max{9, x1} s_A(x1) = 49 add_A(x1,x2) = max{25, x1 + 16, x2 + 5} active_A(x1) = max{9, x1} terms_A(x1) = max{72, x1 + 22} cons_A(x1,x2) = 21 recip_A(x1) = max{21, x1 + 11} |0|_A = 0 first_A(x1,x2) = max{5, x1 - 3} nil_A = 1 precedence: mark = active > active# > mark# > dbl = sqr = s = add = terms = cons = recip = |0| = first = nil partial status: pi(mark#) = [] pi(dbl) = [1] pi(sqr) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(add) = [2] pi(active) = [] pi(terms) = [1] pi(cons) = [] pi(recip) = [1] pi(|0|) = [] pi(first) = [] pi(nil) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p3: mark#(sqr(X)) -> mark#(X) p4: mark#(s(X)) -> active#(s(X)) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(add(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(s(X)) -> active#(s(X)) p7: mark#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{7, x1 + 3} dbl_A(x1) = max{13, x1} add_A(x1,x2) = max{94, x1 + 6, x2 + 50} active#_A(x1) = max{8, x1 - 1} mark_A(x1) = max{44, x1} s_A(x1) = 9 sqr_A(x1) = max{22, x1} active_A(x1) = max{44, x1} terms_A(x1) = max{2, x1 - 19} cons_A(x1,x2) = max{1, x1 - 109, x2 - 44} recip_A(x1) = max{1, x1 - 42} |0|_A = 0 first_A(x1,x2) = max{152, x2 + 108} nil_A = 64 precedence: dbl = sqr > add = active# > mark# = mark = active = terms > s = |0| > cons = recip > first = nil partial status: pi(mark#) = [1] pi(dbl) = [] pi(add) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(sqr) = [] pi(active) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(|0|) = [] pi(first) = [] pi(nil) = [] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(sqr(X)) -> mark#(X) p3: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(add(X1,X2)) -> mark#(X1) p6: mark#(add(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{15, x1} dbl_A(x1) = max{84, x1 + 79} sqr_A(x1) = x1 + 71 add_A(x1,x2) = max{x1 + 153, x2 + 153} active#_A(x1) = max{153, x1 - 68} mark_A(x1) = x1 + 66 s_A(x1) = 14 active_A(x1) = max{80, x1} terms_A(x1) = max{103, x1 + 65} cons_A(x1,x2) = 26 recip_A(x1) = 15 |0|_A = 115 first_A(x1,x2) = 125 nil_A = 59 precedence: |0| > mark = recip = first > sqr > mark# = dbl = add = active# > nil > s = active = terms = cons partial status: pi(mark#) = [1] pi(dbl) = [] pi(sqr) = [1] pi(add) = [1] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(active) = [1] pi(terms) = [1] pi(cons) = [] pi(recip) = [] pi(|0|) = [] pi(first) = [] pi(nil) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(sqr(X)) -> mark#(X) p3: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(add(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(dbl(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{3, x1 + 2} dbl_A(x1) = x1 add_A(x1,x2) = max{x1, x2} sqr_A(x1) = x1 + 1 precedence: mark# = dbl = add = sqr partial status: pi(mark#) = [1] pi(dbl) = [1] pi(add) = [1, 2] pi(sqr) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(add(X1,X2)) -> mark#(X2) p2: mark#(add(X1,X2)) -> mark#(X1) p3: mark#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(add(X1,X2)) -> mark#(X2) p2: mark#(sqr(X)) -> mark#(X) p3: mark#(add(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 2 add_A(x1,x2) = max{x1 + 1, x2 + 1} sqr_A(x1) = x1 precedence: mark# = add = sqr partial status: pi(mark#) = [] pi(add) = [2] pi(sqr) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(sqr(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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#(sqr(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = max{4, x1 + 3} sqr_A(x1) = x1 + 2 add_A(x1,x2) = max{x1 + 1, x2 + 1} precedence: mark# = sqr = add partial status: pi(mark#) = [] pi(sqr) = [1] pi(add) = [2] 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#(add(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(add(X1,X2)) -> mark#(X1) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: mark#_A(x1) = x1 + 2 add_A(x1,x2) = max{x1 + 1, x2 + 1} precedence: mark# = add partial status: pi(mark#) = [] pi(add) = [2] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: cons#(mark(X1),X2) -> cons#(X1,X2) p2: cons#(X1,active(X2)) -> cons#(X1,X2) p3: cons#(active(X1),X2) -> cons#(X1,X2) p4: cons#(X1,mark(X2)) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: cons#_A(x1,x2) = max{0, x2 - 2} mark_A(x1) = x1 active_A(x1) = max{3, x1 + 1} precedence: cons# = mark = active partial status: pi(cons#) = [] pi(mark) = [1] pi(active) = [1] 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: cons#(mark(X1),X2) -> cons#(X1,X2) p2: cons#(active(X1),X2) -> cons#(X1,X2) p3: cons#(X1,mark(X2)) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: cons#(mark(X1),X2) -> cons#(X1,X2) p2: cons#(X1,mark(X2)) -> cons#(X1,X2) p3: cons#(active(X1),X2) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: cons#_A(x1,x2) = max{0, x1 - 2} mark_A(x1) = max{3, x1 + 1} active_A(x1) = x1 precedence: cons# = mark = active partial status: pi(cons#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cons#(X1,mark(X2)) -> cons#(X1,X2) p2: cons#(active(X1),X2) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: cons#(X1,mark(X2)) -> cons#(X1,X2) p2: cons#(active(X1),X2) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: cons#_A(x1,x2) = x2 + 1 mark_A(x1) = x1 + 1 active_A(x1) = x1 + 1 precedence: cons# = mark = active partial status: pi(cons#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cons#(active(X1),X2) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: cons#(active(X1),X2) -> cons#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: cons#_A(x1,x2) = max{1, x1, x2} active_A(x1) = x1 + 1 precedence: cons# = active partial status: pi(cons#) = [1, 2] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: recip#(mark(X)) -> recip#(X) p2: recip#(active(X)) -> recip#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: recip#_A(x1) = max{3, x1 + 2} mark_A(x1) = x1 active_A(x1) = x1 + 1 precedence: recip# = mark = active partial status: pi(recip#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: recip#(active(X)) -> recip#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: recip#(active(X)) -> recip#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: recip#_A(x1) = x1 + 1 active_A(x1) = x1 precedence: recip# = active partial status: pi(recip#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: sqr#(mark(X)) -> sqr#(X) p2: sqr#(active(X)) -> sqr#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: sqr#_A(x1) = max{3, x1 + 2} mark_A(x1) = x1 active_A(x1) = x1 + 1 precedence: sqr# = mark = active partial status: pi(sqr#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: sqr#(active(X)) -> sqr#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: sqr#(active(X)) -> sqr#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: sqr#_A(x1) = x1 + 1 active_A(x1) = x1 precedence: sqr# = active partial status: pi(sqr#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: terms#(mark(X)) -> terms#(X) p2: terms#(active(X)) -> terms#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: terms#_A(x1) = max{3, x1 + 2} mark_A(x1) = x1 active_A(x1) = x1 + 1 precedence: terms# = mark = active partial status: pi(terms#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: terms#(active(X)) -> terms#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: terms#(active(X)) -> terms#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: terms#_A(x1) = x1 + 1 active_A(x1) = x1 precedence: terms# = active partial status: pi(terms#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: s#(mark(X)) -> s#(X) p2: s#(active(X)) -> s#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: s#_A(x1) = max{3, x1 + 2} mark_A(x1) = x1 active_A(x1) = x1 + 1 precedence: s# = mark = active partial status: pi(s#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: s#_A(x1) = x1 + 1 active_A(x1) = x1 precedence: s# = active partial status: pi(s#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: add#(mark(X1),X2) -> add#(X1,X2) p2: add#(X1,active(X2)) -> add#(X1,X2) p3: add#(active(X1),X2) -> add#(X1,X2) p4: add#(X1,mark(X2)) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: add#_A(x1,x2) = max{0, x2 - 2} mark_A(x1) = x1 active_A(x1) = max{3, x1 + 1} precedence: add# = mark = active partial status: pi(add#) = [] pi(mark) = [1] pi(active) = [1] 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: add#(mark(X1),X2) -> add#(X1,X2) p2: add#(active(X1),X2) -> add#(X1,X2) p3: add#(X1,mark(X2)) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: add#(mark(X1),X2) -> add#(X1,X2) p2: add#(X1,mark(X2)) -> add#(X1,X2) p3: add#(active(X1),X2) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: add#_A(x1,x2) = max{0, x1 - 2} mark_A(x1) = max{3, x1 + 1} active_A(x1) = x1 precedence: add# = mark = active partial status: pi(add#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: add#(X1,mark(X2)) -> add#(X1,X2) p2: add#(active(X1),X2) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: add#(X1,mark(X2)) -> add#(X1,X2) p2: add#(active(X1),X2) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: add#_A(x1,x2) = x2 + 1 mark_A(x1) = x1 + 1 active_A(x1) = x1 + 1 precedence: add# = mark = active partial status: pi(add#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: add#(active(X1),X2) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: add#(active(X1),X2) -> add#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: add#_A(x1,x2) = max{1, x1, x2} active_A(x1) = x1 + 1 precedence: add# = active partial status: pi(add#) = [1, 2] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: dbl#(mark(X)) -> dbl#(X) p2: dbl#(active(X)) -> dbl#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: dbl#_A(x1) = x1 + 1 mark_A(x1) = x1 active_A(x1) = x1 precedence: dbl# = mark = active partial status: pi(dbl#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: dbl#(active(X)) -> dbl#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: dbl#(active(X)) -> dbl#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: weighted path order base order: max/plus interpretations on natural numbers: dbl#_A(x1) = x1 + 1 active_A(x1) = x1 precedence: dbl# = active partial status: pi(dbl#) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: first#(mark(X1),X2) -> first#(X1,X2) p2: first#(X1,active(X2)) -> first#(X1,X2) p3: first#(active(X1),X2) -> first#(X1,X2) p4: first#(X1,mark(X2)) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: first#_A(x1,x2) = max{0, x2 - 2} mark_A(x1) = x1 active_A(x1) = max{3, x1 + 1} precedence: first# = mark = active partial status: pi(first#) = [] pi(mark) = [1] pi(active) = [1] 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: first#(mark(X1),X2) -> first#(X1,X2) p2: first#(active(X1),X2) -> first#(X1,X2) p3: first#(X1,mark(X2)) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: first#(mark(X1),X2) -> first#(X1,X2) p2: first#(X1,mark(X2)) -> first#(X1,X2) p3: first#(active(X1),X2) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: first#_A(x1,x2) = max{0, x1 - 2} mark_A(x1) = max{3, x1 + 1} active_A(x1) = x1 precedence: first# = mark = active partial status: pi(first#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: first#(X1,mark(X2)) -> first#(X1,X2) p2: first#(active(X1),X2) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(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: first#(X1,mark(X2)) -> first#(X1,X2) p2: first#(active(X1),X2) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: first#_A(x1,x2) = x2 + 1 mark_A(x1) = x1 + 1 active_A(x1) = x1 + 1 precedence: first# = mark = active partial status: pi(first#) = [] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: first#(active(X1),X2) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: first#(active(X1),X2) -> first#(X1,X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: first#_A(x1,x2) = max{1, x1, x2} active_A(x1) = x1 + 1 precedence: first# = active partial status: pi(first#) = [1, 2] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.