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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(0,0)) x1 + (2,2) terms_A(x1) = (2,2) mark#_A(x1) = (4,2) cons_A(x1,x2) = (1,1) recip_A(x1) = (1,3) sqr_A(x1) = (2,7) s_A(x1) = (1,3) first_A(x1,x2) = (2,5) mark_A(x1) = (3,6) dbl_A(x1) = (2,1) add_A(x1,x2) = (2,1) |0|_A() = (0,3) active_A(x1) = (3,6) nil_A() = (1,4) precedence: terms = s > sqr = first = mark = dbl = add = |0| = active = nil > cons > active# = mark# > recip 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: p19 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: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p18: mark#(recip(X)) -> 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#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: active#(add(|0|(),X)) -> mark#(X) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p15: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (4,3) terms_A(x1) = (3,7) mark#_A(x1) = (4,6) cons_A(x1,x2) = (2,4) recip_A(x1) = (5,0) sqr_A(x1) = (3,1) s_A(x1) = (0,0) mark_A(x1) = (3,2) add_A(x1,x2) = (3,1) dbl_A(x1) = (3,3) |0|_A() = (2,0) first_A(x1,x2) = (3,3) active_A(x1) = (3,2) nil_A() = (1,3) precedence: terms = recip = sqr = s > cons > active# = mark# = mark = add = dbl = |0| = first = active = nil partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(dbl) = [] pi(|0|) = [] pi(first) = [] 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: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> active#(terms(mark(X))) p3: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p4: mark#(terms(X)) -> mark#(X) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p6: mark#(cons(X1,X2)) -> mark#(X1) p7: mark#(recip(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) p9: active#(add(|0|(),X)) -> mark#(X) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(s(X)) -> active#(s(X)) p12: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p13: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p14: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) 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: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p18: mark#(recip(X)) -> mark#(X) p19: mark#(cons(X1,X2)) -> mark#(X1) p20: mark#(terms(X)) -> mark#(X) p21: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (2,1) terms_A(x1) = (5,0) mark#_A(x1) = (2,6) cons_A(x1,x2) = (3,7) recip_A(x1) = (1,7) sqr_A(x1) = (5,5) s_A(x1) = (4,0) first_A(x1,x2) = (5,8) mark_A(x1) = (7,9) dbl_A(x1) = (5,0) add_A(x1,x2) = (5,0) |0|_A() = (6,0) active_A(x1) = (7,9) nil_A() = (0,1) precedence: terms = recip = sqr = dbl > cons > active# = mark# > first = mark = |0| = active > s = add = nil 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: p13 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: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p17: mark#(recip(X)) -> mark#(X) p18: mark#(cons(X1,X2)) -> mark#(X1) p19: mark#(terms(X)) -> mark#(X) p20: 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} -- 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#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> mark#(X1) p6: mark#(recip(X)) -> mark#(X) p7: mark#(sqr(X)) -> active#(sqr(mark(X))) p8: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p9: mark#(sqr(X)) -> mark#(X) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: active#(add(|0|(),X)) -> mark#(X) p12: mark#(add(X1,X2)) -> mark#(X1) p13: mark#(add(X1,X2)) -> mark#(X2) p14: mark#(dbl(X)) -> active#(dbl(mark(X))) p15: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p16: mark#(dbl(X)) -> mark#(X) p17: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p18: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p19: mark#(first(X1,X2)) -> mark#(X1) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = x1 + (32,5) terms_A(x1) = x1 + (32,21) mark#_A(x1) = ((1,0),(1,0)) x1 + (33,2) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (6,7) recip_A(x1) = ((1,0),(0,0)) x1 + (0,1) sqr_A(x1) = x1 + (7,1) s_A(x1) = (2,6) mark_A(x1) = ((1,0),(1,1)) x1 + (0,7) add_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (34,0) dbl_A(x1) = ((1,0),(0,0)) x1 + (34,11) |0|_A() = (34,35) first_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (34,0) active_A(x1) = x1 + (0,7) nil_A() = (68,1) precedence: recip = sqr > terms > cons > active# = mark# > dbl = |0| = first > s = mark = add = active = nil partial status: pi(active#) = [] pi(terms) = [1] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(dbl) = [] 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#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p3: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> mark#(X1) p5: mark#(recip(X)) -> mark#(X) p6: mark#(sqr(X)) -> active#(sqr(mark(X))) p7: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p8: mark#(sqr(X)) -> mark#(X) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: active#(add(|0|(),X)) -> mark#(X) p11: mark#(add(X1,X2)) -> mark#(X1) p12: mark#(add(X1,X2)) -> mark#(X2) p13: mark#(dbl(X)) -> active#(dbl(mark(X))) p14: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p15: mark#(dbl(X)) -> mark#(X) p16: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p17: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p18: mark#(first(X1,X2)) -> mark#(X1) 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: 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#(sqr(X)) -> mark#(X) p14: mark#(sqr(X)) -> active#(sqr(mark(X))) p15: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(cons(X1,X2)) -> mark#(X1) p18: mark#(terms(X)) -> mark#(X) p19: active#(sqr(s(X))) -> mark#(s(add(sqr(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 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(0,0)) x1 + (2,19) terms_A(x1) = ((1,0),(0,0)) x1 + (46,2) mark#_A(x1) = x1 + (9,11) cons_A(x1,x2) = x1 + (25,1) recip_A(x1) = x1 + (3,2) sqr_A(x1) = ((1,0),(1,1)) x1 + (10,1) s_A(x1) = (0,7) first_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (26,20) mark_A(x1) = ((1,0),(1,1)) x1 + (0,5) dbl_A(x1) = x1 + (11,10) add_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (10,9) |0|_A() = (8,1) active_A(x1) = x1 + (0,3) nil_A() = (9,1) precedence: first = |0| > dbl > s > mark = add = active = nil > terms = mark# = recip = sqr > active# > cons partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [1] pi(cons) = [] pi(recip) = [] pi(sqr) = [1] pi(s) = [] pi(first) = [2] 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#(sqr(X)) -> mark#(X) p13: mark#(sqr(X)) -> active#(sqr(mark(X))) p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p15: mark#(recip(X)) -> mark#(X) p16: mark#(cons(X1,X2)) -> mark#(X1) p17: mark#(terms(X)) -> mark#(X) p18: active#(sqr(s(X))) -> mark#(s(add(sqr(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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> mark#(X) p3: mark#(cons(X1,X2)) -> mark#(X1) p4: mark#(recip(X)) -> mark#(X) p5: mark#(sqr(X)) -> active#(sqr(mark(X))) p6: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> mark#(X2) p12: mark#(dbl(X)) -> active#(dbl(mark(X))) p13: active#(add(|0|(),X)) -> mark#(X) p14: mark#(dbl(X)) -> mark#(X) p15: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p16: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p17: mark#(first(X1,X2)) -> mark#(X2) p18: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(0,0)) x1 + (3,23) terms_A(x1) = ((1,0),(0,0)) x1 + (18,2) mark#_A(x1) = ((1,0),(0,0)) x1 + (3,23) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (4,0) recip_A(x1) = ((1,0),(0,0)) x1 + (4,5) sqr_A(x1) = ((1,0),(1,0)) x1 + (6,0) s_A(x1) = (22,6) mark_A(x1) = x1 + (0,4) add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 dbl_A(x1) = ((1,0),(0,0)) x1 + (1,24) |0|_A() = (2,0) first_A(x1,x2) = ((1,0),(0,0)) x2 + (5,24) active_A(x1) = x1 + (0,3) nil_A() = (5,0) precedence: active# = terms = mark# = sqr = s = add > |0| = first > cons > nil > recip = mark = dbl = active partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(dbl) = [] pi(|0|) = [] pi(first) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p13 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> mark#(X) p3: mark#(cons(X1,X2)) -> mark#(X1) p4: mark#(recip(X)) -> mark#(X) p5: mark#(sqr(X)) -> active#(sqr(mark(X))) p6: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) 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)) -> active#(first(mark(X1),mark(X2))) p15: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p16: mark#(first(X1,X2)) -> mark#(X2) p17: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) 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: 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#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p12: mark#(sqr(X)) -> mark#(X) p13: mark#(sqr(X)) -> active#(sqr(mark(X))) p14: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p15: mark#(recip(X)) -> mark#(X) p16: mark#(cons(X1,X2)) -> mark#(X1) p17: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((1,0),(0,0)) x1 + (0,11) terms_A(x1) = ((1,0),(0,0)) x1 + (9,10) mark#_A(x1) = x1 + (2,4) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (3,2) recip_A(x1) = ((1,0),(0,0)) x1 + (1,2) sqr_A(x1) = ((1,0),(0,0)) x1 + (3,9) s_A(x1) = (4,3) first_A(x1,x2) = ((1,0),(0,0)) x2 + (5,12) mark_A(x1) = x1 dbl_A(x1) = ((1,0),(1,0)) x1 + (8,12) add_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,8) active_A(x1) = ((1,0),(0,0)) x1 + (0,1) |0|_A() = (2,2) nil_A() = (1,1) precedence: terms = recip = s = add > sqr > active# = dbl > cons > mark# = first = mark = active = |0| = nil partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [1] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(first) = [] pi(mark) = [] pi(dbl) = [] pi(add) = [] pi(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(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: mark#(dbl(X)) -> mark#(X) p5: mark#(dbl(X)) -> active#(dbl(mark(X))) p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p7: mark#(add(X1,X2)) -> mark#(X2) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) 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: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p14: mark#(recip(X)) -> mark#(X) p15: mark#(cons(X1,X2)) -> mark#(X1) p16: 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} -- 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)) -> mark#(X1) p4: mark#(recip(X)) -> mark#(X) p5: mark#(sqr(X)) -> active#(sqr(mark(X))) p6: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> mark#(X2) p12: mark#(dbl(X)) -> active#(dbl(mark(X))) p13: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: active#_A(x1) = ((0,0),(1,0)) x1 + (5,1) terms_A(x1) = (6,3) mark#_A(x1) = (5,4) cons_A(x1,x2) = (1,2) recip_A(x1) = (0,0) sqr_A(x1) = (3,0) s_A(x1) = (2,1) mark_A(x1) = (5,3) add_A(x1,x2) = (3,2) dbl_A(x1) = (3,0) first_A(x1,x2) = (1,0) active_A(x1) = (5,3) |0|_A() = (4,0) nil_A() = (6,0) precedence: active# = mark# = sqr > terms = cons = recip > s = mark = add = dbl = first = active = |0| = nil partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(dbl) = [] pi(first) = [] pi(active) = [] 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#(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#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X)))) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> mark#(X2) p11: mark#(dbl(X)) -> active#(dbl(mark(X))) p12: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p13: mark#(dbl(X)) -> mark#(X) p14: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) 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#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(dbl(s(X))) -> mark#(s(s(dbl(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#(sqr(s(X))) -> mark#(s(add(sqr(X),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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = x1 + (1,24) terms_A(x1) = ((1,0),(1,1)) x1 + (21,47) first_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (23,25) active#_A(x1) = ((1,0),(1,1)) x1 mark_A(x1) = ((1,0),(1,1)) x1 + (0,5) add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (16,11) s_A(x1) = (15,1) dbl_A(x1) = x1 + (18,0) sqr_A(x1) = ((1,0),(1,0)) x1 + (2,0) recip_A(x1) = ((1,0),(0,0)) x1 + (2,6) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (16,21) active_A(x1) = x1 + (0,5) |0|_A() = (0,4) nil_A() = (22,3) precedence: dbl = sqr > s > mark = add = |0| > mark# = terms = active# = recip = cons = active = nil > first partial status: pi(mark#) = [1] pi(terms) = [1] pi(first) = [] pi(active#) = [] pi(mark) = [] pi(add) = [] pi(s) = [] pi(dbl) = [] pi(sqr) = [] pi(recip) = [] pi(cons) = [] pi(active) = [1] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p11 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(dbl(X)) -> active#(dbl(mark(X))) p7: active#(dbl(s(X))) -> mark#(s(s(dbl(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: 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#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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)) -> active#(first(mark(X1),mark(X2))) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = x1 + (2,6) terms_A(x1) = ((1,0),(1,0)) x1 + (20,21) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (15,4) recip_A(x1) = ((1,0),(0,0)) x1 + (3,4) sqr_A(x1) = ((1,0),(0,0)) x1 + (1,10) active#_A(x1) = x1 + (0,4) mark_A(x1) = ((1,0),(1,0)) x1 dbl_A(x1) = ((1,0),(0,0)) x1 + (3,0) s_A(x1) = (9,3) add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (3,1) first_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (16,5) active_A(x1) = ((1,0),(0,0)) x1 |0|_A() = (1,11) nil_A() = (0,0) precedence: cons > recip > terms > dbl > mark# = active# > sqr = s = |0| > mark = first = active = nil > add partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(active#) = [] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(add) = [] pi(first) = [] pi(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p12 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#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> mark#(X2) p11: mark#(dbl(X)) -> active#(dbl(mark(X))) p12: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) 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#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p4: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p5: mark#(dbl(X)) -> active#(dbl(mark(X))) p6: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p7: mark#(add(X1,X2)) -> mark#(X2) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(sqr(X)) -> active#(sqr(mark(X))) p12: mark#(recip(X)) -> mark#(X) p13: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (10,10) terms_A(x1) = (4,0) first_A(x1,x2) = (1,1) active#_A(x1) = ((0,0),(1,0)) x1 + (10,1) mark_A(x1) = (6,2) add_A(x1,x2) = (9,1) s_A(x1) = (3,0) dbl_A(x1) = (9,0) sqr_A(x1) = (8,0) recip_A(x1) = (5,0) cons_A(x1,x2) = (2,0) active_A(x1) = (6,2) |0|_A() = (7,0) nil_A() = (8,0) precedence: mark# = active# = add = dbl > terms = first = mark = s = sqr = recip = cons = active = |0| = nil partial status: pi(mark#) = [] pi(terms) = [] pi(first) = [] pi(active#) = [] pi(mark) = [] pi(add) = [] pi(s) = [] pi(dbl) = [] pi(sqr) = [] pi(recip) = [] pi(cons) = [] pi(active) = [] pi(|0|) = [] 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#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p4: mark#(dbl(X)) -> active#(dbl(mark(X))) p5: active#(dbl(s(X))) -> mark#(s(s(dbl(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: mark#(sqr(X)) -> mark#(X) p10: mark#(sqr(X)) -> active#(sqr(mark(X))) p11: mark#(recip(X)) -> mark#(X) p12: 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} -- 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#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(add(X1,X2)) -> mark#(X2) p11: mark#(dbl(X)) -> active#(dbl(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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = (5,2) terms_A(x1) = (0,0) cons_A(x1,x2) = (3,0) recip_A(x1) = (5,2) sqr_A(x1) = (0,0) active#_A(x1) = ((0,0),(1,0)) x1 + (5,1) mark_A(x1) = (0,0) dbl_A(x1) = (1,0) s_A(x1) = (4,0) add_A(x1,x2) = (1,1) first_A(x1,x2) = (2,0) active_A(x1) = (0,0) |0|_A() = (2,0) nil_A() = (1,0) precedence: cons = recip = sqr > mark# = terms = active# = mark = dbl = first = active > add > s = |0| = nil partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(active#) = [] pi(mark) = [] pi(dbl) = [] pi(s) = [] pi(add) = [] pi(first) = [] pi(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: active#(dbl(s(X))) -> mark#(s(s(dbl(X)))) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(dbl(X)) -> active#(dbl(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#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> active#(dbl(mark(X))) p4: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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#(sqr(X)) -> mark#(X) p10: mark#(recip(X)) -> mark#(X) p11: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(1,1)) x1 + (0,2) terms_A(x1) = x1 + (4,1) first_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (3,1) dbl_A(x1) = ((0,0),(1,0)) x1 + (0,4) active#_A(x1) = (0,3) mark_A(x1) = ((1,0),(1,1)) x1 add_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (1,4) s_A(x1) = (0,0) sqr_A(x1) = ((1,0),(1,1)) x1 + (1,9) recip_A(x1) = ((1,0),(1,1)) x1 + (1,3) cons_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (1,3) active_A(x1) = x1 |0|_A() = (0,1) nil_A() = (0,0) precedence: add > mark = sqr = recip = cons = |0| > terms = nil > first = s = active > dbl > active# > mark# partial status: pi(mark#) = [1] pi(terms) = [1] pi(first) = [] pi(dbl) = [] pi(active#) = [] pi(mark) = [1] pi(add) = [2] pi(s) = [] pi(sqr) = [1] pi(recip) = [] pi(cons) = [1] pi(active) = [1] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p8 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> active#(dbl(mark(X))) p4: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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: mark#(sqr(X)) -> mark#(X) p9: mark#(recip(X)) -> mark#(X) p10: 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} -- 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)) -> mark#(X) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> mark#(X2) p9: mark#(dbl(X)) -> active#(dbl(mark(X))) p10: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = x1 + (1,14) terms_A(x1) = x1 + (28,13) cons_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (9,15) recip_A(x1) = x1 + (9,13) sqr_A(x1) = ((1,0),(1,1)) x1 + (9,12) add_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + (9,11) active#_A(x1) = ((1,0),(1,0)) x1 + (0,1) mark_A(x1) = ((1,0),(1,1)) x1 + (0,12) s_A(x1) = (6,1) dbl_A(x1) = (7,18) first_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (31,7) active_A(x1) = x1 + (0,8) |0|_A() = (0,0) nil_A() = (1,1) precedence: dbl > terms = add > mark > recip > mark# = cons = active# = first = |0| = nil > sqr = s = active partial status: pi(mark#) = [1] pi(terms) = [1] pi(cons) = [1] pi(recip) = [1] pi(sqr) = [] pi(add) = [1] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(dbl) = [] pi(first) = [] pi(active) = [1] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p9 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: mark#(sqr(X)) -> mark#(X) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> mark#(X2) p9: 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} -- 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#(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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(recip(X)) -> mark#(X) p9: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(1,0)) x1 + (0,1) terms_A(x1) = ((1,0),(1,1)) x1 + (18,11) first_A(x1,x2) = x1 + x2 + (35,18) add_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (20,13) active#_A(x1) = (5,14) mark_A(x1) = ((1,0),(1,1)) x1 + (0,22) s_A(x1) = ((0,0),(1,0)) x1 + (4,6) sqr_A(x1) = ((1,0),(1,0)) x1 + (3,19) recip_A(x1) = ((1,0),(1,0)) x1 + (1,21) cons_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (13,23) active_A(x1) = x1 + (0,12) |0|_A() = (2,10) dbl_A(x1) = ((1,0),(1,0)) x1 + (20,21) nil_A() = (1,1) precedence: terms = first = s = recip = dbl > mark# = add = active# = mark = sqr > cons > active = |0| = nil partial status: pi(mark#) = [] pi(terms) = [] pi(first) = [] pi(add) = [2] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(sqr) = [] pi(recip) = [] pi(cons) = [] pi(active) = [1] pi(|0|) = [] pi(dbl) = [] 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#(terms(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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(recip(X)) -> mark#(X) p8: 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} -- 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)) -> mark#(X) p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(1,1)) x1 + (1,1) terms_A(x1) = ((1,0),(1,1)) x1 + (8,11) cons_A(x1,x2) = ((1,0),(1,1)) x1 + (2,1) recip_A(x1) = x1 + (2,2) sqr_A(x1) = ((1,0),(1,1)) x1 + (3,2) add_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (5,17) active#_A(x1) = (4,16) mark_A(x1) = x1 s_A(x1) = (2,12) active_A(x1) = x1 |0|_A() = (1,0) dbl_A(x1) = x1 + (3,0) first_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (3,13) nil_A() = (2,13) precedence: mark = s = active = nil > terms > mark# = cons = recip = sqr = add = active# = |0| = dbl = first partial status: pi(mark#) = [1] pi(terms) = [1] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(add) = [] pi(active#) = [] pi(mark) = [] pi(s) = [] pi(active) = [] pi(|0|) = [] pi(dbl) = [1] 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#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(recip(X)) -> mark#(X) p4: mark#(sqr(X)) -> mark#(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, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(sqr(X)) -> mark#(X) p5: mark#(recip(X)) -> mark#(X) p6: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((0,0),(1,0)) x1 + (2,2) terms_A(x1) = ((1,0),(0,0)) x1 + (3,1) add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (3,3) sqr_A(x1) = ((1,0),(0,0)) x1 + (3,3) recip_A(x1) = ((1,0),(1,1)) x1 + (3,3) cons_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,1) precedence: terms = add > recip > mark# = sqr > cons partial status: pi(mark#) = [] pi(terms) = [] pi(add) = [] pi(sqr) = [] pi(recip) = [] pi(cons) = [2] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(recip(X)) -> mark#(X) p5: 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} -- 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#(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 set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 + (1,1) terms_A(x1) = x1 + (2,2) cons_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,2) recip_A(x1) = x1 + (2,2) add_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (2,2) precedence: terms = cons > mark# = recip = add partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [2] pi(recip) = [1] pi(add) = [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#(cons(X1,X2)) -> mark#(X1) p2: mark#(recip(X)) -> mark#(X) p3: mark#(add(X1,X2)) -> mark#(X1) p4: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(add(X1,X2)) -> mark#(X2) p3: mark#(add(X1,X2)) -> mark#(X1) p4: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 cons_A(x1,x2) = x1 + x2 + (1,1) add_A(x1,x2) = x1 + x2 + (1,1) recip_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: cons > mark# = add = recip partial status: pi(mark#) = [] pi(cons) = [1, 2] pi(add) = [1, 2] pi(recip) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(cons(X1,X2)) -> mark#(X1) p2: mark#(add(X1,X2)) -> mark#(X2) 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 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#(cons(X1,X2)) -> mark#(X1) p2: mark#(add(X1,X2)) -> mark#(X1) p3: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 cons_A(x1,x2) = x1 + x2 + (1,1) add_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,1) precedence: cons = add > mark# partial status: pi(mark#) = [] pi(cons) = [2] pi(add) = [] 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) p2: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(add(X1,X2)) -> mark#(X1) p2: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(0,0)) x1 add_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (1,1) precedence: add > mark# partial status: pi(mark#) = [] 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#(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: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: mark#_A(x1) = ((1,0),(1,1)) x1 add_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,1) precedence: mark# = add partial status: pi(mark#) = [1] 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: cons#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,3) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: cons# = mark > active partial status: pi(cons#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: cons#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (2,2) mark_A(x1) = ((1,0),(0,0)) x1 + (3,1) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: cons# = mark = active partial status: pi(cons#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cons#(mark(X1),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#(mark(X1),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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: cons#_A(x1,x2) = x1 mark_A(x1) = ((1,0),(1,0)) x1 + (1,1) active_A(x1) = x1 + (1,1) precedence: mark > cons# > active partial status: pi(cons#) = [1] pi(mark) = [] 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) 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#(mark(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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: cons#_A(x1,x2) = x1 mark_A(x1) = x1 + (1,1) precedence: cons# = mark partial status: pi(cons#) = [] pi(mark) = [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: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: recip#_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (2,2) precedence: recip# = mark = active partial status: pi(recip#) = [] pi(mark) = [1] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: recip#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: recip# = active partial status: pi(recip#) = [] 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: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: sqr#_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (2,2) precedence: sqr# = mark = active partial status: pi(sqr#) = [] pi(mark) = [1] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: sqr#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: sqr# = active partial status: pi(sqr#) = [] 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: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: terms#_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (2,2) precedence: terms# = mark = active partial status: pi(terms#) = [] pi(mark) = [1] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: terms#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: terms# = active partial status: pi(terms#) = [] 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: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: s#_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (2,2) precedence: s# = mark = active partial status: pi(s#) = [] pi(mark) = [1] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: s#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: s# = active partial status: pi(s#) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: add#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,3) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: add# = mark > active partial status: pi(add#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: add#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: add# = mark = active partial status: pi(add#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: add#(mark(X1),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#(mark(X1),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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: add#_A(x1,x2) = x1 mark_A(x1) = ((1,0),(1,0)) x1 + (1,1) active_A(x1) = x1 + (1,1) precedence: mark > add# > active partial status: pi(add#) = [1] pi(mark) = [] 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) 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#(mark(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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: add#_A(x1,x2) = x1 mark_A(x1) = x1 + (1,1) precedence: add# = mark partial status: pi(add#) = [] pi(mark) = [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: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: dbl#_A(x1) = ((1,0),(0,0)) x1 + (1,1) mark_A(x1) = x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (2,2) precedence: dbl# = mark = active partial status: pi(dbl#) = [] pi(mark) = [1] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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 reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: dbl#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: dbl# = active partial status: pi(dbl#) = [] 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: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: first#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,3) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: first# = mark > active partial status: pi(first#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: first#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,2) mark_A(x1) = ((1,0),(0,0)) x1 + (2,1) active_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: first# = mark = active partial status: pi(first#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: first#(mark(X1),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#(mark(X1),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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: first#_A(x1,x2) = x1 mark_A(x1) = ((1,0),(1,0)) x1 + (1,1) active_A(x1) = x1 + (1,1) precedence: mark > first# > active partial status: pi(first#) = [1] pi(mark) = [] 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) 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#(mark(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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: first#_A(x1,x2) = x1 mark_A(x1) = x1 + (1,1) precedence: first# = mark partial status: pi(first#) = [] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.