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