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: standard order interpretations: active#_A(x1) = ((1,0),(1,0)) x1 + (7,0) terms_A(x1) = ((1,1),(1,1)) x1 + (35,5) mark#_A(x1) = ((1,0),(1,0)) x1 + (8,2) cons_A(x1,x2) = ((1,1),(0,0)) x1 + (9,9) recip_A(x1) = ((1,1),(0,0)) x1 + (1,1) sqr_A(x1) = ((1,1),(0,0)) x1 + (9,5) s_A(x1) = (3,0) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (8,30) mark_A(x1) = ((1,1),(0,0)) x1 dbl_A(x1) = ((1,1),(1,1)) x1 + (18,18) add_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,0)) x2 + (9,12) |0|_A() = (0,0) active_A(x1) = ((1,1),(0,0)) x1 nil_A() = (6,1) precedence: recip = s = first = dbl = add > terms > active# = mark# = cons = sqr = mark = active = nil > |0| 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: p14 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: 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#(recip(X)) -> active#(recip(mark(X))) p19: mark#(cons(X1,X2)) -> mark#(X1) p20: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p21: mark#(terms(X)) -> mark#(X) p22: mark#(terms(X)) -> active#(terms(mark(X))) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> active#(terms(mark(X))) p3: active#(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#(add(|0|(),X)) -> mark#(X) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> active#(recip(mark(X))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p10: mark#(recip(X)) -> mark#(X) p11: mark#(sqr(X)) -> active#(sqr(mark(X))) p12: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p13: mark#(sqr(X)) -> mark#(X) p14: mark#(s(X)) -> active#(s(X)) p15: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p16: mark#(add(X1,X2)) -> mark#(X1) p17: mark#(add(X1,X2)) -> mark#(X2) p18: mark#(dbl(X)) -> active#(dbl(mark(X))) p19: mark#(dbl(X)) -> mark#(X) p20: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p21: mark#(first(X1,X2)) -> mark#(X1) p22: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 + (5,2) terms_A(x1) = ((1,0),(1,0)) x1 + (37,31) mark#_A(x1) = ((1,0),(1,0)) x1 + (4,0) cons_A(x1,x2) = ((1,0),(0,0)) x1 + (8,2) recip_A(x1) = ((1,0),(0,0)) x1 + (3,0) sqr_A(x1) = ((1,0),(1,0)) x1 + (20,0) s_A(x1) = (14,8) mark_A(x1) = ((1,0),(0,0)) x1 + (0,1) add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (5,0) dbl_A(x1) = ((1,0),(1,0)) x1 + (3,1) |0|_A() = (5,0) first_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (4,2) active_A(x1) = ((1,0),(0,0)) x1 + (0,1) nil_A() = (4,1) precedence: |0| > active# = mark# = recip = sqr = dbl = first > s > mark = active > cons > terms > add = 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: 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#(terms(X)) -> active#(terms(mark(X))) p3: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p5: active#(add(|0|(),X)) -> mark#(X) p6: mark#(cons(X1,X2)) -> mark#(X1) p7: mark#(recip(X)) -> active#(recip(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(recip(X)) -> mark#(X) p10: mark#(sqr(X)) -> active#(sqr(mark(X))) p11: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p12: mark#(sqr(X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p15: mark#(add(X1,X2)) -> mark#(X1) p16: mark#(add(X1,X2)) -> mark#(X2) p17: mark#(dbl(X)) -> active#(dbl(mark(X))) p18: mark#(dbl(X)) -> mark#(X) p19: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p20: mark#(first(X1,X2)) -> mark#(X1) p21: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(dbl(X)) -> mark#(X) p7: mark#(dbl(X)) -> active#(dbl(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(add(|0|(),X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(recip(X)) -> active#(recip(mark(X))) p18: mark#(cons(X1,X2)) -> mark#(X1) p19: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p20: mark#(terms(X)) -> mark#(X) 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: standard order interpretations: active#_A(x1) = ((1,0),(0,0)) x1 terms_A(x1) = ((1,1),(1,1)) x1 + (15,12) mark#_A(x1) = ((0,1),(0,0)) x1 + (4,0) cons_A(x1,x2) = ((0,0),(1,1)) x1 recip_A(x1) = ((0,0),(1,1)) x1 + (5,2) sqr_A(x1) = ((0,0),(1,1)) x1 + (3,0) s_A(x1) = (4,0) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (5,2) mark_A(x1) = ((0,0),(1,1)) x1 dbl_A(x1) = ((0,0),(1,1)) x1 + (5,8) add_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (4,1) |0|_A() = (2,0) active_A(x1) = ((0,0),(1,1)) x1 nil_A() = (1,10) precedence: terms = nil > active# = mark# = cons = recip = sqr = s = first = mark = dbl = add = |0| = active partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(first) = [] pi(mark) = [] pi(dbl) = [] pi(add) = [] pi(|0|) = [] pi(active) = [] pi(nil) = [] The next rules are strictly ordered: p17 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(dbl(X)) -> mark#(X) p7: mark#(dbl(X)) -> active#(dbl(mark(X))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p9: mark#(add(X1,X2)) -> mark#(X2) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: active#(add(|0|(),X)) -> mark#(X) p13: mark#(s(X)) -> active#(s(X)) p14: mark#(sqr(X)) -> mark#(X) p15: mark#(sqr(X)) -> active#(sqr(mark(X))) p16: mark#(recip(X)) -> mark#(X) p17: mark#(cons(X1,X2)) -> mark#(X1) p18: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) 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#(add(|0|(),X)) -> mark#(X) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(s(X)) -> active#(s(X)) p13: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p14: mark#(add(X1,X2)) -> mark#(X1) p15: mark#(add(X1,X2)) -> mark#(X2) p16: mark#(dbl(X)) -> active#(dbl(mark(X))) p17: mark#(dbl(X)) -> mark#(X) p18: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p19: mark#(first(X1,X2)) -> mark#(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: standard order interpretations: active#_A(x1) = ((0,1),(1,0)) x1 terms_A(x1) = ((1,1),(1,1)) x1 + (34,28) mark#_A(x1) = ((1,1),(1,1)) x1 + (5,2) cons_A(x1,x2) = x1 + (7,2) recip_A(x1) = ((0,1),(1,0)) x1 + (5,2) sqr_A(x1) = x1 + (4,2) s_A(x1) = (3,3) mark_A(x1) = ((1,1),(1,1)) x1 add_A(x1,x2) = ((0,1),(1,0)) x1 + ((1,1),(1,1)) x2 + (10,9) |0|_A() = (2,2) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (6,8) dbl_A(x1) = ((0,1),(1,0)) x1 + (6,2) active_A(x1) = x1 + (2,1) nil_A() = (1,11) precedence: recip = mark = active = nil > |0| > cons = sqr = first > add > active# = terms = mark# = s = dbl partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [1] pi(cons) = [] pi(recip) = [] pi(sqr) = [1] pi(s) = [] pi(mark) = [] pi(add) = [] pi(|0|) = [] pi(first) = [1] pi(dbl) = [] 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#(terms(X)) -> active#(terms(mark(X))) p3: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p5: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p6: mark#(cons(X1,X2)) -> mark#(X1) p7: mark#(recip(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) p9: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(s(X)) -> active#(s(X)) p12: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p13: mark#(add(X1,X2)) -> mark#(X1) p14: mark#(add(X1,X2)) -> mark#(X2) p15: mark#(dbl(X)) -> active#(dbl(mark(X))) p16: mark#(dbl(X)) -> mark#(X) p17: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p18: mark#(first(X1,X2)) -> mark#(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: mark#(s(X)) -> active#(s(X)) p13: mark#(sqr(X)) -> mark#(X) p14: mark#(sqr(X)) -> active#(sqr(mark(X))) p15: mark#(recip(X)) -> mark#(X) p16: mark#(cons(X1,X2)) -> mark#(X1) p17: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p18: mark#(terms(X)) -> mark#(X) p19: 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: standard order interpretations: active#_A(x1) = ((1,0),(1,1)) x1 + (11,1) terms_A(x1) = ((1,1),(0,0)) x1 + (10,11) mark#_A(x1) = ((1,1),(1,1)) x1 + (11,2) cons_A(x1,x2) = ((0,0),(1,1)) x1 + (1,2) recip_A(x1) = ((1,1),(0,0)) x1 + (1,2) sqr_A(x1) = ((1,1),(0,0)) x1 + (1,2) s_A(x1) = (0,0) first_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (12,2) mark_A(x1) = ((0,0),(1,1)) x1 dbl_A(x1) = ((1,1),(0,0)) x1 + (12,0) add_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + (0,1) active_A(x1) = ((0,0),(1,1)) x1 |0|_A() = (3,0) nil_A() = (0,0) precedence: terms > sqr = s > cons = add > mark = active = |0| > dbl > active# = mark# > recip = first = 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(active) = [] 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: 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#(X1) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: mark#(s(X)) -> active#(s(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) p16: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p17: mark#(terms(X)) -> mark#(X) p18: 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} -- 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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(s(X)) -> active#(s(X)) p12: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p13: mark#(add(X1,X2)) -> mark#(X1) p14: mark#(dbl(X)) -> active#(dbl(mark(X))) p15: mark#(dbl(X)) -> mark#(X) p16: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p17: mark#(first(X1,X2)) -> mark#(X1) p18: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = x1 terms_A(x1) = ((1,1),(0,1)) x1 + (67,20) mark#_A(x1) = ((1,1),(0,1)) x1 + (5,1) cons_A(x1,x2) = x1 + (37,6) recip_A(x1) = x1 + (1,5) sqr_A(x1) = x1 + (4,8) s_A(x1) = (36,7) mark_A(x1) = ((1,1),(0,1)) x1 add_A(x1,x2) = x1 + ((1,1),(0,1)) x2 + (12,8) first_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (0,8) dbl_A(x1) = x1 + (3,16) active_A(x1) = x1 + (5,0) |0|_A() = (2,8) nil_A() = (1,14) precedence: add > cons = mark = active > s > |0| > first > terms > mark# > sqr > nil > active# = recip = dbl partial status: pi(active#) = [1] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(first) = [] pi(dbl) = [] pi(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p14 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N)))) p2: mark#(terms(X)) -> active#(terms(mark(X))) p3: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(s(X)) -> active#(s(X)) p12: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p13: mark#(add(X1,X2)) -> mark#(X1) p14: mark#(dbl(X)) -> mark#(X) p15: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p16: mark#(first(X1,X2)) -> mark#(X1) p17: mark#(first(X1,X2)) -> mark#(X2) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) p10: mark#(s(X)) -> active#(s(X)) p11: mark#(sqr(X)) -> mark#(X) p12: mark#(sqr(X)) -> active#(sqr(mark(X))) p13: mark#(recip(X)) -> mark#(X) p14: mark#(cons(X1,X2)) -> mark#(X1) p15: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p16: mark#(terms(X)) -> mark#(X) p17: 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: standard order interpretations: active#_A(x1) = ((1,1),(0,0)) x1 + (1,0) terms_A(x1) = (1,2) mark#_A(x1) = (4,0) cons_A(x1,x2) = (0,0) recip_A(x1) = (4,3) sqr_A(x1) = (2,0) s_A(x1) = (1,1) first_A(x1,x2) = (1,2) mark_A(x1) = (1,2) dbl_A(x1) = (1,0) add_A(x1,x2) = (1,2) active_A(x1) = (1,2) |0|_A() = (0,0) nil_A() = (1,0) precedence: active# = terms = mark# = cons = recip = s = first = mark = dbl = add = active = |0| > sqr > 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(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p10 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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) p14: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p15: mark#(terms(X)) -> mark#(X) p16: 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} -- 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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p4: mark#(terms(X)) -> mark#(X) p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) p6: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p7: mark#(cons(X1,X2)) -> mark#(X1) p8: mark#(recip(X)) -> mark#(X) p9: mark#(sqr(X)) -> active#(sqr(mark(X))) p10: mark#(sqr(X)) -> mark#(X) p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p12: mark#(add(X1,X2)) -> mark#(X1) p13: mark#(dbl(X)) -> mark#(X) p14: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p15: mark#(first(X1,X2)) -> mark#(X1) 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: standard order interpretations: active#_A(x1) = ((0,1),(0,0)) x1 + (2,6) terms_A(x1) = (3,7) mark#_A(x1) = (9,6) cons_A(x1,x2) = (0,0) recip_A(x1) = ((1,0),(0,0)) x1 + (1,4) sqr_A(x1) = (6,5) s_A(x1) = ((0,0),(1,0)) x1 mark_A(x1) = ((1,0),(0,0)) x1 + (2,5) add_A(x1,x2) = ((1,0),(0,0)) x2 + (9,7) first_A(x1,x2) = ((1,0),(0,0)) x1 + (10,7) dbl_A(x1) = ((1,0),(0,0)) x1 + (5,5) active_A(x1) = ((1,0),(0,0)) x1 + (0,5) |0|_A() = (4,0) nil_A() = (1,8) precedence: recip > first = dbl > add > sqr = s = mark = active = |0| > active# = mark# > cons > terms = nil partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(first) = [] pi(dbl) = [] pi(active) = [] pi(|0|) = [] 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#(add(s(X),Y)) -> mark#(s(add(X,Y))) p4: mark#(terms(X)) -> mark#(X) p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) p6: mark#(cons(X1,X2)) -> mark#(X1) p7: mark#(recip(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) p9: mark#(sqr(X)) -> mark#(X) p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p11: mark#(add(X1,X2)) -> mark#(X1) p12: mark#(dbl(X)) -> mark#(X) p13: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p14: mark#(first(X1,X2)) -> mark#(X1) 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: 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#(add(X1,X2)) -> mark#(X1) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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) p14: mark#(terms(X)) -> mark#(X) p15: 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: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 + (22,0) terms_A(x1) = ((0,0),(0,1)) x1 + (49,24) mark#_A(x1) = ((0,1),(0,1)) x1 + (28,1) cons_A(x1,x2) = ((0,0),(0,1)) x1 + (43,8) recip_A(x1) = ((0,0),(0,1)) x1 + (29,1) sqr_A(x1) = ((0,0),(0,1)) x1 + (23,8) s_A(x1) = ((0,1),(0,0)) x1 + (1,7) first_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (27,0) mark_A(x1) = ((0,1),(0,1)) x1 + (30,0) dbl_A(x1) = ((0,0),(0,1)) x1 + (9,7) add_A(x1,x2) = ((0,0),(0,1)) x1 + ((0,1),(0,1)) x2 + (33,6) active_A(x1) = ((0,1),(0,1)) x1 + (24,0) |0|_A() = (0,8) nil_A() = (30,1) precedence: recip > add = |0| > active# = mark# = nil > first > dbl > terms = cons = sqr = s = mark = active partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(first) = [] pi(mark) = [] pi(dbl) = [] pi(add) = [] pi(active) = [] pi(|0|) = [] 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#(first(X1,X2)) -> mark#(X2) p3: mark#(first(X1,X2)) -> mark#(X1) p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p5: mark#(dbl(X)) -> mark#(X) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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) p13: mark#(terms(X)) -> mark#(X) p14: 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} -- 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#(add(s(X),Y)) -> mark#(s(add(X,Y))) 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: mark#(sqr(X)) -> mark#(X) p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p10: mark#(add(X1,X2)) -> mark#(X1) p11: mark#(dbl(X)) -> mark#(X) p12: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p13: mark#(first(X1,X2)) -> mark#(X1) 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: standard order interpretations: active#_A(x1) = ((1,1),(1,0)) x1 + (8,2) terms_A(x1) = ((1,1),(1,1)) x1 mark#_A(x1) = ((1,1),(1,1)) x1 + (8,2) cons_A(x1,x2) = ((0,0),(1,1)) x1 recip_A(x1) = ((0,0),(1,1)) x1 sqr_A(x1) = ((1,1),(0,0)) x1 s_A(x1) = ((0,1),(0,1)) x1 + (7,2) mark_A(x1) = ((0,0),(1,1)) x1 add_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (9,0) dbl_A(x1) = ((1,1),(0,0)) x1 + (8,4) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,0)) x2 + (9,11) active_A(x1) = ((0,0),(1,1)) x1 |0|_A() = (2,2) nil_A() = (1,1) precedence: cons = first > dbl > active# = mark# > recip > add > nil > s = mark = active = |0| > terms = sqr 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: 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#(terms(X)) -> active#(terms(mark(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: mark#(sqr(X)) -> mark#(X) p8: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) p9: mark#(add(X1,X2)) -> mark#(X1) p10: mark#(dbl(X)) -> mark#(X) p11: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p12: mark#(first(X1,X2)) -> mark#(X1) 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: 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: mark#(dbl(X)) -> mark#(X) 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#(sqr(X)) -> active#(sqr(mark(X))) p10: mark#(recip(X)) -> mark#(X) p11: mark#(cons(X1,X2)) -> mark#(X1) p12: mark#(terms(X)) -> mark#(X) p13: 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: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 + (3,1) terms_A(x1) = ((1,1),(0,0)) x1 + (13,16) mark#_A(x1) = (19,17) cons_A(x1,x2) = ((0,0),(1,1)) x1 + (2,0) recip_A(x1) = ((1,1),(0,0)) x1 + (1,18) sqr_A(x1) = ((1,1),(0,0)) x1 + (1,6) s_A(x1) = (3,2) first_A(x1,x2) = ((1,1),(0,0)) x2 + (4,15) mark_A(x1) = ((0,0),(1,1)) x1 + (0,1) dbl_A(x1) = ((0,0),(1,1)) x1 + (20,0) add_A(x1,x2) = ((1,1),(0,0)) x2 + (17,13) active_A(x1) = ((0,0),(1,1)) x1 |0|_A() = (1,7) nil_A() = (1,6) precedence: dbl = |0| > recip = nil > active# = mark# > mark = active > add > terms = s > sqr > cons = first 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(active) = [] pi(|0|) = [] pi(nil) = [] The next rules are strictly ordered: p7 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: mark#(dbl(X)) -> mark#(X) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(sqr(X)) -> active#(sqr(mark(X))) p9: mark#(recip(X)) -> mark#(X) p10: mark#(cons(X1,X2)) -> mark#(X1) p11: mark#(terms(X)) -> mark#(X) p12: 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} -- 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: 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: mark#(sqr(X)) -> mark#(X) p8: mark#(add(X1,X2)) -> mark#(X1) p9: mark#(dbl(X)) -> mark#(X) p10: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p11: mark#(first(X1,X2)) -> mark#(X1) 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: standard order interpretations: active#_A(x1) = ((0,1),(0,0)) x1 + (1,0) terms_A(x1) = (35,30) mark#_A(x1) = (31,0) cons_A(x1,x2) = (1,26) recip_A(x1) = (36,32) sqr_A(x1) = (10,29) s_A(x1) = (0,3) mark_A(x1) = ((0,1),(1,1)) x1 + (8,1) add_A(x1,x2) = ((0,1),(1,1)) x2 + (9,4) dbl_A(x1) = (11,15) first_A(x1,x2) = (32,28) active_A(x1) = x1 + (2,1) |0|_A() = (10,4) nil_A() = (0,23) precedence: terms > mark = dbl = first = active > add > recip > active# = mark# = cons = s = |0| > sqr > 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: p6 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: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> mark#(X1) p5: mark#(recip(X)) -> mark#(X) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(dbl(X)) -> mark#(X) p9: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) p10: mark#(first(X1,X2)) -> mark#(X1) 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: 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: mark#(dbl(X)) -> mark#(X) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(sqr(X)) -> mark#(X) p8: mark#(recip(X)) -> mark#(X) p9: mark#(cons(X1,X2)) -> mark#(X1) p10: mark#(terms(X)) -> mark#(X) p11: 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: standard order interpretations: active#_A(x1) = ((0,1),(0,0)) x1 + (1,0) terms_A(x1) = (0,2) mark#_A(x1) = (3,0) cons_A(x1,x2) = (3,0) recip_A(x1) = (7,1) sqr_A(x1) = (7,4) s_A(x1) = (4,3) first_A(x1,x2) = (0,1) mark_A(x1) = (6,0) dbl_A(x1) = (5,5) add_A(x1,x2) = (5,5) active_A(x1) = (6,0) |0|_A() = (1,1) nil_A() = (1,0) precedence: active# = mark# = first > terms > sqr = s = mark = dbl = add = active > recip > cons > |0| > 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(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)) -> mark#(X1) p4: mark#(dbl(X)) -> mark#(X) p5: mark#(add(X1,X2)) -> mark#(X1) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(recip(X)) -> mark#(X) p8: mark#(cons(X1,X2)) -> mark#(X1) p9: mark#(terms(X)) -> mark#(X) p10: 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} -- 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: mark#(terms(X)) -> mark#(X) p4: mark#(cons(X1,X2)) -> mark#(X1) p5: mark#(recip(X)) -> mark#(X) p6: mark#(sqr(X)) -> mark#(X) p7: mark#(add(X1,X2)) -> mark#(X1) p8: mark#(dbl(X)) -> mark#(X) p9: mark#(first(X1,X2)) -> mark#(X1) 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: standard order interpretations: active#_A(x1) = ((0,1),(0,1)) x1 + (1,4) terms_A(x1) = x1 + (17,15) mark#_A(x1) = ((0,1),(0,1)) x1 + (12,16) cons_A(x1,x2) = ((0,0),(0,1)) x1 + (8,1) recip_A(x1) = ((0,1),(0,1)) x1 + (0,1) sqr_A(x1) = ((0,0),(0,1)) x1 + (15,1) s_A(x1) = (0,5) mark_A(x1) = x1 + (9,0) add_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (9,16) dbl_A(x1) = ((1,1),(0,1)) x1 + (13,16) first_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (13,16) active_A(x1) = x1 |0|_A() = (5,1) nil_A() = (0,17) precedence: mark = active > |0| > recip > nil > active# = cons > sqr > add > first > dbl > s > terms = mark# partial status: pi(active#) = [] pi(terms) = [] pi(mark#) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [] pi(s) = [] pi(mark) = [] pi(add) = [] pi(dbl) = [] pi(first) = [2] pi(active) = [] pi(|0|) = [] 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: mark#(terms(X)) -> mark#(X) p3: mark#(cons(X1,X2)) -> mark#(X1) p4: mark#(recip(X)) -> mark#(X) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(add(X1,X2)) -> mark#(X1) p7: mark#(dbl(X)) -> mark#(X) p8: mark#(first(X1,X2)) -> mark#(X1) 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: {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#(first(X1,X2)) -> mark#(X1) p4: mark#(dbl(X)) -> mark#(X) p5: mark#(add(X1,X2)) -> mark#(X1) 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 set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2) terms_A(x1) = x1 + (1,1) first_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (3,2) dbl_A(x1) = ((0,0),(0,1)) x1 + (1,1) add_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1) sqr_A(x1) = x1 + (1,1) recip_A(x1) = ((0,0),(0,1)) x1 + (1,1) cons_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1) precedence: mark# > first > dbl > terms > add = sqr = recip = cons partial status: pi(mark#) = [] pi(terms) = [] pi(first) = [1] pi(dbl) = [] pi(add) = [2] pi(sqr) = [1] pi(recip) = [] pi(cons) = [] 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: mark#(dbl(X)) -> mark#(X) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(sqr(X)) -> mark#(X) p6: mark#(recip(X)) -> mark#(X) p7: 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} -- 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)) -> mark#(X1) p6: mark#(dbl(X)) -> mark#(X) p7: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,1)) x1 + (2,2) terms_A(x1) = ((1,1),(1,1)) x1 + (3,2) cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) recip_A(x1) = ((0,0),(0,1)) x1 + (1,1) sqr_A(x1) = x1 + (1,1) add_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1) dbl_A(x1) = x1 + (3,1) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(0,1)) x2 + (1,1) precedence: sqr = add > terms > cons > mark# > dbl = first > recip partial status: pi(mark#) = [] pi(terms) = [] pi(cons) = [] pi(recip) = [] pi(sqr) = [1] pi(add) = [2] pi(dbl) = [1] pi(first) = [1] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(cons(X1,X2)) -> mark#(X1) p3: mark#(sqr(X)) -> mark#(X) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(dbl(X)) -> mark#(X) p6: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(first(X1,X2)) -> mark#(X2) p3: mark#(dbl(X)) -> mark#(X) p4: mark#(add(X1,X2)) -> mark#(X1) p5: mark#(sqr(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: standard order interpretations: mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2) terms_A(x1) = x1 + (3,1) first_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1) dbl_A(x1) = x1 + (1,1) add_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1) sqr_A(x1) = x1 + (1,1) cons_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1) precedence: dbl > mark# = terms = first = add = sqr = cons partial status: pi(mark#) = [] pi(terms) = [1] pi(first) = [] pi(dbl) = [1] pi(add) = [] pi(sqr) = [] pi(cons) = [2] 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: mark#(add(X1,X2)) -> mark#(X1) p4: mark#(sqr(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#(sqr(X)) -> mark#(X) p4: mark#(add(X1,X2)) -> mark#(X1) p5: 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 (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,1)) x1 + (1,2) terms_A(x1) = x1 + (0,1) cons_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(1,1)) x2 + (2,2) sqr_A(x1) = ((0,0),(0,1)) x1 + (0,1) add_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (0,1) first_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(0,1)) x2 + (0,1) precedence: cons = add > mark# = terms > first > sqr partial status: pi(mark#) = [] pi(terms) = [1] pi(cons) = [2] pi(sqr) = [] pi(add) = [2] pi(first) = [1] 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#(sqr(X)) -> mark#(X) p4: 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} -- 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#(sqr(X)) -> mark#(X) p4: 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: standard order interpretations: mark#_A(x1) = ((0,1),(0,1)) x1 + (2,2) terms_A(x1) = ((1,1),(1,1)) x1 + (3,2) first_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1) sqr_A(x1) = ((0,0),(0,1)) x1 + (1,1) cons_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (3,1) precedence: terms > mark# = sqr = cons > first partial status: pi(mark#) = [] pi(terms) = [1] pi(first) = [2] pi(sqr) = [] pi(cons) = [] 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#(sqr(X)) -> mark#(X) p3: 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} -- 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#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2) terms_A(x1) = x1 + (1,1) cons_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (0,1) sqr_A(x1) = ((0,0),(0,1)) x1 + (3,1) precedence: mark# > terms = cons = sqr partial status: pi(mark#) = [] pi(terms) = [1] pi(cons) = [2] pi(sqr) = [] 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#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(terms(X)) -> mark#(X) p2: mark#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2) terms_A(x1) = ((0,0),(0,1)) x1 + (1,1) sqr_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: mark# = terms = sqr partial status: pi(mark#) = [] pi(terms) = [] pi(sqr) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(sqr(X)) -> mark#(X) 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#(sqr(X)) -> mark#(X) and R consists of: r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N)))) r2: active(sqr(|0|())) -> mark(|0|()) r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X)))) r4: active(dbl(|0|())) -> mark(|0|()) r5: active(dbl(s(X))) -> mark(s(s(dbl(X)))) r6: active(add(|0|(),X)) -> mark(X) r7: active(add(s(X),Y)) -> mark(s(add(X,Y))) r8: active(first(|0|(),X)) -> mark(nil()) r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) r10: mark(terms(X)) -> active(terms(mark(X))) r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) r12: mark(recip(X)) -> active(recip(mark(X))) r13: mark(sqr(X)) -> active(sqr(mark(X))) r14: mark(s(X)) -> active(s(X)) r15: mark(|0|()) -> active(|0|()) r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) r17: mark(dbl(X)) -> active(dbl(mark(X))) r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) r19: mark(nil()) -> active(nil()) r20: terms(mark(X)) -> terms(X) r21: terms(active(X)) -> terms(X) r22: cons(mark(X1),X2) -> cons(X1,X2) r23: cons(X1,mark(X2)) -> cons(X1,X2) r24: cons(active(X1),X2) -> cons(X1,X2) r25: cons(X1,active(X2)) -> cons(X1,X2) r26: recip(mark(X)) -> recip(X) r27: recip(active(X)) -> recip(X) r28: sqr(mark(X)) -> sqr(X) r29: sqr(active(X)) -> sqr(X) r30: s(mark(X)) -> s(X) r31: s(active(X)) -> s(X) r32: add(mark(X1),X2) -> add(X1,X2) r33: add(X1,mark(X2)) -> add(X1,X2) r34: add(active(X1),X2) -> add(X1,X2) r35: add(X1,active(X2)) -> add(X1,X2) r36: dbl(mark(X)) -> dbl(X) r37: dbl(active(X)) -> dbl(X) r38: first(mark(X1),X2) -> first(X1,X2) r39: first(X1,mark(X2)) -> first(X1,X2) r40: first(active(X1),X2) -> first(X1,X2) r41: first(X1,active(X2)) -> first(X1,X2) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: mark#_A(x1) = ((1,0),(1,0)) x1 + (2,2) sqr_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: mark# = sqr partial status: pi(mark#) = [] pi(sqr) = [] 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: standard order interpretations: cons#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: cons# = mark = active partial status: pi(cons#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cons#(X1,active(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#(X1,active(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: standard order interpretations: cons#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: cons# > active = mark partial status: pi(cons#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cons#(X1,active(X2)) -> cons#(X1,X2) p2: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: cons#(X1,active(X2)) -> cons#(X1,X2) p2: 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: standard order interpretations: cons#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: cons# = active = mark partial status: pi(cons#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: cons#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: cons# = mark partial status: pi(cons#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: recip#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: recip# = mark = active partial status: pi(recip#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard 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: standard order interpretations: sqr#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: sqr# = mark = active partial status: pi(sqr#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard 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: standard order interpretations: terms#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: terms# = mark = active partial status: pi(terms#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard 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: standard order interpretations: s#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: s# = mark = active partial status: pi(s#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: s#(active(X)) -> s#(X) and R consists of: r1: active(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: standard order interpretations: s#_A(x1) = ((1,0),(1,0)) x1 + (2,2) active_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: s# = active partial status: pi(s#) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: add#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: add# = mark = active partial status: pi(add#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: add#(X1,active(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#(X1,active(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: standard order interpretations: add#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: add# > active = mark partial status: pi(add#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: add#(X1,active(X2)) -> add#(X1,X2) p2: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: add#(X1,active(X2)) -> add#(X1,X2) p2: 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: standard order interpretations: add#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: add# = active = mark partial status: pi(add#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: add#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: add# = mark partial status: pi(add#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: dbl#_A(x1) = ((0,1),(0,0)) x1 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) active_A(x1) = ((0,1),(0,1)) x1 + (1,1) precedence: dbl# = mark = active partial status: pi(dbl#) = [] pi(mark) = [] pi(active) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard 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: standard order interpretations: first#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2) mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) active_A(x1) = ((1,1),(1,1)) x1 + (1,1) precedence: first# = mark = active partial status: pi(first#) = [1] pi(mark) = [1] pi(active) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: first#(X1,active(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#(X1,active(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: standard order interpretations: first#_A(x1,x2) = ((1,1),(1,1)) x1 + (2,2) active_A(x1) = ((1,1),(1,1)) x1 + (3,2) mark_A(x1) = (1,1) precedence: first# > active = mark partial status: pi(first#) = [] pi(active) = [] pi(mark) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: first#(X1,active(X2)) -> first#(X1,X2) p2: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: first#(X1,active(X2)) -> first#(X1,X2) p2: 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: standard order interpretations: first#_A(x1,x2) = x1 + x2 + (2,2) active_A(x1) = x1 + (1,0) mark_A(x1) = x1 + (1,1) precedence: first# = active = mark partial status: pi(first#) = [2] pi(active) = [1] pi(mark) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: standard order interpretations: first#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,2) mark_A(x1) = ((0,0),(0,1)) x1 + (1,1) precedence: first# = mark partial status: pi(first#) = [] pi(mark) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.