YES We show the termination of the TRS R: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt(),P) -> U72(isPal(activate(P))) U72(tt()) -> tt() U81(tt()) -> tt() isList(V) -> U11(isNeList(activate(V))) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) isPal(V) -> U81(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) 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__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: U21#(tt(),V2) -> U22#(isList(activate(V2))) p4: U21#(tt(),V2) -> isList#(activate(V2)) p5: U21#(tt(),V2) -> activate#(V2) p6: U41#(tt(),V2) -> U42#(isNeList(activate(V2))) p7: U41#(tt(),V2) -> isNeList#(activate(V2)) p8: U41#(tt(),V2) -> activate#(V2) p9: U51#(tt(),V2) -> U52#(isList(activate(V2))) p10: U51#(tt(),V2) -> isList#(activate(V2)) p11: U51#(tt(),V2) -> activate#(V2) p12: U71#(tt(),P) -> U72#(isPal(activate(P))) p13: U71#(tt(),P) -> isPal#(activate(P)) p14: U71#(tt(),P) -> activate#(P) p15: isList#(V) -> U11#(isNeList(activate(V))) p16: isList#(V) -> isNeList#(activate(V)) p17: isList#(V) -> activate#(V) p18: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p19: isList#(n____(V1,V2)) -> isList#(activate(V1)) p20: isList#(n____(V1,V2)) -> activate#(V1) p21: isList#(n____(V1,V2)) -> activate#(V2) p22: isNeList#(V) -> U31#(isQid(activate(V))) p23: isNeList#(V) -> isQid#(activate(V)) p24: isNeList#(V) -> activate#(V) p25: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p26: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p27: isNeList#(n____(V1,V2)) -> activate#(V1) p28: isNeList#(n____(V1,V2)) -> activate#(V2) p29: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p30: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p31: isNeList#(n____(V1,V2)) -> activate#(V1) p32: isNeList#(n____(V1,V2)) -> activate#(V2) p33: isNePal#(V) -> U61#(isQid(activate(V))) p34: isNePal#(V) -> isQid#(activate(V)) p35: isNePal#(V) -> activate#(V) p36: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) p37: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I)) p38: isNePal#(n____(I,n____(P,I))) -> activate#(I) p39: isNePal#(n____(I,n____(P,I))) -> activate#(P) p40: isPal#(V) -> U81#(isNePal(activate(V))) p41: isPal#(V) -> isNePal#(activate(V)) p42: isPal#(V) -> activate#(V) p43: activate#(n__nil()) -> nil#() p44: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2)) p45: activate#(n____(X1,X2)) -> activate#(X1) p46: activate#(n____(X1,X2)) -> activate#(X2) p47: activate#(n__a()) -> a#() p48: activate#(n__e()) -> e#() p49: activate#(n__i()) -> i#() p50: activate#(n__o()) -> o#() p51: activate#(n__u()) -> u#() and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The estimated dependency graph contains the following SCCs: {p13, p36, p41} {p4, p7, p10, p16, p18, p19, p25, p26, p29, p30} {p45, p46} {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(V) -> isNePal#(activate(V)) p2: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) p3: U71#(tt(),P) -> isPal#(activate(P)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isPal#_A(x1) = max{14, x1 + 13} isNePal#_A(x1) = x1 + 8 activate_A(x1) = max{4, x1 + 3} n_____A(x1,x2) = max{15, x1 + 14, x2} U71#_A(x1,x2) = max{x1 - 24, x2 + 17} isQid_A(x1) = x1 + 19 tt_A = 41 ___A(x1,x2) = max{16, x1 + 14, x2} nil_A = 5 n__nil_A = 3 a_A = 24 n__a_A = 23 e_A = 24 n__e_A = 23 i_A = 23 n__i_A = 23 o_A = 24 n__o_A = 23 u_A = 42 n__u_A = 42 precedence: U71# = isQid = nil = a > n__a > n__e = i > activate = e = n__i = o > __ > isNePal# = n____ = n__o = u > n__u > isPal# = tt = n__nil partial status: pi(isPal#) = [1] pi(isNePal#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(U71#) = [2] pi(isQid) = [1] pi(tt) = [] pi(__) = [1, 2] pi(nil) = [] 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: max/plus interpretations on natural numbers: isPal#_A(x1) = x1 + 20 isNePal#_A(x1) = x1 + 10 activate_A(x1) = max{8, x1 - 19} n_____A(x1,x2) = max{x1 - 14, x2 + 13} U71#_A(x1,x2) = x2 + 28 isQid_A(x1) = max{64, x1 + 56} tt_A = 65 ___A(x1,x2) = max{x1 + 34, x2 + 33} nil_A = 9 n__nil_A = 29 a_A = 9 n__a_A = 29 e_A = 9 n__e_A = 29 i_A = 9 n__i_A = 29 o_A = 9 n__o_A = 29 u_A = 9 n__u_A = 29 precedence: isPal# = isNePal# = activate = n____ = U71# = isQid = tt = __ = nil = n__nil = a = n__a = e = n__e = i = n__i = o = n__o = u = n__u partial status: pi(isPal#) = [] pi(isNePal#) = [1] pi(activate) = [] pi(n____) = [2] pi(U71#) = [2] pi(isQid) = [] pi(tt) = [] pi(__) = [] pi(nil) = [] 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 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(n____(V1,V2)) -> isList#(activate(V1)) p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p5: U21#(tt(),V2) -> isList#(activate(V2)) p6: isList#(V) -> isNeList#(activate(V)) p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p8: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p9: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p10: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = max{39, x1 - 23} n_____A(x1,x2) = max{122, x1 + 113, x2} U51#_A(x1,x2) = max{38, x1 - 62, x2 - 23} isNeList_A(x1) = x1 + 124 activate_A(x1) = max{8, x1} tt_A = 103 isList#_A(x1) = max{40, x1 - 23} U21#_A(x1,x2) = max{9, x1 - 62, x2 - 23} isList_A(x1) = x1 + 133 U41#_A(x1,x2) = max{39, x2 - 23} U22_A(x1) = max{104, x1 - 37} U42_A(x1) = 190 U52_A(x1) = max{111, x1 - 19} ___A(x1,x2) = max{122, x1 + 113, x2} nil_A = 1 U11_A(x1) = 133 U21_A(x1,x2) = max{x1 - 96, x2 + 104} U31_A(x1) = max{104, x1 + 2} U41_A(x1,x2) = max{123, x1 + 87, x2 - 9} U51_A(x1,x2) = max{x1 - 94, x2 + 123} isQid_A(x1) = max{99, x1 + 98} n__a_A = 6 n__e_A = 6 n__i_A = 9 n__o_A = 6 n__u_A = 6 n__nil_A = 0 a_A = 7 e_A = 7 i_A = 9 o_A = 7 u_A = 7 precedence: isList > n__e > activate = nil = a = e = i > u > __ > n____ > n__i > n__a > U52 > isNeList = U11 = U31 > U41 > U42 = U51 > U22 = U21 = n__nil = o > n__o > isQid > isNeList# = U51# = tt = isList# = U21# = U41# = n__u partial status: pi(isNeList#) = [] pi(n____) = [2] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [1] pi(tt) = [] pi(isList#) = [] pi(U21#) = [] pi(isList) = [1] pi(U41#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [2] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(isQid) = [1] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = 4 n_____A(x1,x2) = max{27, x2 + 19} U51#_A(x1,x2) = 4 isNeList_A(x1) = x1 + 49 activate_A(x1) = 72 tt_A = 80 isList#_A(x1) = 4 U21#_A(x1,x2) = 4 isList_A(x1) = x1 + 119 U41#_A(x1,x2) = 4 U22_A(x1) = 145 U42_A(x1) = 81 U52_A(x1) = 81 ___A(x1,x2) = max{24, x2} nil_A = 71 U11_A(x1) = 81 U21_A(x1,x2) = max{145, x2 + 74} U31_A(x1) = 81 U41_A(x1,x2) = 71 U51_A(x1,x2) = 67 isQid_A(x1) = max{48, x1 + 11} n__a_A = 70 n__e_A = 70 n__i_A = 70 n__o_A = 70 n__u_A = 71 n__nil_A = 71 a_A = 71 e_A = 69 i_A = 70 o_A = 71 u_A = 72 precedence: o > activate > __ > u > isNeList > n__e > n____ = U51 > U52 > U42 > nil = U41 > n__o = a > isNeList# = U51# = isList# = U21# = U41# = n__a = n__i = n__u = n__nil = e = i > isList > U21 > tt = U22 = U11 = U31 = isQid partial status: pi(isNeList#) = [] pi(n____) = [2] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [] pi(tt) = [] pi(isList#) = [] pi(U21#) = [] pi(isList) = [] pi(U41#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(n____(V1,V2)) -> isList#(activate(V1)) p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p5: U21#(tt(),V2) -> isList#(activate(V2)) p6: isList#(V) -> isNeList#(activate(V)) p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p8: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p9: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(V) -> isNeList#(activate(V)) p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p5: U41#(tt(),V2) -> isNeList#(activate(V2)) p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p7: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p8: U21#(tt(),V2) -> isList#(activate(V2)) p9: 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: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = x1 + 61 n_____A(x1,x2) = max{41, x1 + 21, x2} U51#_A(x1,x2) = max{79, x1 + 42, x2 + 61} isNeList_A(x1) = x1 + 40 activate_A(x1) = max{4, x1} tt_A = 36 isList#_A(x1) = max{79, x1 + 61} U41#_A(x1,x2) = max{x1 + 29, x2 + 61} isList_A(x1) = x1 + 45 U21#_A(x1,x2) = max{79, x2 + 61} U22_A(x1) = 37 U42_A(x1) = 40 U52_A(x1) = 36 ___A(x1,x2) = max{41, x1 + 21, x2} nil_A = 37 U11_A(x1) = max{37, x1 + 1} U21_A(x1,x2) = max{38, x1} U31_A(x1) = max{9, x1 + 1} U41_A(x1,x2) = max{x1 - 12, x2 + 40} U51_A(x1,x2) = max{40, x2 - 5} isQid_A(x1) = max{35, x1 + 34} n__a_A = 37 n__e_A = 3 n__i_A = 37 n__o_A = 37 n__u_A = 37 n__nil_A = 37 a_A = 37 e_A = 4 i_A = 37 o_A = 37 u_A = 37 precedence: isNeList > U22 = U31 = isQid > n__i = i > n__u = u > activate = U52 = e > __ > n____ > isNeList# = U51# = isList# = U41# = U21# = U41 = U51 = n__a = a = o > U42 = n__e > isList > U21 > nil > n__o = n__nil > tt = U11 partial status: pi(isNeList#) = [] pi(n____) = [1, 2] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [1] pi(tt) = [] pi(isList#) = [] pi(U41#) = [] pi(isList) = [1] pi(U21#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [1] pi(U31) = [1] pi(U41) = [] pi(U51) = [] pi(isQid) = [1] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = 29 n_____A(x1,x2) = max{79, x1 + 33, x2} U51#_A(x1,x2) = 29 isNeList_A(x1) = x1 + 17 activate_A(x1) = max{30, x1 + 17} tt_A = 98 isList#_A(x1) = 29 U41#_A(x1,x2) = 29 isList_A(x1) = x1 + 109 U21#_A(x1,x2) = 29 U22_A(x1) = 114 U42_A(x1) = 9 U52_A(x1) = 139 ___A(x1,x2) = max{96, x1 + 33, x2} nil_A = 31 U11_A(x1) = 99 U21_A(x1,x2) = max{97, x1 + 16} U31_A(x1) = max{12, x1 + 1} U41_A(x1,x2) = 10 U51_A(x1,x2) = 11 isQid_A(x1) = max{12, x1 - 15} n__a_A = 114 n__e_A = 114 n__i_A = 114 n__o_A = 114 n__u_A = 114 n__nil_A = 30 a_A = 115 e_A = 115 i_A = 115 o_A = 115 u_A = 115 precedence: n__nil = a = e = i = o = u > isNeList = activate = n__u > isNeList# = U51# = isList# = U41# = isList = U21# = U42 = U52 = __ > n____ > U22 = nil = U11 = U21 > tt > U31 = U41 = U51 = isQid = n__a = n__e = n__i = n__o partial status: pi(isNeList#) = [] pi(n____) = [] pi(U51#) = [] pi(isNeList) = [] pi(activate) = [1] pi(tt) = [] pi(isList#) = [] pi(U41#) = [] pi(isList) = [] pi(U21#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [1] pi(U41) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(V) -> isNeList#(activate(V)) p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p5: U41#(tt(),V2) -> isNeList#(activate(V2)) p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p7: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p8: U21#(tt(),V2) -> isList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p4: U21#(tt(),V2) -> isList#(activate(V2)) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p7: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p8: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = max{0, x1 - 14} n_____A(x1,x2) = max{64, x1 + 32, x2} U51#_A(x1,x2) = max{49, x1 - 76, x2 - 14} isNeList_A(x1) = max{61, x1 + 21} activate_A(x1) = max{3, x1} tt_A = 0 isList#_A(x1) = max{0, x1 - 14} U21#_A(x1,x2) = max{50, x1 - 36, x2 - 14} isList_A(x1) = x1 + 18 U41#_A(x1,x2) = max{0, x1 - 4, x2 - 14} U22_A(x1) = max{51, x1 - 26} U42_A(x1) = 3 U52_A(x1) = max{6, x1 + 1} ___A(x1,x2) = max{64, x1 + 32, x2} nil_A = 2 U11_A(x1) = max{1, x1 - 43} U21_A(x1,x2) = max{51, x2 - 4} U31_A(x1) = 0 U41_A(x1,x2) = x1 + 35 U51_A(x1,x2) = max{33, x1 + 7, x2 + 21} isQid_A(x1) = max{62, x1 + 1} n__a_A = 1 n__e_A = 1 n__i_A = 1 n__o_A = 4 n__u_A = 1 n__nil_A = 1 a_A = 2 e_A = 2 i_A = 2 o_A = 4 u_A = 2 precedence: a > i > n__a > activate > __ > nil = isQid = n__e = u > isList > n__u > U11 = U21 = n__nil > U52 > isNeList > o > U22 > U42 = U41 = e > n__i > isNeList# = n____ = U51# = tt = isList# = U21# = U41# = U31 = U51 = n__o partial status: pi(isNeList#) = [] pi(n____) = [2] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [1] pi(tt) = [] pi(isList#) = [] pi(U21#) = [] pi(isList) = [1] pi(U41#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [1] pi(U51) = [1, 2] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = 12 n_____A(x1,x2) = 0 U51#_A(x1,x2) = 12 isNeList_A(x1) = x1 + 26 activate_A(x1) = 2 tt_A = 10 isList#_A(x1) = 12 U21#_A(x1,x2) = 12 isList_A(x1) = x1 + 2 U41#_A(x1,x2) = 12 U22_A(x1) = 1 U42_A(x1) = 22 U52_A(x1) = 18 ___A(x1,x2) = 0 nil_A = 3 U11_A(x1) = 3 U21_A(x1,x2) = 0 U31_A(x1) = 11 U41_A(x1,x2) = x1 + 21 U51_A(x1,x2) = x2 + 23 isQid_A(x1) = 27 n__a_A = 4 n__e_A = 9 n__i_A = 4 n__o_A = 4 n__u_A = 3 n__nil_A = 4 a_A = 3 e_A = 3 i_A = 3 o_A = 3 u_A = 3 precedence: U22 = U52 > isNeList# = U51# = isList# = U21# = U41# = U31 > activate > __ > n____ > isNeList = tt = isList = U42 = nil = U11 = U21 = U41 = U51 = isQid = n__a = n__e = n__i = n__o = n__u = n__nil = a = e = i = o = u partial status: pi(isNeList#) = [] pi(n____) = [] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [] pi(tt) = [] pi(isList#) = [] pi(U21#) = [] pi(isList) = [1] pi(U41#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [2] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p4: U21#(tt(),V2) -> isList#(activate(V2)) p5: isList#(V) -> isNeList#(activate(V)) p6: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p7: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(V) -> isNeList#(activate(V)) p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p5: U41#(tt(),V2) -> isNeList#(activate(V2)) p6: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p7: U21#(tt(),V2) -> isList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = ((0,1),(0,1)) x1 + (6,5) n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (18,5) U51#_A(x1,x2) = ((0,1),(0,1)) x2 + (10,5) isNeList_A(x1) = x1 + (10,5) activate_A(x1) = ((1,1),(0,1)) x1 + (5,0) tt_A() = (8,4) isList#_A(x1) = ((0,1),(0,1)) x1 + (7,5) U41#_A(x1,x2) = ((0,0),(0,1)) x1 + ((0,1),(0,1)) x2 + (6,1) isList_A(x1) = ((0,1),(0,0)) x1 + (13,6) U21#_A(x1,x2) = ((0,1),(0,1)) x2 + (8,5) U22_A(x1) = ((0,1),(0,0)) x1 + (5,5) U42_A(x1) = (9,4) U52_A(x1) = (8,4) ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (18,5) nil_A() = (10,4) U11_A(x1) = (8,4) U21_A(x1,x2) = ((1,0),(0,0)) x1 + (4,5) U31_A(x1) = (9,4) U41_A(x1,x2) = (16,5) U51_A(x1,x2) = (9,6) isQid_A(x1) = ((0,1),(1,0)) x1 + (0,4) n__a_A() = (0,9) n__e_A() = (9,9) n__i_A() = (9,9) n__o_A() = (9,9) n__u_A() = (1,9) n__nil_A() = (1,4) a_A() = (0,9) e_A() = (9,9) i_A() = (9,9) o_A() = (9,9) u_A() = (1,9) precedence: n__a = a > n__u = u > activate > n__o = o > isNeList = U51 > e > isList > U11 > U31 > U51# > isQid > U21 > U21# > U22 = U52 > tt > nil = n__nil > __ > n____ > isList# > isNeList# = U41# > n__e > i > n__i > U42 = U41 partial status: pi(isNeList#) = [] pi(n____) = [2] pi(U51#) = [] pi(isNeList) = [1] pi(activate) = [1] pi(tt) = [] pi(isList#) = [] pi(U41#) = [] pi(isList) = [] pi(U21#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = (5,4) n_____A(x1,x2) = ((1,1),(1,0)) x2 + (9,4) U51#_A(x1,x2) = (4,2) isNeList_A(x1) = ((1,0),(0,0)) x1 + (1,3) activate_A(x1) = ((0,0),(1,0)) x1 + (3,2) tt_A() = (6,3) isList#_A(x1) = (4,2) U41#_A(x1,x2) = (5,4) isList_A(x1) = (8,3) U21#_A(x1,x2) = (4,2) U22_A(x1) = (7,3) U42_A(x1) = (9,3) U52_A(x1) = (0,0) ___A(x1,x2) = ((1,1),(0,0)) x1 + (5,5) nil_A() = (2,3) U11_A(x1) = (7,3) U21_A(x1,x2) = (7,3) U31_A(x1) = (7,4) U41_A(x1,x2) = (9,3) U51_A(x1,x2) = (0,0) isQid_A(x1) = (7,4) n__a_A() = (0,1) n__e_A() = (0,1) n__i_A() = (0,0) n__o_A() = (0,1) n__u_A() = (1,1) n__nil_A() = (1,1) a_A() = (1,1) e_A() = (4,3) i_A() = (1,0) o_A() = (3,2) u_A() = (2,2) precedence: n__e > e > activate > i > n__i > n__nil > U11 > a > isNeList > U31 > tt = n__a = n__o = n__u = o = u > nil > U41 > isList > isQid > isNeList# = U41# = U21 > U51# > n____ = isList# = U21# = U22 = U42 = U52 = __ = U51 partial status: pi(isNeList#) = [] pi(n____) = [] pi(U51#) = [] pi(isNeList) = [] pi(activate) = [] pi(tt) = [] pi(isList#) = [] pi(U41#) = [] pi(isList) = [] pi(U21#) = [] pi(U22) = [] pi(U42) = [] pi(U52) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p1, p2, p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p2: U41#(tt(),V2) -> isNeList#(activate(V2)) p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p4: U21#(tt(),V2) -> isList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2} {p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p2: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = x1 n_____A(x1,x2) = x1 + x2 + (9,0) U41#_A(x1,x2) = x2 + (1,0) isList_A(x1) = ((1,1),(0,1)) x1 + (5,16) activate_A(x1) = x1 tt_A() = (6,5) U42_A(x1) = (7,6) U52_A(x1) = (7,6) U22_A(x1) = (7,6) U31_A(x1) = ((0,1),(0,0)) x1 + (2,5) U41_A(x1,x2) = (8,6) isNeList_A(x1) = ((1,0),(1,1)) x1 + (3,6) U51_A(x1,x2) = ((0,0),(0,1)) x1 + (8,1) isQid_A(x1) = ((1,0),(1,0)) x1 + (4,0) n__a_A() = (5,1) n__e_A() = (5,1) n__i_A() = (5,0) n__o_A() = (5,0) n__u_A() = (5,0) ___A(x1,x2) = x1 + x2 + (9,0) nil_A() = (1,1) U11_A(x1) = ((1,0),(0,0)) x1 + (1,5) U21_A(x1,x2) = ((0,1),(0,0)) x2 + (10,6) n__nil_A() = (1,1) a_A() = (5,1) e_A() = (5,1) i_A() = (5,0) o_A() = (5,0) u_A() = (5,0) precedence: U41# > activate = isNeList = isQid = a = e = i = o = u > __ > n____ > U41 > U42 = n__a = n__i = n__u = nil > n__o > n__e > isNeList# = isList = tt = U52 = U22 = U31 = U51 = U11 = U21 = n__nil partial status: pi(isNeList#) = [] pi(n____) = [1] pi(U41#) = [2] pi(isList) = [] pi(activate) = [1] pi(tt) = [] pi(U42) = [] pi(U52) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(isNeList) = [1] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [1] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = (5,14) n_____A(x1,x2) = ((1,1),(1,0)) x1 + (1,2) U41#_A(x1,x2) = (1,2) isList_A(x1) = (4,14) activate_A(x1) = (6,6) tt_A() = (0,2) U42_A(x1) = (1,2) U52_A(x1) = (1,2) U22_A(x1) = (0,2) U31_A(x1) = (1,2) U41_A(x1,x2) = (2,3) isNeList_A(x1) = ((1,0),(1,1)) x1 + (2,2) U51_A(x1,x2) = (2,3) isQid_A(x1) = (1,2) n__a_A() = (0,1) n__e_A() = (0,0) n__i_A() = (0,0) n__o_A() = (0,1) n__u_A() = (0,2) ___A(x1,x2) = (2,3) nil_A() = (1,2) U11_A(x1) = (1,2) U21_A(x1,x2) = (7,2) n__nil_A() = (0,1) a_A() = (1,6) e_A() = (1,1) i_A() = (1,1) o_A() = (1,2) u_A() = (1,3) precedence: n__o = o > n__u = u > n__i = i > n__a = n__e = a = e > U11 > U22 > isQid > U42 > tt > n__nil > nil > U52 > isNeList# = activate = U41 = U51 > n____ > U21 > isList > U41# = U31 = isNeList = __ partial status: pi(isNeList#) = [] pi(n____) = [] pi(U41#) = [] pi(isList) = [] pi(activate) = [] pi(tt) = [] pi(U42) = [] pi(U52) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(isNeList) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] 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: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: 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: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p2: U21#(tt(),V2) -> isList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isList#_A(x1) = x1 n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (9,8) U21#_A(x1,x2) = x1 + x2 isList_A(x1) = ((1,1),(0,1)) x1 + (7,4) activate_A(x1) = x1 tt_A() = (2,2) U42_A(x1) = (3,3) U52_A(x1) = (7,3) U22_A(x1) = ((1,0),(0,0)) x1 + (1,3) U31_A(x1) = ((1,0),(0,0)) x1 + (1,2) U41_A(x1,x2) = ((1,0),(1,0)) x1 + (2,1) isNeList_A(x1) = ((1,1),(1,0)) x1 + (10,5) U51_A(x1,x2) = ((0,1),(0,0)) x1 + (6,3) isQid_A(x1) = ((0,1),(1,0)) x1 + (3,0) n__a_A() = (3,0) n__e_A() = (3,1) n__i_A() = (3,0) n__o_A() = (3,0) n__u_A() = (3,1) ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (9,8) nil_A() = (1,0) U11_A(x1) = ((0,1),(0,0)) x1 + (1,4) U21_A(x1,x2) = ((1,1),(0,0)) x2 + (9,3) n__nil_A() = (1,0) a_A() = (3,0) e_A() = (3,1) i_A() = (3,0) o_A() = (3,0) u_A() = (3,1) precedence: n__a = a > activate = nil = e > __ > isList = U11 > n__nil > U21 > u > isNeList > U51 > n____ > isList# = U21# > o > n__o > i > U41 = n__i > n__e > U42 = U52 = U22 = U31 > isQid > n__u > tt partial status: pi(isList#) = [1] pi(n____) = [1, 2] pi(U21#) = [1, 2] pi(isList) = [1] pi(activate) = [1] pi(tt) = [] pi(U42) = [] pi(U52) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(isNeList) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isList#_A(x1) = ((1,1),(0,1)) x1 n_____A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(1,1)) x2 + (4,2) U21#_A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (1,0) isList_A(x1) = ((1,1),(1,1)) x1 + (1,2) activate_A(x1) = (0,0) tt_A() = (4,5) U42_A(x1) = (5,6) U52_A(x1) = (0,0) U22_A(x1) = (0,0) U31_A(x1) = (5,5) U41_A(x1,x2) = (1,1) isNeList_A(x1) = (6,6) U51_A(x1,x2) = (1,0) isQid_A(x1) = (5,5) n__a_A() = (0,0) n__e_A() = (0,0) n__i_A() = (0,0) n__o_A() = (0,0) n__u_A() = (0,0) ___A(x1,x2) = (0,1) nil_A() = (2,2) U11_A(x1) = (5,5) U21_A(x1,x2) = (1,0) n__nil_A() = (1,1) a_A() = (0,0) e_A() = (0,0) i_A() = (0,0) o_A() = (0,0) u_A() = (0,0) precedence: activate = n__o = o > i > n__i = n__u = u > U42 > isNeList > U41 > U52 > U31 > U22 = nil > isList# = n____ = U21# = isList = tt = U51 = isQid = n__a = n__e = __ = U11 = U21 = n__nil = a = e partial status: pi(isList#) = [] pi(n____) = [] pi(U21#) = [1, 2] pi(isList) = [1] pi(activate) = [] pi(tt) = [] pi(U42) = [] pi(U52) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(isNeList) = [] pi(U51) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] 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: 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: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: 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: __#(__(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: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r32 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.