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,__(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)) -> __(X1,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,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p23: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) p24: isNePal#(n____(I,__(P,I))) -> activate#(I) p25: isNePal#(n____(I,__(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)) -> __#(X1,X2) p30: activate#(n__isList(X)) -> isList#(X) p31: activate#(n__isNeList(X)) -> isNeList#(X) p32: activate#(n__isPal(X)) -> isPal#(X) p33: activate#(n__a()) -> a#() p34: activate#(n__e()) -> e#() p35: activate#(n__i()) -> i#() p36: activate#(n__o()) -> o#() p37: 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,__(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)) -> __(X1,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} {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,__(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: isList#(n____(V1,V2)) -> activate#(V1) 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)) -> activate#(V1) 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,__(P,I))) -> activate#(I) p22: isNePal#(n____(I,__(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 12 activate#_A(x1) = max{1, x1} n__isPal_A(x1) = x1 + 16 isNePal#_A(x1) = x1 + 6 activate_A(x1) = max{5, x1} n_____A(x1,x2) = max{21, x1 + 16, x2} ___A(x1,x2) = max{21, x1 + 16, x2} n__isNeList_A(x1) = max{7, x1} isNeList#_A(x1) = max{6, x1} n__isList_A(x1) = max{15, x1} isList#_A(x1) = max{15, x1} and#_A(x1,x2) = max{x1 - 8, x2} isList_A(x1) = max{15, x1} tt_A = 16 isNeList_A(x1) = max{7, x1} isQid_A(x1) = max{0, x1 - 5} isNePal_A(x1) = x1 + 10 and_A(x1,x2) = max{5, x1 - 16, x2} nil_A = 17 isPal_A(x1) = x1 + 16 n__nil_A = 17 a_A = 22 n__a_A = 22 e_A = 22 n__e_A = 22 i_A = 22 n__i_A = 22 o_A = 22 n__o_A = 22 u_A = 22 n__u_A = 22 precedence: e = n__e > isPal# > nil = n__nil = a = n__a = u = n__u > n____ = __ > n__isPal = isPal > n__isList = isList > isList# > activate = isNeList = isNePal = and = o = n__o > isNePal# = n__isNeList = isNeList# = and# = i = n__i > activate# > tt = isQid partial status: pi(isPal#) = [1] pi(activate#) = [1] pi(n__isPal) = [1] pi(isNePal#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(__) = [1, 2] pi(n__isNeList) = [1] pi(isNeList#) = [1] pi(n__isList) = [1] pi(isList#) = [1] pi(and#) = [2] pi(isList) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isQid) = [] pi(isNePal) = [1] pi(and) = [2] pi(nil) = [] pi(isPal) = [1] 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: p8 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,__(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#(V1) 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)) -> activate#(V1) 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,__(P,I))) -> activate#(I) p21: isNePal#(n____(I,__(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,__(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)) -> __(X1,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: isPal#(V) -> activate#(V) 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,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p12: isNePal#(n____(I,__(P,I))) -> activate#(I) p13: isNePal#(n____(I,__(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#(V1) 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) p22: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 14 activate#_A(x1) = max{3, x1 - 5} n__isList_A(x1) = max{91, x1 + 69} isList#_A(x1) = x1 + 64 isNeList#_A(x1) = x1 + 64 activate_A(x1) = x1 n__isNeList_A(x1) = x1 + 69 n_____A(x1,x2) = max{x1 + 40, x2} and#_A(x1,x2) = max{1, x1 - 28, x2 - 5} isList_A(x1) = max{91, x1 + 69} tt_A = 32 n__isPal_A(x1) = max{39, x1 + 20} isNePal#_A(x1) = x1 + 13 ___A(x1,x2) = max{x1 + 40, x2} isQid_A(x1) = max{33, x1 - 2} isNeList_A(x1) = x1 + 69 isNePal_A(x1) = max{35, x1} and_A(x1,x2) = max{x1 + 1, x2} nil_A = 33 isPal_A(x1) = max{39, x1 + 20} n__nil_A = 33 a_A = 1 n__a_A = 1 e_A = 33 n__e_A = 33 i_A = 1 n__i_A = 1 o_A = 1 n__o_A = 1 u_A = 34 n__u_A = 34 precedence: isPal# = activate# = n__isList = isList# = isNeList# = activate = n__isNeList = n____ = and# = isList = tt = n__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(isPal#) = [] pi(activate#) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [] pi(n__isNeList) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(__) = [] pi(isQid) = [] pi(isNeList) = [] pi(isNePal) = [] pi(and) = [] 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: p20 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__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,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p12: isNePal#(n____(I,__(P,I))) -> activate#(I) p13: isNePal#(n____(I,__(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#(V1) p19: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p20: isNeList#(n____(V1,V2)) -> activate#(V1) p21: isNeList#(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,__(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)) -> __(X1,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: isPal#(V) -> activate#(V) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,__(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#(V1) 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)) -> 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,__(P,I))) -> activate#(I) p20: isNePal#(n____(I,__(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = max{8, x1 - 2} activate#_A(x1) = max{8, x1 - 8} n__isPal_A(x1) = x1 + 7 isNePal#_A(x1) = max{8, x1 - 2} activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 23, x2} ___A(x1,x2) = max{x1 + 23, x2} n__isNeList_A(x1) = max{23, x1} isNeList#_A(x1) = max{9, x1 - 8} n__isList_A(x1) = max{23, x1} isList#_A(x1) = max{10, x1 - 8} and#_A(x1,x2) = max{11, x1 - 32, x2 - 8} isList_A(x1) = max{23, x1} tt_A = 2 isNeList_A(x1) = max{23, x1} isQid_A(x1) = max{3, x1 - 32} isNePal_A(x1) = max{3, x1 - 16} and_A(x1,x2) = max{7, x2} nil_A = 3 isPal_A(x1) = x1 + 7 n__nil_A = 3 a_A = 1 n__a_A = 1 e_A = 35 n__e_A = 35 i_A = 3 n__i_A = 3 o_A = 1 n__o_A = 1 u_A = 1 n__u_A = 1 precedence: n____ = __ > n__isList = isList = tt > isNePal > n__isPal = isPal > activate = isNeList = and = u > isPal# = activate# = isNePal# = n__isNeList = isNeList# = isList# = and# = isQid = nil = n__nil = a = n__a = e = n__e = i = n__i = o = n__o = n__u partial status: pi(isPal#) = [] pi(activate#) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n____) = [1, 2] pi(__) = [1, 2] pi(n__isNeList) = [1] pi(isNeList#) = [] pi(n__isList) = [1] pi(isList#) = [] pi(and#) = [] pi(isList) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isQid) = [] pi(isNePal) = [] pi(and) = [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: p4 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: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> activate#(V2) p6: activate#(n__isList(X)) -> isList#(X) p7: isList#(n____(V1,V2)) -> activate#(V1) 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)) -> 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,__(P,I))) -> activate#(I) p19: isNePal#(n____(I,__(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,__(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)) -> __(X1,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: isPal#(V) -> activate#(V) 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,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) p12: isNePal#(n____(I,__(P,I))) -> activate#(I) p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p14: isList#(V) -> activate#(V) p15: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p16: isList#(n____(V1,V2)) -> isList#(activate(V1)) p17: isList#(n____(V1,V2)) -> activate#(V1) p18: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p19: isNeList#(n____(V1,V2)) -> activate#(V1) p20: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 34 activate#_A(x1) = max{0, x1 - 46} n__isList_A(x1) = max{10, x1} isList#_A(x1) = max{0, x1 - 46} isNeList#_A(x1) = max{0, x1 - 46} activate_A(x1) = max{9, x1} n__isNeList_A(x1) = max{1, x1} n_____A(x1,x2) = max{67, x1 + 45, x2} and#_A(x1,x2) = max{0, x1 - 1, x2 - 46} isList_A(x1) = max{10, x1} tt_A = 3 n__isPal_A(x1) = x1 + 81 isNePal#_A(x1) = x1 + 24 ___A(x1,x2) = max{67, x1 + 45, x2} isQid_A(x1) = max{4, x1 - 10} isNeList_A(x1) = max{5, x1} isNePal_A(x1) = x1 + 46 and_A(x1,x2) = max{9, x1 - 3, x2} nil_A = 8 isPal_A(x1) = x1 + 81 n__nil_A = 3 a_A = 9 n__a_A = 2 e_A = 14 n__e_A = 14 i_A = 10 n__i_A = 10 o_A = 14 n__o_A = 14 u_A = 14 n__u_A = 14 precedence: n____ = __ = o = n__o > isNePal# > isPal# = n__isList = isList = isNePal > activate = n__isNeList = tt = n__isPal = isQid = isNeList = and = nil = isPal = a = e = n__e = i = n__i = u = n__u > activate# = isList# = isNeList# = and# = n__nil = n__a partial status: pi(isPal#) = [1] pi(activate#) = [] pi(n__isList) = [1] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [1] pi(n__isNeList) = [1] pi(n____) = [1, 2] pi(and#) = [] pi(isList) = [1] pi(tt) = [] pi(n__isPal) = [] pi(isNePal#) = [1] pi(__) = [1, 2] pi(isQid) = [] pi(isNeList) = [1] pi(isNePal) = [] pi(and) = [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: p11 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__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,__(P,I))) -> activate#(I) p12: isNeList#(n____(V1,V2)) -> isList#(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#(V1) p17: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p18: isNeList#(n____(V1,V2)) -> activate#(V1) p19: isNeList#(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,__(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)) -> __(X1,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: isPal#(V) -> activate#(V) p2: activate#(n__isPal(X)) -> isPal#(X) p3: isPal#(V) -> isNePal#(activate(V)) p4: isNePal#(n____(I,__(P,I))) -> activate#(I) 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#(V1) 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)) -> 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#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = max{15, x1 - 16} activate#_A(x1) = max{14, x1 - 21} n__isPal_A(x1) = max{36, x1 + 6} isNePal#_A(x1) = max{14, x1 - 21} activate_A(x1) = max{13, x1} n_____A(x1,x2) = max{37, x1 + 19, x2} ___A(x1,x2) = max{37, x1 + 19, x2} n__isNeList_A(x1) = x1 + 7 isNeList#_A(x1) = max{14, x1 - 14} n__isList_A(x1) = max{25, x1 + 7} isList#_A(x1) = max{14, x1 - 14} and#_A(x1,x2) = max{0, x1 - 2, x2 - 21} isList_A(x1) = max{25, x1 + 7} tt_A = 26 isNeList_A(x1) = max{13, x1 + 7} isNePal_A(x1) = max{36, x1 - 7} isQid_A(x1) = max{1, x1 - 7} and_A(x1,x2) = max{26, x1 - 26, x2} nil_A = 27 isPal_A(x1) = max{36, x1 + 6} n__nil_A = 27 n__a_A = 34 n__e_A = 34 n__i_A = 34 n__o_A = 34 n__u_A = 34 a_A = 34 e_A = 34 i_A = 34 o_A = 34 u_A = 34 precedence: n__isPal = activate = n____ = __ = n__isNeList = n__isList = isList = tt = isNeList = isNePal = isQid = and = nil = isPal = n__nil = n__e = n__o = e = o > isPal# = activate# = isNePal# = isNeList# = isList# = and# = n__i = i = u > n__u = a > n__a partial status: pi(isPal#) = [] pi(activate#) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(activate) = [] pi(n____) = [] pi(__) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n__isList) = [] pi(isList#) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isNePal) = [] pi(isQid) = [] pi(and) = [] 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: p9 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,__(P,I))) -> activate#(I) 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#(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)) -> 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#(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,__(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)) -> __(X1,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: isPal#(V) -> activate#(V) 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,__(P,I))) -> activate#(I) p12: isNeList#(n____(V1,V2)) -> isList#(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)) -> activate#(V1) p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p17: isNeList#(n____(V1,V2)) -> activate#(V1) p18: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 4 activate#_A(x1) = max{0, x1 - 9} n__isList_A(x1) = x1 + 8 isList#_A(x1) = max{0, x1 - 1} isNeList#_A(x1) = max{0, x1 - 1} activate_A(x1) = x1 n__isNeList_A(x1) = x1 + 8 n_____A(x1,x2) = max{25, x1 + 15, x2} and#_A(x1,x2) = max{1, x1 - 10, x2 - 9} isList_A(x1) = x1 + 8 tt_A = 2 n__isPal_A(x1) = x1 + 14 isNePal#_A(x1) = max{3, x1 + 1} ___A(x1,x2) = max{25, x1 + 15, x2} isNeList_A(x1) = x1 + 8 isNePal_A(x1) = x1 + 13 isQid_A(x1) = 4 and_A(x1,x2) = max{24, x1 - 3, x2} nil_A = 3 isPal_A(x1) = x1 + 14 n__nil_A = 3 n__a_A = 1 n__e_A = 3 n__i_A = 3 n__o_A = 3 n__u_A = 3 a_A = 1 e_A = 3 i_A = 3 o_A = 3 u_A = 3 precedence: isPal# = activate# = isList# = isNeList# = activate = n__isNeList = n____ = and# = isList = isNePal# = __ = isNeList = isQid = and > n__isList > o > n__isPal = isPal > isNePal > nil = n__nil = u > a > tt = n__e = n__o = e > n__i = n__u = i > n__a partial status: pi(isPal#) = [] pi(activate#) = [] pi(n__isList) = [] pi(isList#) = [] pi(isNeList#) = [] pi(activate) = [] pi(n__isNeList) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(n__isPal) = [] pi(isNePal#) = [] pi(__) = [] pi(isNeList) = [] pi(isNePal) = [1] pi(isQid) = [] pi(and) = [] 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: p15 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__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,__(P,I))) -> activate#(I) p12: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p13: isList#(V) -> activate#(V) p14: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p15: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p16: isNeList#(n____(V1,V2)) -> activate#(V1) p17: isNeList#(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,__(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)) -> __(X1,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} -- 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,__(P,I))) -> activate#(I) 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)) -> 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)) -> activate#(V1) p13: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p14: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p15: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p16: isNeList#(V) -> activate#(V) p17: 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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 20 activate#_A(x1) = x1 + 16 n__isPal_A(x1) = x1 + 24 isNePal#_A(x1) = max{19, x1 + 17} activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 23, x2} ___A(x1,x2) = max{x1 + 23, x2} n__isNeList_A(x1) = max{6, x1} isNeList#_A(x1) = x1 + 16 n__isList_A(x1) = max{11, x1} isList#_A(x1) = x1 + 16 and#_A(x1,x2) = max{x1 + 13, x2 + 16} isList_A(x1) = max{11, x1} tt_A = 4 isNeList_A(x1) = max{6, x1} isNePal_A(x1) = max{24, x1 + 13} isQid_A(x1) = max{5, x1} and_A(x1,x2) = max{1, x1 - 12, x2} nil_A = 5 isPal_A(x1) = x1 + 24 n__nil_A = 5 n__a_A = 5 n__e_A = 5 n__i_A = 5 n__o_A = 5 n__u_A = 5 a_A = 5 e_A = 5 i_A = 5 o_A = 5 u_A = 5 precedence: activate# = isNePal# = isNeList# = isList# = and# > isPal# > n__isPal = tt = isNePal = isPal > n__i = i > n__o = o > n____ = __ > n__isList = isList > n__isNeList = isNeList > and = n__u = u > activate = isQid = nil = n__nil = n__a = n__e = a = e partial status: pi(isPal#) = [1] pi(activate#) = [] pi(n__isPal) = [1] pi(isNePal#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(__) = [1, 2] pi(n__isNeList) = [1] pi(isNeList#) = [] pi(n__isList) = [1] pi(isList#) = [] pi(and#) = [] pi(isList) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isNePal) = [] pi(isQid) = [1] pi(and) = [2] pi(nil) = [] pi(isPal) = [1] 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: p2 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: isPal#(V) -> isNePal#(activate(V)) p3: isNePal#(n____(I,__(P,I))) -> activate#(I) p4: activate#(n__isNeList(X)) -> isNeList#(X) p5: isNeList#(n____(V1,V2)) -> activate#(V2) p6: activate#(n__isList(X)) -> isList#(X) p7: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p8: and#(tt(),X) -> activate#(X) p9: isList#(V) -> activate#(V) p10: isList#(V) -> isNeList#(activate(V)) p11: isNeList#(n____(V1,V2)) -> activate#(V1) p12: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p14: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p15: isNeList#(V) -> activate#(V) p16: 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,__(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)) -> __(X1,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, 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__isNeList(X)) -> isNeList#(X) p2: isNeList#(V) -> activate#(V) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p6: and#(tt(),X) -> activate#(X) p7: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p8: isList#(V) -> activate#(V) p9: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p10: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p11: isNeList#(n____(V1,V2)) -> activate#(V1) p12: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 + 6 n__isNeList_A(x1) = x1 isNeList#_A(x1) = x1 + 6 n__isList_A(x1) = max{3, x1} isList#_A(x1) = x1 + 6 activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 10, x2} and#_A(x1,x2) = max{x1 - 4, x2 + 6} isList_A(x1) = max{3, x1} tt_A = 6 isNeList_A(x1) = x1 isNePal_A(x1) = x1 + 9 isQid_A(x1) = max{0, x1 - 8} ___A(x1,x2) = max{x1 + 10, x2} and_A(x1,x2) = max{x1 + 7, x2} n__isPal_A(x1) = x1 + 9 nil_A = 7 isPal_A(x1) = x1 + 9 n__nil_A = 7 n__a_A = 15 n__e_A = 15 n__i_A = 15 n__o_A = 15 n__u_A = 15 a_A = 15 e_A = 15 i_A = 15 o_A = 15 u_A = 15 precedence: activate# = n__isNeList = isNeList# = n__isList = isList# = activate = n____ = and# = isList = tt = isNeList = isNePal = isQid = __ = and = n__isPal = nil = isPal = n__nil = n__a = n__e = n__i = n__o = n__u = a = e = i = o = u partial status: pi(activate#) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n__isList) = [] pi(isList#) = [] pi(activate) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(tt) = [] pi(isNeList) = [] pi(isNePal) = [] pi(isQid) = [] pi(__) = [] pi(and) = [] pi(n__isPal) = [] 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__isNeList(X)) -> isNeList#(X) p2: isNeList#(V) -> activate#(V) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p6: and#(tt(),X) -> activate#(X) p7: isList#(V) -> activate#(V) p8: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p9: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p10: isNeList#(n____(V1,V2)) -> activate#(V1) p11: isNeList#(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,__(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)) -> __(X1,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__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isList#(V) -> activate#(V) p7: isList#(V) -> isNeList#(activate(V)) p8: isNeList#(n____(V1,V2)) -> activate#(V1) p9: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p10: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p11: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = max{0, x1 - 40} n__isNeList_A(x1) = x1 + 53 isNeList#_A(x1) = x1 + 13 n_____A(x1,x2) = max{x1 + 30, x2} n__isList_A(x1) = x1 + 53 isList#_A(x1) = x1 + 13 and#_A(x1,x2) = max{1, x1 - 24, x2 - 40} isList_A(x1) = x1 + 53 activate_A(x1) = x1 tt_A = 25 isNeList_A(x1) = x1 + 53 isNePal_A(x1) = x1 + 28 isQid_A(x1) = 26 ___A(x1,x2) = max{x1 + 30, x2} and_A(x1,x2) = max{x1 + 7, x2} n__isPal_A(x1) = x1 + 28 nil_A = 1 isPal_A(x1) = x1 + 28 n__nil_A = 1 n__a_A = 26 n__e_A = 1 n__i_A = 26 n__o_A = 26 n__u_A = 1 a_A = 26 e_A = 1 i_A = 26 o_A = 26 u_A = 1 precedence: activate# = n__isNeList = isNeList# = n____ = n__isList = isList# = and# = isList = activate = tt = isNeList = isNePal = isQid = __ = and = n__isPal = nil = isPal = n__nil = n__a = n__e = n__i = n__o = n__u = a = e = i = o = u partial status: pi(activate#) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n____) = [] pi(n__isList) = [] pi(isList#) = [] pi(and#) = [] pi(isList) = [] pi(activate) = [] pi(tt) = [] pi(isNeList) = [] pi(isNePal) = [] pi(isQid) = [] pi(__) = [] pi(and) = [] pi(n__isPal) = [] 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: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isList#(V) -> isNeList#(activate(V)) p7: isNeList#(n____(V1,V2)) -> activate#(V1) p8: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p9: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p10: isNeList#(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,__(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)) -> __(X1,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} -- 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: activate#(n__isList(X)) -> isList#(X) p4: isList#(V) -> isNeList#(activate(V)) 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)) -> activate#(V1) p9: isNeList#(n____(V1,V2)) -> activate#(V2) p10: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 n__isNeList_A(x1) = max{4, x1} isNeList#_A(x1) = max{3, x1} n__isList_A(x1) = max{7, x1} isList#_A(x1) = max{6, x1} activate_A(x1) = max{6, x1} n_____A(x1,x2) = max{x1 + 17, x2} and#_A(x1,x2) = max{x1 + 4, x2} isList_A(x1) = max{7, x1} tt_A = 0 isNeList_A(x1) = max{4, x1} isNePal_A(x1) = max{4, x1 - 3} isQid_A(x1) = 0 ___A(x1,x2) = max{x1 + 17, x2} and_A(x1,x2) = max{x1 + 7, x2} n__isPal_A(x1) = max{8, x1 + 7} nil_A = 2 isPal_A(x1) = max{8, x1 + 7} n__nil_A = 1 n__a_A = 4 n__e_A = 4 n__i_A = 7 n__o_A = 4 n__u_A = 7 a_A = 5 e_A = 5 i_A = 7 o_A = 5 u_A = 7 precedence: isNePal > n____ = __ > n__isList = isList# = and# = isList > and > n__isPal = isPal > activate = nil = u > tt = isNeList = isQid > n__isNeList > isNeList# > activate# = n__a > n__nil = n__e = n__i = n__o = n__u = a = e = i = o partial status: pi(activate#) = [1] pi(n__isNeList) = [1] pi(isNeList#) = [1] pi(n__isList) = [1] pi(isList#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(and#) = [1, 2] pi(isList) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isNePal) = [] pi(isQid) = [] pi(__) = [1, 2] pi(and) = [2] pi(n__isPal) = [] 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: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(V) -> activate#(V) p3: activate#(n__isList(X)) -> isList#(X) p4: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: isNeList#(n____(V1,V2)) -> activate#(V1) p8: isNeList#(n____(V1,V2)) -> activate#(V2) p9: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V1) p7: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) p9: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 n__isNeList_A(x1) = max{2, x1} isNeList#_A(x1) = max{1, x1} n_____A(x1,x2) = max{x1 + 29, x2} n__isList_A(x1) = max{7, x1} isList#_A(x1) = max{6, x1} and#_A(x1,x2) = max{x1 - 15, x2} isList_A(x1) = max{7, x1} activate_A(x1) = max{5, x1} tt_A = 14 isNeList_A(x1) = max{3, x1} isNePal_A(x1) = x1 + 16 isQid_A(x1) = max{0, x1 - 4} ___A(x1,x2) = max{x1 + 29, x2} and_A(x1,x2) = max{4, x1 - 8, x2} n__isPal_A(x1) = x1 + 22 nil_A = 15 isPal_A(x1) = x1 + 22 n__nil_A = 15 n__a_A = 19 n__e_A = 19 n__i_A = 19 n__o_A = 19 n__u_A = 19 a_A = 19 e_A = 19 i_A = 19 o_A = 19 u_A = 19 precedence: n____ = __ = n__e = e > and > n__isList = isList > activate = nil = n__nil = a = i > n__i > u > n__isNeList = isNeList = isPal > isNePal > n__u > isNeList# > and# > isList# = n__isPal > activate# > tt = isQid = n__a = n__o = o partial status: pi(activate#) = [1] pi(n__isNeList) = [1] pi(isNeList#) = [1] pi(n____) = [1, 2] pi(n__isList) = [1] pi(isList#) = [1] pi(and#) = [2] pi(isList) = [1] pi(activate) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isNePal) = [1] pi(isQid) = [] pi(__) = [1, 2] pi(and) = [2] pi(n__isPal) = [1] 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: p8 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> activate#(V1) p7: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p8: isNeList#(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,__(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)) -> __(X1,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} -- 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: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: isNeList#(n____(V1,V2)) -> activate#(V1) p8: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 n__isNeList_A(x1) = max{6, x1} isNeList#_A(x1) = max{3, x1} n__isList_A(x1) = max{7, x1} isList#_A(x1) = max{3, x1} n_____A(x1,x2) = max{x1 + 15, x2} and#_A(x1,x2) = max{1, x1 - 8, x2} isList_A(x1) = max{7, x1} activate_A(x1) = max{2, x1} tt_A = 1 isNeList_A(x1) = max{6, x1} isNePal_A(x1) = x1 + 5 isQid_A(x1) = max{5, x1} ___A(x1,x2) = max{x1 + 15, x2} and_A(x1,x2) = max{6, x2} n__isPal_A(x1) = x1 + 10 nil_A = 3 isPal_A(x1) = x1 + 10 n__nil_A = 3 n__a_A = 3 n__e_A = 3 n__i_A = 3 n__o_A = 0 n__u_A = 3 a_A = 3 e_A = 3 i_A = 3 o_A = 1 u_A = 3 precedence: nil = n__nil = n__e = n__i = e = i > n__a = a > n____ = __ > n__isList = isList > activate = tt = isNeList = isNePal = isQid = and = isPal = o > n__o > n__isNeList > isList# > n__u = u > activate# = isNeList# = and# = n__isPal partial status: pi(activate#) = [1] pi(n__isNeList) = [1] pi(isNeList#) = [1] pi(n__isList) = [1] pi(isList#) = [1] pi(n____) = [1, 2] pi(and#) = [2] pi(isList) = [1] pi(activate) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isNePal) = [] pi(isQid) = [] pi(__) = [1, 2] pi(and) = [2] pi(n__isPal) = [] 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__isNeList(X)) -> isNeList#(X) p2: isNeList#(V) -> activate#(V) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: isNeList#(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,__(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)) -> __(X1,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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> activate#(V2) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p7: isNeList#(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = max{7, x1} n__isNeList_A(x1) = max{2, x1} isNeList#_A(x1) = max{7, x1} n_____A(x1,x2) = max{19, x1 + 14, x2} n__isList_A(x1) = max{6, x1} isList#_A(x1) = x1 and#_A(x1,x2) = max{x1 + 7, x2} isList_A(x1) = max{6, x1} activate_A(x1) = max{4, x1} tt_A = 1 isNeList_A(x1) = max{2, x1} isNePal_A(x1) = x1 + 9 isQid_A(x1) = max{2, x1 - 9} ___A(x1,x2) = max{19, x1 + 14, x2} and_A(x1,x2) = max{5, x1 + 4, x2} n__isPal_A(x1) = x1 + 14 nil_A = 3 isPal_A(x1) = x1 + 14 n__nil_A = 2 n__a_A = 0 n__e_A = 0 n__i_A = 2 n__o_A = 2 n__u_A = 2 a_A = 0 e_A = 1 i_A = 3 o_A = 3 u_A = 3 precedence: a > u > n____ = __ = n__a > n__isList = isList > isList# = and# > isNePal = and = n__isPal = isPal > activate# = n__isNeList = isNeList# = isNeList = isQid > activate = nil = e > n__nil > n__u > n__o > tt > n__e = n__i > i > o partial status: pi(activate#) = [1] pi(n__isNeList) = [1] pi(isNeList#) = [1] pi(n____) = [1, 2] pi(n__isList) = [1] pi(isList#) = [1] pi(and#) = [2] pi(isList) = [1] pi(activate) = [1] pi(tt) = [] pi(isNeList) = [1] pi(isNePal) = [1] pi(isQid) = [] pi(__) = [1, 2] pi(and) = [1, 2] pi(n__isPal) = [] 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: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: activate#(n__isList(X)) -> isList#(X) p3: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p4: and#(tt(),X) -> activate#(X) p5: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p6: isNeList#(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,__(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)) -> __(X1,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} -- 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: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p5: and#(tt(),X) -> activate#(X) p6: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 + 3 n__isNeList_A(x1) = x1 + 37 isNeList#_A(x1) = x1 + 40 n__isList_A(x1) = max{47, x1 + 37} isList#_A(x1) = x1 + 40 n_____A(x1,x2) = max{x1 + 36, x2} and#_A(x1,x2) = max{x1 - 54, x2 + 3} isList_A(x1) = max{47, x1 + 37} activate_A(x1) = max{10, x1} tt_A = 57 isNeList_A(x1) = x1 + 37 isNePal_A(x1) = x1 + 13 isQid_A(x1) = max{6, x1 - 4} ___A(x1,x2) = max{x1 + 36, x2} and_A(x1,x2) = max{6, x1 - 47, x2} n__isPal_A(x1) = x1 + 24 nil_A = 58 isPal_A(x1) = x1 + 24 n__nil_A = 58 n__a_A = 62 n__e_A = 61 n__i_A = 62 n__o_A = 62 n__u_A = 62 a_A = 62 e_A = 61 i_A = 62 o_A = 62 u_A = 62 precedence: activate# = isNeList# = n__isList = isList# = and# = isList = activate = isNeList = isNePal = __ = and = n__e = a = e = u > n__isNeList = nil = n__nil > isQid = n__isPal = isPal > tt > n____ > n__u > n__o = o > i > n__i > n__a partial status: pi(activate#) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n__isList) = [] pi(isList#) = [] pi(n____) = [] pi(and#) = [] pi(isList) = [] pi(activate) = [] pi(tt) = [] pi(isNeList) = [] pi(isNePal) = [] pi(isQid) = [] pi(__) = [] pi(and) = [] pi(n__isPal) = [] 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: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: activate#(n__isList(X)) -> isList#(X) p3: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) p4: and#(tt(),X) -> activate#(X) p5: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(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,__(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)) -> __(X1,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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__isNeList(X)) -> isNeList#(X) p2: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p3: and#(tt(),X) -> activate#(X) p4: activate#(n__isList(X)) -> isList#(X) p5: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: activate#_A(x1) = x1 n__isNeList_A(x1) = 13 isNeList#_A(x1) = 12 n_____A(x1,x2) = max{x1 + 36, x2} and#_A(x1,x2) = max{1, x1 - 12, x2} isNeList_A(x1) = 13 activate_A(x1) = max{13, x1} n__isList_A(x1) = 9 tt_A = 13 isList#_A(x1) = 9 isList_A(x1) = 13 isNePal_A(x1) = max{13, x1 + 8} isQid_A(x1) = 13 ___A(x1,x2) = max{x1 + 36, x2} and_A(x1,x2) = max{12, x1, x2} n__isPal_A(x1) = x1 + 22 nil_A = 12 isPal_A(x1) = x1 + 22 n__nil_A = 11 n__a_A = 12 n__e_A = 14 n__i_A = 10 n__o_A = 14 n__u_A = 14 a_A = 13 e_A = 14 i_A = 13 o_A = 14 u_A = 14 precedence: n__isNeList = n____ = isNeList = activate = n__isList = isList = isNePal = isQid = __ = and = isPal = n__o = e = o > n__e > isNeList# = nil = n__i > n__u = u > a > activate# = and# = tt = isList# = n__isPal = n__nil = n__a = i partial status: pi(activate#) = [] pi(n__isNeList) = [] pi(isNeList#) = [] pi(n____) = [] pi(and#) = [] pi(isNeList) = [] pi(activate) = [] pi(n__isList) = [] pi(tt) = [] pi(isList#) = [] pi(isList) = [] pi(isNePal) = [] pi(isQid) = [] pi(__) = [] pi(and) = [] pi(n__isPal) = [] 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: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) p2: and#(tt(),X) -> activate#(X) p3: activate#(n__isList(X)) -> isList#(X) p4: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: {p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: and#(tt(),X) -> activate#(X) p2: activate#(n__isList(X)) -> isList#(X) p3: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: and#_A(x1,x2) = max{x1, x2} tt_A = 3 activate#_A(x1) = max{3, x1} n__isList_A(x1) = max{2, x1} isList#_A(x1) = max{1, x1} n_____A(x1,x2) = max{12, x1 + 5, x2} isList_A(x1) = max{2, x1} activate_A(x1) = x1 isNePal_A(x1) = max{1, x1 - 6} isQid_A(x1) = max{0, x1 - 6} ___A(x1,x2) = max{12, x1 + 5, x2} and_A(x1,x2) = x2 n__isPal_A(x1) = max{4, x1 - 2} n__a_A = 10 n__e_A = 9 n__i_A = 10 n__o_A = 9 n__u_A = 10 nil_A = 4 isNeList_A(x1) = max{1, x1} n__isNeList_A(x1) = max{1, x1} isPal_A(x1) = max{4, x1 - 2} n__nil_A = 4 a_A = 10 e_A = 9 i_A = 10 o_A = 9 u_A = 10 precedence: n____ = __ > isNePal > n__isPal = n__e = isPal = e > and > n__isList = isList > activate = o > and# > isList# > tt = isQid = n__o = isNeList > n__isNeList > activate# = nil = n__nil > n__a = a > n__u = i = u > n__i partial status: pi(and#) = [1, 2] pi(tt) = [] pi(activate#) = [1] pi(n__isList) = [1] pi(isList#) = [1] pi(n____) = [1, 2] pi(isList) = [1] pi(activate) = [1] pi(isNePal) = [] pi(isQid) = [] pi(__) = [1, 2] pi(and) = [2] pi(n__isPal) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(nil) = [] pi(isNeList) = [1] pi(n__isNeList) = [1] pi(isPal) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: and#(tt(),X) -> activate#(X) p2: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(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,__(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)) -> __(X1,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: (no SCCs) -- 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,__(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)) -> __(X1,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: max/plus interpretations on natural numbers: __#_A(x1,x2) = max{0, x1 - 5} ___A(x1,x2) = max{6, x1 + 4, x2} nil_A = 0 n_____A(x1,x2) = max{x1 + 1, x2} precedence: __# = __ = nil = n____ partial status: pi(__#) = [] pi(__) = [1, 2] pi(nil) = [] pi(n____) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(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,__(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)) -> __(X1,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) -> __#(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,__(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)) -> __(X1,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 (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: __#_A(x1,x2) = max{x1 + 1, x2 + 1} ___A(x1,x2) = x2 precedence: __# = __ partial status: pi(__#) = [1] pi(__) = [2] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.