YES We show the termination of the TRS R: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) activate(n__isList(X)) -> isList(X) activate(n__isNeList(X)) -> isNeList(X) activate(n__isPal(X)) -> isPal(X) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__o()) -> o() activate(n__u()) -> u() activate(X) -> X -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) p2: __#(__(X,Y),Z) -> __#(Y,Z) p3: and#(tt(),X) -> activate#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isList#(V) -> activate#(V) p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p7: isList#(n____(V1,V2)) -> isList#(activate(V1)) p8: isList#(n____(V1,V2)) -> activate#(V1) p9: isList#(n____(V1,V2)) -> activate#(V2) p10: isNeList#(V) -> isQid#(activate(V)) p11: isNeList#(V) -> activate#(V) p12: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p14: isNeList#(n____(V1,V2)) -> activate#(V1) p15: isNeList#(n____(V1,V2)) -> activate#(V2) p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p17: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p18: isNeList#(n____(V1,V2)) -> activate#(V1) p19: isNeList#(n____(V1,V2)) -> activate#(V2) p20: isNePal#(V) -> isQid#(activate(V)) p21: isNePal#(V) -> activate#(V) p22: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p23: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I)) p24: isNePal#(n____(I,n____(P,I))) -> activate#(I) p25: isNePal#(n____(I,n____(P,I))) -> activate#(P) p26: isPal#(V) -> isNePal#(activate(V)) p27: isPal#(V) -> activate#(V) p28: activate#(n__nil()) -> nil#() p29: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2)) p30: activate#(n____(X1,X2)) -> activate#(X1) p31: activate#(n____(X1,X2)) -> activate#(X2) p32: activate#(n__isList(X)) -> isList#(X) p33: activate#(n__isNeList(X)) -> isNeList#(X) p34: activate#(n__isPal(X)) -> isPal#(X) p35: activate#(n__a()) -> a#() p36: activate#(n__e()) -> e#() p37: activate#(n__i()) -> i#() p38: activate#(n__o()) -> o#() p39: activate#(n__u()) -> u#() and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p3, p4, p5, p6, p7, p8, p9, p11, p12, p13, p14, p15, p16, p17, p18, p19, p21, p22, p24, p25, p26, p27, p30, p31, p32, p33, p34} {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(V) -> activate#(V) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,n____(P,I))) -> activate#(P) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V2) p7: activate#(n__isList(X)) -> isList#(X) p8: isList#(n____(V1,V2)) -> activate#(V2) p9: activate#(n____(X1,X2)) -> activate#(X2) p10: activate#(n____(X1,X2)) -> activate#(X1) p11: isList#(n____(V1,V2)) -> activate#(V1) p12: isList#(n____(V1,V2)) -> isList#(activate(V1)) p13: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p14: and#(tt(),X) -> activate#(X) p15: isList#(V) -> activate#(V) p16: isList#(V) -> isNeList#(activate(V)) p17: isNeList#(n____(V1,V2)) -> activate#(V1) p18: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p19: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p20: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p21: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p22: isNeList#(V) -> activate#(V) p23: isNePal#(n____(I,n____(P,I))) -> activate#(I) p24: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p25: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isPal#_A(x1) = ((1,0),(0,0)) x1 + (3,2) activate#_A(x1) = ((1,0),(0,0)) x1 + (1,3) n__isPal_A(x1) = ((1,0),(1,1)) x1 + (4,21) isNePal#_A(x1) = ((1,0),(0,0)) x1 + (2,4) activate_A(x1) = x1 + (0,5) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (33,18) n__isNeList_A(x1) = ((1,0),(1,1)) x1 + (3,15) isNeList#_A(x1) = ((1,0),(1,0)) x1 + (2,1) n__isList_A(x1) = ((1,0),(1,1)) x1 + (4,21) isList#_A(x1) = ((1,0),(0,0)) x1 + (3,2) and#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (2,0) isList_A(x1) = ((1,0),(1,1)) x1 + (4,25) tt_A() = (0,0) isNeList_A(x1) = ((1,0),(1,1)) x1 + (3,19) isQid_A(x1) = (0,18) isNePal_A(x1) = x1 + (0,19) and_A(x1,x2) = ((1,0),(1,1)) x2 + (1,6) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (33,19) nil_A() = (0,2) isPal_A(x1) = ((1,0),(1,1)) x1 + (4,25) n__nil_A() = (0,1) a_A() = (1,2) n__a_A() = (1,1) e_A() = (1,2) n__e_A() = (1,1) i_A() = (1,2) n__i_A() = (1,1) o_A() = (1,2) n__o_A() = (1,1) u_A() = (1,2) n__u_A() = (1,1) precedence: and > isPal# = activate# = n__isPal = isNePal# = and# > n____ > e = n__e > activate = isList = isNeList = __ = isPal = u > isQid = isNePal > a > i = o > n__o = n__u > tt = nil = n__nil = n__a = n__i > n__isNeList = isNeList# = n__isList = isList# partial status: pi(isPal#) = [] pi(activate#) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n____) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n__isList) = [] pi(isList#) = [] pi(and#) = [] pi(isList) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isQid) = [] pi(isNePal) = [1] pi(and) = [2] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: isPal#(V) -> activate#(V) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,n____(P,I))) -> activate#(P) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: activate#(n__isList(X)) -> isList#(X) p7: isList#(n____(V1,V2)) -> activate#(V2) p8: activate#(n____(X1,X2)) -> activate#(X2) p9: activate#(n____(X1,X2)) -> activate#(X1) p10: isList#(n____(V1,V2)) -> activate#(V1) p11: isList#(n____(V1,V2)) -> isList#(activate(V1)) p12: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p13: and#(tt(),X) -> activate#(X) p14: isList#(V) -> activate#(V) p15: isList#(V) -> isNeList#(activate(V)) p16: isNeList#(n____(V1,V2)) -> activate#(V1) p17: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p18: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p19: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p20: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p21: isNeList#(V) -> activate#(V) p22: isNePal#(n____(I,n____(P,I))) -> activate#(I) p23: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p24: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(V) -> activate#(V) p2: activate#(n____(X1,X2)) -> activate#(X1) p3: activate#(n____(X1,X2)) -> activate#(X2) p4: activate#(n__isList(X)) -> isList#(X) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(V) -> activate#(V) p7: activate#(n__isNeList(X)) -> isNeList#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: and#(tt(),X) -> activate#(X) p10: activate#(n__isPal(X)) -> isPal#(X) p11: isPal#(V) -> isNePal#(activate(V)) p12: isNePal#(V) -> activate#(V) p13: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p14: isNePal#(n____(I,n____(P,I))) -> activate#(I) p15: isNePal#(n____(I,n____(P,I))) -> activate#(P) p16: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p17: isList#(V) -> activate#(V) p18: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p19: isList#(n____(V1,V2)) -> isList#(activate(V1)) p20: isList#(n____(V1,V2)) -> activate#(V1) p21: isList#(n____(V1,V2)) -> activate#(V2) p22: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p23: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p24: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isPal#_A(x1) = x1 + (12,12) activate#_A(x1) = ((1,0),(1,0)) x1 + (3,1) n_____A(x1,x2) = x1 + x2 + (15,45) n__isList_A(x1) = ((1,0),(0,0)) x1 + (8,5) isList#_A(x1) = ((1,0),(1,0)) x1 + (7,8) isNeList#_A(x1) = ((1,0),(0,0)) x1 + (4,7) activate_A(x1) = ((1,0),(1,1)) x1 + (0,13) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (5,107) and#_A(x1,x2) = ((1,0),(0,0)) x2 + (4,44) isList_A(x1) = ((1,0),(0,0)) x1 + (8,6) tt_A() = (2,2) n__isPal_A(x1) = ((1,0),(1,0)) x1 + (10,91) isNePal#_A(x1) = ((1,0),(1,0)) x1 + (4,13) isQid_A(x1) = (3,1) isNeList_A(x1) = ((1,0),(0,0)) x1 + (5,124) isNePal_A(x1) = ((1,0),(1,0)) x1 + (4,92) and_A(x1,x2) = ((1,0),(0,0)) x2 + (6,123) ___A(x1,x2) = x1 + x2 + (15,46) nil_A() = (3,4) isPal_A(x1) = ((1,0),(1,0)) x1 + (10,92) n__nil_A() = (3,3) a_A() = (3,4) n__a_A() = (3,3) e_A() = (3,4) n__e_A() = (3,3) i_A() = (3,4) n__i_A() = (3,3) o_A() = (1,4) n__o_A() = (1,3) u_A() = (3,4) n__u_A() = (3,3) precedence: and# = isNeList > isNePal# > activate# = isList# = isNeList# > and > n____ = activate = n__isNeList = n__isPal = __ = nil = isPal = a = e = o = n__o > isNePal > isPal# = n__nil > n__isList = isList > i = n__i = u > tt = isQid = n__a = n__u > n__e partial status: pi(isPal#) = [1] pi(activate#) = [] pi(n____) = [1] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [1] pi(n__isNeList) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(isQid) = [] pi(isNeList) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [1, 2] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n____(X1,X2)) -> activate#(X1) p2: activate#(n____(X1,X2)) -> activate#(X2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isNeList#(V) -> activate#(V) p6: activate#(n__isNeList(X)) -> isNeList#(X) p7: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p8: and#(tt(),X) -> activate#(X) p9: activate#(n__isPal(X)) -> isPal#(X) p10: isPal#(V) -> isNePal#(activate(V)) p11: isNePal#(V) -> activate#(V) p12: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p13: isNePal#(n____(I,n____(P,I))) -> activate#(I) p14: isNePal#(n____(I,n____(P,I))) -> activate#(P) p15: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p16: isList#(V) -> activate#(V) p17: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p18: isList#(n____(V1,V2)) -> isList#(activate(V1)) p19: isList#(n____(V1,V2)) -> activate#(V1) p20: isList#(n____(V1,V2)) -> activate#(V2) p21: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p22: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p23: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n____(X1,X2)) -> activate#(X1) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,n____(P,I))) -> activate#(P) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V1) p7: activate#(n__isList(X)) -> isList#(X) p8: isList#(n____(V1,V2)) -> activate#(V2) p9: activate#(n____(X1,X2)) -> activate#(X2) p10: isList#(n____(V1,V2)) -> activate#(V1) p11: isList#(n____(V1,V2)) -> isList#(activate(V1)) p12: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p13: and#(tt(),X) -> activate#(X) p14: isList#(V) -> activate#(V) p15: isList#(V) -> isNeList#(activate(V)) p16: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p17: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p18: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p19: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p20: isNeList#(V) -> activate#(V) p21: isNePal#(n____(I,n____(P,I))) -> activate#(I) p22: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p23: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = x1 + (9,1) n_____A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (4,47) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (11,4) isPal#_A(x1) = ((1,0),(0,0)) x1 + (15,3) isNePal#_A(x1) = ((1,0),(0,0)) x1 + (14,2) activate_A(x1) = ((1,0),(1,1)) x1 + (0,16) n__isNeList_A(x1) = ((1,0),(1,1)) x1 + (10,24) isNeList#_A(x1) = x1 + (18,19) n__isList_A(x1) = x1 + (11,72) isList#_A(x1) = ((1,0),(1,1)) x1 + (18,36) and#_A(x1,x2) = x2 + (10,0) isList_A(x1) = x1 + (11,73) tt_A() = (1,47) isNeList_A(x1) = ((1,0),(1,1)) x1 + (10,49) isQid_A(x1) = (9,48) isNePal_A(x1) = ((1,0),(1,0)) x1 + (10,7) and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (2,1) ___A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (4,48) nil_A() = (18,1) isPal_A(x1) = ((1,0),(1,0)) x1 + (11,30) n__nil_A() = (18,0) a_A() = (2,49) n__a_A() = (2,48) e_A() = (2,49) n__e_A() = (2,48) i_A() = (2,49) n__i_A() = (2,48) o_A() = (2,49) n__o_A() = (2,48) u_A() = (2,49) n__u_A() = (2,48) precedence: __ > n__isPal > activate = isList = tt = isNeList = isQid = isNePal = isPal = i > activate# = isPal# = isNePal# = n__isNeList = isNeList# = n__isList = isList# = and# = n__i = o = n__o > nil = n__nil > and > n__a > n____ > a = e = n__e = u = n__u partial status: pi(activate#) = [] pi(n____) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n__isList) = [1] pi(isList#) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isQid) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n____(X1,X2)) -> activate#(X1) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,n____(P,I))) -> activate#(P) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V1) p7: activate#(n__isList(X)) -> isList#(X) p8: isList#(n____(V1,V2)) -> activate#(V2) p9: activate#(n____(X1,X2)) -> activate#(X2) p10: isList#(n____(V1,V2)) -> isList#(activate(V1)) p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p12: and#(tt(),X) -> activate#(X) p13: isList#(V) -> activate#(V) p14: isList#(V) -> isNeList#(activate(V)) p15: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p17: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p18: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p19: isNeList#(V) -> activate#(V) p20: isNePal#(n____(I,n____(P,I))) -> activate#(I) p21: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p22: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n____(X1,X2)) -> activate#(X1) p2: activate#(n____(X1,X2)) -> activate#(X2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isNeList#(V) -> activate#(V) p6: activate#(n__isNeList(X)) -> isNeList#(X) p7: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p8: and#(tt(),X) -> activate#(X) p9: activate#(n__isPal(X)) -> isPal#(X) p10: isPal#(V) -> isNePal#(activate(V)) p11: isNePal#(V) -> activate#(V) p12: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p13: isNePal#(n____(I,n____(P,I))) -> activate#(I) p14: isNePal#(n____(I,n____(P,I))) -> activate#(P) p15: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p16: isList#(V) -> activate#(V) p17: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p18: isList#(n____(V1,V2)) -> isList#(activate(V1)) p19: isList#(n____(V1,V2)) -> activate#(V2) p20: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p21: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p22: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((0,0),(1,0)) x1 + (9,0) n_____A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (10,0) n__isList_A(x1) = ((1,0),(0,0)) x1 + (7,4) isList#_A(x1) = ((0,0),(1,0)) x1 + (9,5) isNeList#_A(x1) = ((0,0),(1,0)) x1 + (9,3) activate_A(x1) = x1 + (0,2) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (4,2) and#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (9,1) isList_A(x1) = ((1,0),(0,0)) x1 + (7,5) tt_A() = (2,0) n__isPal_A(x1) = ((1,0),(1,0)) x1 + (16,14) isPal#_A(x1) = ((0,0),(1,0)) x1 + (9,15) isNePal#_A(x1) = ((0,0),(1,0)) x1 + (9,1) isQid_A(x1) = (3,3) isNeList_A(x1) = ((1,0),(0,0)) x1 + (4,3) isNePal_A(x1) = ((1,0),(1,1)) x1 + (4,4) and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (2,3) ___A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (10,0) nil_A() = (3,0) isPal_A(x1) = ((1,0),(1,0)) x1 + (16,15) n__nil_A() = (3,0) a_A() = (3,1) n__a_A() = (3,1) e_A() = (3,2) n__e_A() = (3,1) i_A() = (3,2) n__i_A() = (3,1) o_A() = (1,2) n__o_A() = (1,1) u_A() = (3,1) n__u_A() = (3,1) precedence: activate# = n____ = n__isList = isList# = isNeList# = activate = n__isNeList = and# = isList = tt = n__isPal = isPal# = isNePal# = isQid = isNeList = isNePal = and = __ = nil = isPal = n__nil = a = n__a = e = n__e = i = n__i = o = n__o = u = n__u partial status: pi(activate#) = [] pi(n____) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [] pi(n__isNeList) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(isQid) = [] pi(isNeList) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n____(X1,X2)) -> activate#(X2) p2: activate#(n__isList(X)) -> isList#(X) p3: isList#(V) -> isNeList#(activate(V)) p4: isNeList#(V) -> activate#(V) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p7: and#(tt(),X) -> activate#(X) p8: activate#(n__isPal(X)) -> isPal#(X) p9: isPal#(V) -> isNePal#(activate(V)) p10: isNePal#(V) -> activate#(V) p11: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p12: isNePal#(n____(I,n____(P,I))) -> activate#(I) p13: isNePal#(n____(I,n____(P,I))) -> activate#(P) p14: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p15: isList#(V) -> activate#(V) p16: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p17: isList#(n____(V1,V2)) -> isList#(activate(V1)) p18: isList#(n____(V1,V2)) -> activate#(V2) p19: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p20: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p21: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n____(X1,X2)) -> activate#(X2) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,n____(P,I))) -> activate#(P) p5: activate#(n__isNeList(X)) -> isNeList#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V1) p7: activate#(n__isList(X)) -> isList#(X) p8: isList#(n____(V1,V2)) -> activate#(V2) p9: isList#(n____(V1,V2)) -> isList#(activate(V1)) p10: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p11: and#(tt(),X) -> activate#(X) p12: isList#(V) -> activate#(V) p13: isList#(V) -> isNeList#(activate(V)) p14: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p15: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p16: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p17: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p18: isNeList#(V) -> activate#(V) p19: isNePal#(n____(I,n____(P,I))) -> activate#(I) p20: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p21: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = x1 + (3,1) n_____A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (17,4) n__isPal_A(x1) = ((1,0),(1,1)) x1 + (18,12) isPal#_A(x1) = x1 + (5,11) isNePal#_A(x1) = x1 + (4,2) activate_A(x1) = x1 + (0,8) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (11,5) isNeList#_A(x1) = ((1,0),(1,1)) x1 + (13,7) n__isList_A(x1) = ((1,0),(1,0)) x1 + (12,0) isList#_A(x1) = ((1,0),(0,0)) x1 + (14,1) and#_A(x1,x2) = ((1,0),(0,0)) x2 + (4,7) isList_A(x1) = ((1,0),(1,0)) x1 + (12,7) tt_A() = (2,2) isNeList_A(x1) = ((1,0),(0,0)) x1 + (11,6) isQid_A(x1) = (3,3) isNePal_A(x1) = ((1,0),(1,0)) x1 + (18,18) and_A(x1,x2) = ((1,0),(1,1)) x2 + (0,13) ___A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (17,5) nil_A() = (0,2) isPal_A(x1) = ((1,0),(1,1)) x1 + (18,19) n__nil_A() = (0,1) a_A() = (3,4) n__a_A() = (3,3) e_A() = (0,4) n__e_A() = (0,3) i_A() = (1,4) n__i_A() = (1,3) o_A() = (3,4) n__o_A() = (3,3) u_A() = (0,4) n__u_A() = (0,3) precedence: n__isPal = activate = n__isList = isList = isNeList = isQid = isNePal = and = __ = isPal > n____ = n__isNeList > activate# = isPal# = isNePal# = isList# = and# > isNeList# > tt = nil = n__nil = a = n__a = i = n__i = o = n__o > u = n__u > e = n__e partial status: pi(activate#) = [] pi(n____) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(activate) = [] pi(n__isNeList) = [] pi(isNeList#) = [1] pi(n__isList) = [] pi(isList#) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isQid) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(n____(I,n____(P,I))) -> activate#(P) p4: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> activate#(V1) p6: activate#(n__isList(X)) -> isList#(X) p7: isList#(n____(V1,V2)) -> activate#(V2) p8: isList#(n____(V1,V2)) -> isList#(activate(V1)) p9: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p10: and#(tt(),X) -> activate#(X) p11: isList#(V) -> activate#(V) p12: isList#(V) -> isNeList#(activate(V)) p13: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p14: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p15: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p16: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p17: isNeList#(V) -> activate#(V) p18: isNePal#(n____(I,n____(P,I))) -> activate#(I) p19: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p20: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(V) -> activate#(V) p4: activate#(n__isList(X)) -> isList#(X) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(V) -> activate#(V) p7: activate#(n__isNeList(X)) -> isNeList#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: and#(tt(),X) -> activate#(X) p10: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p11: isList#(V) -> activate#(V) p12: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p13: isList#(n____(V1,V2)) -> isList#(activate(V1)) p14: isList#(n____(V1,V2)) -> activate#(V2) p15: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p16: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p17: isNeList#(n____(V1,V2)) -> activate#(V1) p18: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p19: isNePal#(n____(I,n____(P,I))) -> activate#(I) p20: isNePal#(n____(I,n____(P,I))) -> activate#(P) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((1,0),(1,0)) x1 + (25,19) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (24,27) isPal#_A(x1) = ((1,0),(1,0)) x1 + (26,42) isNePal#_A(x1) = ((1,0),(1,0)) x1 + (26,20) activate_A(x1) = ((1,0),(1,1)) x1 + (0,27) n__isList_A(x1) = ((1,0),(0,0)) x1 + (14,1) isList#_A(x1) = ((1,0),(1,0)) x1 + (27,31) isNeList#_A(x1) = ((1,0),(1,0)) x1 + (25,31) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (13,1) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,30) and#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (1,1) isList_A(x1) = ((1,0),(1,0)) x1 + (14,36) tt_A() = (24,0) isNeList_A(x1) = ((1,0),(0,0)) x1 + (13,35) isQid_A(x1) = ((1,0),(0,0)) x1 + (2,29) isNePal_A(x1) = ((1,0),(0,0)) x1 + (20,56) and_A(x1,x2) = x2 + (1,28) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,31) nil_A() = (25,2) isPal_A(x1) = ((1,0),(0,0)) x1 + (24,57) n__nil_A() = (25,1) a_A() = (25,2) n__a_A() = (25,1) e_A() = (23,51) n__e_A() = (23,1) i_A() = (25,2) n__i_A() = (25,1) o_A() = (25,2) n__o_A() = (25,1) u_A() = (23,2) n__u_A() = (23,1) precedence: activate# = isPal# = isNePal# = isList# = isNeList# = n__isNeList = and# > n__isPal = activate = isList = tt = isNeList = isQid = isNePal = and = __ = nil = isPal = n__nil > n__isList = a = n__a = e = n__e = i = n__i = o = n__o = u = n__u > n____ partial status: pi(activate#) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(activate) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(n__isNeList) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isQid) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(V) -> activate#(V) p4: activate#(n__isList(X)) -> isList#(X) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(V) -> activate#(V) p7: activate#(n__isNeList(X)) -> isNeList#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: and#(tt(),X) -> activate#(X) p10: isList#(V) -> activate#(V) p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p12: isList#(n____(V1,V2)) -> isList#(activate(V1)) p13: isList#(n____(V1,V2)) -> activate#(V2) p14: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p15: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p16: isNeList#(n____(V1,V2)) -> activate#(V1) p17: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p18: isNePal#(n____(I,n____(P,I))) -> activate#(I) p19: isNePal#(n____(I,n____(P,I))) -> activate#(P) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(n____(I,n____(P,I))) -> activate#(P) p4: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> activate#(V1) p6: activate#(n__isList(X)) -> isList#(X) p7: isList#(n____(V1,V2)) -> activate#(V2) p8: isList#(n____(V1,V2)) -> isList#(activate(V1)) p9: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p10: and#(tt(),X) -> activate#(X) p11: isList#(V) -> activate#(V) p12: isList#(V) -> isNeList#(activate(V)) p13: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p14: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p15: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p16: isNeList#(V) -> activate#(V) p17: isNePal#(n____(I,n____(P,I))) -> activate#(I) p18: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p19: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((1,0),(1,0)) x1 + (14,39) n__isPal_A(x1) = ((1,0),(1,0)) x1 + (17,0) isPal#_A(x1) = ((1,0),(0,0)) x1 + (16,1) isNePal#_A(x1) = ((1,0),(0,0)) x1 + (15,0) activate_A(x1) = ((1,0),(1,1)) x1 + (0,36) n_____A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (26,37) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (19,0) isNeList#_A(x1) = ((1,0),(1,1)) x1 + (20,40) n__isList_A(x1) = x1 + (22,0) isList#_A(x1) = ((1,0),(0,0)) x1 + (21,38) and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (2,19) isList_A(x1) = x1 + (22,0) tt_A() = (13,37) isNeList_A(x1) = ((1,0),(1,0)) x1 + (19,54) isQid_A(x1) = (14,54) isNePal_A(x1) = ((1,0),(1,0)) x1 + (15,1) and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (3,24) ___A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (26,38) nil_A() = (14,39) isPal_A(x1) = ((1,0),(1,0)) x1 + (17,37) n__nil_A() = (14,38) a_A() = (1,2) n__a_A() = (1,1) e_A() = (14,39) n__e_A() = (14,38) i_A() = (14,39) n__i_A() = (14,38) o_A() = (1,39) n__o_A() = (1,38) u_A() = (1,39) n__u_A() = (1,38) precedence: n____ = n__isList = isList > o > activate = isNePal = and = __ = isPal = n__o > n__isPal > n__isNeList = isNeList = isQid > isNeList# > activate# = isPal# = isNePal# = isList# = and# > tt = a = n__a = e = n__e = i = n__i = u = n__u > nil = n__nil partial status: pi(activate#) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n____) = [] pi(n__isNeList) = [] pi(isNeList#) = [1] pi(n__isList) = [] pi(isList#) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isQid) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [1] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: activate#(n__isNeList(X)) -> isNeList#(X) p4: isNeList#(n____(V1,V2)) -> activate#(V1) p5: activate#(n__isList(X)) -> isList#(X) p6: isList#(n____(V1,V2)) -> activate#(V2) p7: isList#(n____(V1,V2)) -> isList#(activate(V1)) p8: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p9: and#(tt(),X) -> activate#(X) p10: isList#(V) -> activate#(V) p11: isList#(V) -> isNeList#(activate(V)) p12: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p13: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p14: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p15: isNeList#(V) -> activate#(V) p16: isNePal#(n____(I,n____(P,I))) -> activate#(I) p17: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p18: isNePal#(V) -> activate#(V) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n__isPal(X)) -> isPal#(X) p2: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(V) -> activate#(V) p4: activate#(n__isList(X)) -> isList#(X) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(V) -> activate#(V) p7: activate#(n__isNeList(X)) -> isNeList#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: and#(tt(),X) -> activate#(X) p10: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p11: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p12: isNeList#(n____(V1,V2)) -> activate#(V1) p13: isList#(V) -> activate#(V) p14: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p15: isList#(n____(V1,V2)) -> isList#(activate(V1)) p16: isList#(n____(V1,V2)) -> activate#(V2) p17: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p18: isNePal#(n____(I,n____(P,I))) -> activate#(I) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((1,0),(1,1)) x1 + (1,3) n__isPal_A(x1) = x1 + (0,88) isPal#_A(x1) = ((1,0),(1,1)) x1 + (1,89) isNePal#_A(x1) = ((1,0),(1,1)) x1 + (1,4) activate_A(x1) = x1 + (0,39) n__isList_A(x1) = ((1,0),(1,1)) x1 + (29,0) isList#_A(x1) = ((1,0),(1,0)) x1 + (3,31) isNeList#_A(x1) = ((1,0),(1,0)) x1 + (2,27) n__isNeList_A(x1) = x1 + (3,20) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (31,60) and#_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (3,19) isList_A(x1) = ((1,0),(1,1)) x1 + (29,22) tt_A() = (2,2) isNeList_A(x1) = x1 + (3,20) isQid_A(x1) = ((1,0),(0,0)) x1 + (0,3) isNePal_A(x1) = ((1,0),(0,0)) x1 + (0,125) and_A(x1,x2) = x2 + (1,40) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (31,61) nil_A() = (3,4) isPal_A(x1) = x1 + (0,126) n__nil_A() = (3,3) a_A() = (3,2) n__a_A() = (3,1) e_A() = (3,4) n__e_A() = (3,3) i_A() = (3,2) n__i_A() = (3,1) o_A() = (3,4) n__o_A() = (3,3) u_A() = (3,3) n__u_A() = (3,3) precedence: activate# = isNePal# = n__isList = isList# = isNeList# = isList = __ = n__nil = n__i > isPal# > n__isPal = activate = isQid = isNePal = and = isPal = a = e = o > n__isNeList = isNeList = i > n____ = and# = tt = nil = n__a = n__e = n__o = u = n__u partial status: pi(activate#) = [] pi(n__isPal) = [] pi(isPal#) = [] pi(isNePal#) = [] pi(activate) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(n__isNeList) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [1] pi(isQid) = [] pi(isNePal) = [] pi(and) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] 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: isPal#(V) -> isNePal#(activate(V)) p2: isNePal#(V) -> activate#(V) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isNeList#(V) -> activate#(V) p6: activate#(n__isNeList(X)) -> isNeList#(X) p7: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p8: and#(tt(),X) -> activate#(X) p9: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p10: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p11: isNeList#(n____(V1,V2)) -> activate#(V1) p12: isList#(V) -> activate#(V) p13: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p14: isList#(n____(V1,V2)) -> isList#(activate(V1)) p15: isList#(n____(V1,V2)) -> activate#(V2) p16: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p17: isNePal#(n____(I,n____(P,I))) -> activate#(I) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {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: activate#(n__isList(X)) -> isList#(X) p2: isList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isNeList(X)) -> isNeList#(X) p4: isNeList#(n____(V1,V2)) -> activate#(V1) p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: and#(tt(),X) -> activate#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: isNeList#(V) -> activate#(V) p10: isList#(n____(V1,V2)) -> isList#(activate(V1)) p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p12: isList#(V) -> activate#(V) p13: isList#(V) -> isNeList#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((1,0),(0,0)) x1 + (3,3) n__isList_A(x1) = ((1,0),(0,0)) x1 + (0,4) isList#_A(x1) = ((1,0),(0,0)) x1 + (3,3) n_____A(x1,x2) = ((1,0),(0,0)) x1 + x2 n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (0,4) isNeList#_A(x1) = ((1,0),(0,0)) x1 + (3,3) activate_A(x1) = ((1,0),(1,1)) x1 + (0,7) and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,4) isNeList_A(x1) = ((1,0),(0,0)) x1 + (0,5) tt_A() = (2,2) isList_A(x1) = ((1,0),(0,0)) x1 + (0,6) isNePal_A(x1) = ((1,0),(1,0)) x1 + (3,8) isQid_A(x1) = ((1,0),(0,0)) x1 + (0,3) and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 n__isPal_A(x1) = ((1,0),(0,0)) x1 + (3,0) ___A(x1,x2) = ((1,0),(0,0)) x1 + x2 nil_A() = (3,2) isPal_A(x1) = ((1,0),(1,0)) x1 + (3,9) n__nil_A() = (3,1) n__a_A() = (3,3) n__e_A() = (2,1) n__i_A() = (3,3) n__o_A() = (3,3) n__u_A() = (2,3) a_A() = (3,4) e_A() = (2,2) i_A() = (3,4) o_A() = (3,4) u_A() = (2,4) precedence: activate# = isList# = isNeList# = activate = and# = isNeList = tt = isList = isQid = and = n__isPal = nil = isPal > n__isList = isNePal = __ > n____ = n__isNeList > n__nil > n__a = n__e = n__i = n__o = n__u = a = e = i = o = u partial status: pi(activate#) = [] pi(n__isList) = [] pi(isList#) = [] pi(n____) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(activate) = [] pi(and#) = [] pi(isNeList) = [] pi(tt) = [] pi(isList) = [] pi(isNePal) = [] pi(isQid) = [] pi(and) = [] pi(n__isPal) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p11 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isList(X)) -> isList#(X) p2: isList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isNeList(X)) -> isNeList#(X) p4: isNeList#(n____(V1,V2)) -> activate#(V1) p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: and#(tt(),X) -> activate#(X) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: isNeList#(V) -> activate#(V) p10: isList#(n____(V1,V2)) -> isList#(activate(V1)) p11: isList#(V) -> activate#(V) p12: isList#(V) -> isNeList#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n__isList(X)) -> isList#(X) p2: isList#(V) -> isNeList#(activate(V)) p3: isNeList#(V) -> activate#(V) p4: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p6: and#(tt(),X) -> activate#(X) p7: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p8: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p9: isNeList#(n____(V1,V2)) -> activate#(V1) p10: isList#(V) -> activate#(V) p11: isList#(n____(V1,V2)) -> isList#(activate(V1)) p12: isList#(n____(V1,V2)) -> activate#(V2) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = x1 + (5,11) n__isList_A(x1) = ((1,0),(1,1)) x1 + (0,16) isList#_A(x1) = ((1,0),(1,1)) x1 + (5,26) isNeList#_A(x1) = x1 + (5,21) activate_A(x1) = ((1,0),(1,1)) x1 + (0,4) n__isNeList_A(x1) = x1 + (0,11) n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (7,0) and#_A(x1,x2) = x2 + (6,12) isList_A(x1) = ((1,0),(1,1)) x1 + (0,19) tt_A() = (0,12) isNeList_A(x1) = x1 + (0,14) isNePal_A(x1) = ((1,0),(0,0)) x1 + (4,1) isQid_A(x1) = (0,13) and_A(x1,x2) = ((1,0),(1,1)) x2 + (1,5) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (5,2) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (7,1) nil_A() = (1,14) isPal_A(x1) = ((1,0),(0,0)) x1 + (5,3) n__nil_A() = (1,13) n__a_A() = (1,13) n__e_A() = (1,13) n__i_A() = (1,13) n__o_A() = (0,13) n__u_A() = (1,13) a_A() = (1,14) e_A() = (1,14) i_A() = (1,14) o_A() = (0,14) u_A() = (1,14) precedence: activate# = isList# = isNeList# = activate = and# = isList = isNeList = isNePal = and = n__isPal = __ = isPal > n__isNeList > a > n____ = tt = isQid > nil = n__nil = n__a = n__e = e > n__i = n__o = n__u = i = o = u > n__isList partial status: pi(activate#) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [] pi(n__isNeList) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isNePal) = [] pi(isQid) = [] pi(and) = [] pi(n__isPal) = [] pi(__) = [] pi(nil) = [] pi(isPal) = [] pi(n__nil) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: activate#(n__isList(X)) -> isList#(X) p2: isList#(V) -> isNeList#(activate(V)) p3: isNeList#(V) -> activate#(V) p4: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p6: and#(tt(),X) -> activate#(X) p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p8: isNeList#(n____(V1,V2)) -> activate#(V1) p9: isList#(V) -> activate#(V) p10: isList#(n____(V1,V2)) -> isList#(activate(V1)) p11: isList#(n____(V1,V2)) -> activate#(V2) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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: activate#(n__isList(X)) -> isList#(X) p2: isList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isNeList(X)) -> isNeList#(X) p4: isNeList#(n____(V1,V2)) -> activate#(V1) p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p6: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p7: and#(tt(),X) -> activate#(X) p8: isNeList#(V) -> activate#(V) p9: isList#(n____(V1,V2)) -> isList#(activate(V1)) p10: isList#(V) -> activate#(V) p11: isList#(V) -> isNeList#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = ((1,0),(0,0)) x1 + (1,24) n__isList_A(x1) = x1 + (4,0) isList#_A(x1) = ((1,0),(0,0)) x1 + (3,25) n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (15,10) n__isNeList_A(x1) = x1 + (3,1) isNeList#_A(x1) = ((1,0),(0,0)) x1 + (2,4) activate_A(x1) = ((1,0),(1,1)) x1 and#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (9,1) isList_A(x1) = ((1,0),(1,1)) x1 + (4,3) tt_A() = (24,23) isNePal_A(x1) = ((1,0),(1,1)) x1 + (3,25) isQid_A(x1) = x1 + (2,21) and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,9) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (25,0) n__a_A() = (25,1) n__e_A() = (25,24) n__i_A() = (25,24) n__o_A() = (23,1) n__u_A() = (23,1) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (15,11) nil_A() = (25,48) isNeList_A(x1) = x1 + (3,2) isPal_A(x1) = ((1,0),(0,0)) x1 + (25,24) n__nil_A() = (25,24) a_A() = (25,2) e_A() = (25,25) i_A() = (25,25) o_A() = (23,2) u_A() = (23,2) precedence: activate = isList = n__a = __ = isPal = a > isNePal > isNeList > n__isList > n__o = e = o > activate# = isList# = isNeList# = and# = n__isPal > n__isNeList = isQid > n__e = nil > tt = n__i = n__u = n__nil = i = u > n____ = and partial status: pi(activate#) = [] pi(n__isList) = [1] pi(isList#) = [] pi(n____) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(activate) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNePal) = [] pi(isQid) = [] pi(and) = [] pi(n__isPal) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [] pi(nil) = [] pi(isNeList) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: isList#(n____(V1,V2)) -> activate#(V2) p2: activate#(n__isNeList(X)) -> isNeList#(X) p3: isNeList#(n____(V1,V2)) -> activate#(V1) p4: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p6: and#(tt(),X) -> activate#(X) p7: isNeList#(V) -> activate#(V) p8: isList#(n____(V1,V2)) -> isList#(activate(V1)) p9: isList#(V) -> activate#(V) p10: isList#(V) -> isNeList#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p8} {p2, p3, p4, p5, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isList#(n____(V1,V2)) -> isList#(activate(V1)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isList#_A(x1) = x1 + (1,5) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (6,23) activate_A(x1) = x1 + (0,19) and_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (6,18) tt_A() = (2,2) isNePal_A(x1) = ((1,0),(1,0)) x1 + (4,26) isQid_A(x1) = ((0,0),(1,0)) x1 + (3,39) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (5,24) n__a_A() = (1,1) n__e_A() = (1,1) n__i_A() = (3,1) n__o_A() = (3,3) n__u_A() = (3,3) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (6,24) nil_A() = (1,2) isList_A(x1) = ((1,0),(1,0)) x1 + (4,46) isNeList_A(x1) = ((1,0),(1,0)) x1 + (4,40) n__nil_A() = (1,1) n__isList_A(x1) = ((1,0),(1,0)) x1 + (4,28) n__isNeList_A(x1) = ((1,0),(1,0)) x1 + (4,22) isPal_A(x1) = ((1,0),(0,0)) x1 + (5,25) a_A() = (1,2) e_A() = (1,2) i_A() = (3,2) o_A() = (3,4) u_A() = (3,4) precedence: isList = isNeList > isNePal = n__isPal = isPal > activate = and = n__a = n__u = n__nil = n__isList = a = u > isQid = e > n__e = __ > isList# > n____ = n__o = n__isNeList = o > tt > i > n__i > nil partial status: pi(isList#) = [] pi(n____) = [] pi(activate) = [] pi(and) = [] pi(tt) = [] pi(isNePal) = [] pi(isQid) = [] pi(n__isPal) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [] pi(nil) = [] pi(isList) = [] pi(isNeList) = [] pi(n__nil) = [] pi(n__isList) = [] pi(n__isNeList) = [] pi(isPal) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(V) -> activate#(V) p3: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p4: and#(tt(),X) -> activate#(X) p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p6: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: activate#_A(x1) = x1 n__isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,3) isNeList#_A(x1) = x1 + (1,2) n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (31,12) and#_A(x1,x2) = x2 + (1,1) isList_A(x1) = x1 + (25,51) activate_A(x1) = ((1,0),(1,1)) x1 + (0,13) tt_A() = (2,12) isNePal_A(x1) = ((1,0),(1,0)) x1 + (6,1) isQid_A(x1) = (3,20) and_A(x1,x2) = x1 + x2 + (1,2) n__isPal_A(x1) = ((1,0),(1,0)) x1 + (63,1) n__a_A() = (3,13) n__e_A() = (1,1) n__i_A() = (1,1) n__o_A() = (3,1) n__u_A() = (3,13) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (31,13) nil_A() = (3,1) isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,20) n__isList_A(x1) = x1 + (25,14) isPal_A(x1) = ((1,0),(1,0)) x1 + (63,12) n__nil_A() = (3,0) a_A() = (3,14) e_A() = (1,2) i_A() = (1,2) o_A() = (3,2) u_A() = (3,14) precedence: isNeList# = and# = n__a > isNePal > activate# = activate = and = n__isPal = isPal > n____ = isList = tt = isQid = __ = nil = n__nil > n__isNeList = isNeList > n__i = n__o = a = e = i = o > n__e = n__u = n__isList = u partial status: pi(activate#) = [] pi(n__isNeList) = [1] pi(isNeList#) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(activate) = [] pi(tt) = [] pi(isNePal) = [] pi(isQid) = [] pi(and) = [] pi(n__isPal) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [1, 2] pi(nil) = [] pi(isNeList) = [1] pi(n__isList) = [] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: isNeList#(V) -> activate#(V) p2: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p3: and#(tt(),X) -> activate#(X) p4: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p5: isNeList#(n____(V1,V2)) -> activate#(V1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isNeList#_A(x1) = ((0,0),(1,0)) x1 + (19,9) n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (18,8) activate_A(x1) = ((1,0),(1,1)) x1 + (0,12) and_A(x1,x2) = ((1,0),(1,1)) x2 + (12,13) tt_A() = (2,8) isNePal_A(x1) = x1 + (4,43) isQid_A(x1) = (3,9) n__isPal_A(x1) = ((1,0),(0,0)) x1 + (28,17) n__a_A() = (1,7) n__e_A() = (3,9) n__i_A() = (3,9) n__o_A() = (1,1) n__u_A() = (3,9) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (18,9) nil_A() = (1,2) isList_A(x1) = ((1,0),(1,0)) x1 + (5,11) isNeList_A(x1) = ((1,0),(1,0)) x1 + (4,10) n__nil_A() = (1,1) n__isList_A(x1) = ((1,0),(0,0)) x1 + (5,9) n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (4,8) isPal_A(x1) = ((1,0),(0,0)) x1 + (28,56) a_A() = (1,8) e_A() = (3,10) i_A() = (3,9) o_A() = (1,2) u_A() = (3,10) precedence: n__i = i > isNeList# > and = isList = isNeList > activate = __ = nil = n__nil > n__e = e > a > n__a > n__o = n__isList = o > n__isPal = n__u = isPal = u > n____ = tt = isNePal = isQid = n__isNeList partial status: pi(isNeList#) = [] pi(n____) = [] pi(activate) = [1] pi(and) = [] pi(tt) = [] pi(isNePal) = [] pi(isQid) = [] pi(n__isPal) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [1, 2] pi(nil) = [] pi(isList) = [] pi(isNeList) = [] pi(n__nil) = [] pi(n__isList) = [] pi(n__isNeList) = [] pi(isPal) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) p2: __#(__(X,Y),Z) -> __#(Y,Z) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The set of usable rules consists of r1, r2, r3, r21 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: __#_A(x1,x2) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x2 + (1,1) ___A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (2,0) nil_A() = (1,1) n_____A(x1,x2) = (1,0) precedence: __ > __# = nil = n____ partial status: pi(__#) = [1] pi(__) = [] pi(nil) = [] pi(n____) = [] 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: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: and(tt(),X) -> activate(X) r5: isList(V) -> isNeList(activate(V)) r6: isList(n__nil()) -> tt() r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) r8: isNeList(V) -> isQid(activate(V)) r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) r11: isNePal(V) -> isQid(activate(V)) r12: isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) r13: isPal(V) -> isNePal(activate(V)) r14: isPal(n__nil()) -> tt() r15: isQid(n__a()) -> tt() r16: isQid(n__e()) -> tt() r17: isQid(n__i()) -> tt() r18: isQid(n__o()) -> tt() r19: isQid(n__u()) -> tt() r20: nil() -> n__nil() r21: __(X1,X2) -> n____(X1,X2) r22: isList(X) -> n__isList(X) r23: isNeList(X) -> n__isNeList(X) r24: isPal(X) -> n__isPal(X) r25: a() -> n__a() r26: e() -> n__e() r27: i() -> n__i() r28: o() -> n__o() r29: u() -> n__u() r30: activate(n__nil()) -> nil() r31: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r32: activate(n__isList(X)) -> isList(X) r33: activate(n__isNeList(X)) -> isNeList(X) r34: activate(n__isPal(X)) -> isPal(X) r35: activate(n__a()) -> a() r36: activate(n__e()) -> e() r37: activate(n__i()) -> i() r38: activate(n__o()) -> o() r39: activate(n__u()) -> u() r40: activate(X) -> X The set of usable rules consists of r1, r2, r3, r21 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: __#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (1,2) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,1) nil_A() = (1,1) n_____A(x1,x2) = (1,2) precedence: __# = __ = n____ > nil partial status: pi(__#) = [] pi(__) = [] pi(nil) = [] pi(n____) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.