YES We show the termination of the TRS R: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt(),V) -> U12(isNeList(activate(V))) U12(tt()) -> tt() U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) U22(tt(),V2) -> U23(isList(activate(V2))) U23(tt()) -> tt() U31(tt(),V) -> U32(isQid(activate(V))) U32(tt()) -> tt() U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isNeList(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isList(activate(V2))) U53(tt()) -> tt() U61(tt(),V) -> U62(isQid(activate(V))) U62(tt()) -> tt() U71(tt(),V) -> U72(isNePal(activate(V))) U72(tt()) -> tt() and(tt(),X) -> activate(X) isList(V) -> U11(isPalListKind(activate(V)),activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) isPal(n__nil()) -> tt() isPalListKind(n__a()) -> tt() isPalListKind(n__e()) -> tt() isPalListKind(n__i()) -> tt() isPalListKind(n__nil()) -> tt() isPalListKind(n__o()) -> tt() isPalListKind(n__u()) -> tt() isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) 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) isPalListKind(X) -> n__isPalListKind(X) and(X1,X2) -> n__and(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)) -> __(X1,X2) activate(n__isPalListKind(X)) -> isPalListKind(X) activate(n__and(X1,X2)) -> and(X1,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: U11#(tt(),V) -> U12#(isNeList(activate(V))) p4: U11#(tt(),V) -> isNeList#(activate(V)) p5: U11#(tt(),V) -> activate#(V) p6: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p7: U21#(tt(),V1,V2) -> isList#(activate(V1)) p8: U21#(tt(),V1,V2) -> activate#(V1) p9: U21#(tt(),V1,V2) -> activate#(V2) p10: U22#(tt(),V2) -> U23#(isList(activate(V2))) p11: U22#(tt(),V2) -> isList#(activate(V2)) p12: U22#(tt(),V2) -> activate#(V2) p13: U31#(tt(),V) -> U32#(isQid(activate(V))) p14: U31#(tt(),V) -> isQid#(activate(V)) p15: U31#(tt(),V) -> activate#(V) p16: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p17: U41#(tt(),V1,V2) -> isList#(activate(V1)) p18: U41#(tt(),V1,V2) -> activate#(V1) p19: U41#(tt(),V1,V2) -> activate#(V2) p20: U42#(tt(),V2) -> U43#(isNeList(activate(V2))) p21: U42#(tt(),V2) -> isNeList#(activate(V2)) p22: U42#(tt(),V2) -> activate#(V2) p23: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p24: U51#(tt(),V1,V2) -> isNeList#(activate(V1)) p25: U51#(tt(),V1,V2) -> activate#(V1) p26: U51#(tt(),V1,V2) -> activate#(V2) p27: U52#(tt(),V2) -> U53#(isList(activate(V2))) p28: U52#(tt(),V2) -> isList#(activate(V2)) p29: U52#(tt(),V2) -> activate#(V2) p30: U61#(tt(),V) -> U62#(isQid(activate(V))) p31: U61#(tt(),V) -> isQid#(activate(V)) p32: U61#(tt(),V) -> activate#(V) p33: U71#(tt(),V) -> U72#(isNePal(activate(V))) p34: U71#(tt(),V) -> isNePal#(activate(V)) p35: U71#(tt(),V) -> activate#(V) p36: and#(tt(),X) -> activate#(X) p37: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p38: isList#(V) -> isPalListKind#(activate(V)) p39: isList#(V) -> activate#(V) p40: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p41: isList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) p42: isList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p43: isList#(n____(V1,V2)) -> activate#(V1) p44: isList#(n____(V1,V2)) -> activate#(V2) p45: isNeList#(V) -> U31#(isPalListKind(activate(V)),activate(V)) p46: isNeList#(V) -> isPalListKind#(activate(V)) p47: isNeList#(V) -> activate#(V) p48: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p49: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) p50: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p51: isNeList#(n____(V1,V2)) -> activate#(V1) p52: isNeList#(n____(V1,V2)) -> activate#(V2) p53: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p54: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) p55: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p56: isNeList#(n____(V1,V2)) -> activate#(V1) p57: isNeList#(n____(V1,V2)) -> activate#(V2) p58: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V)) p59: isNePal#(V) -> isPalListKind#(activate(V)) p60: isNePal#(V) -> activate#(V) p61: isNePal#(n____(I,__(P,I))) -> and#(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) p62: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPalListKind(activate(I))) p63: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) p64: isNePal#(n____(I,__(P,I))) -> activate#(I) p65: isNePal#(n____(I,__(P,I))) -> isPal#(activate(P)) p66: isNePal#(n____(I,__(P,I))) -> activate#(P) p67: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V)) p68: isPal#(V) -> isPalListKind#(activate(V)) p69: isPal#(V) -> activate#(V) p70: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) p71: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p72: isPalListKind#(n____(V1,V2)) -> activate#(V1) p73: isPalListKind#(n____(V1,V2)) -> activate#(V2) p74: activate#(n__nil()) -> nil#() p75: activate#(n____(X1,X2)) -> __#(X1,X2) p76: activate#(n__isPalListKind(X)) -> isPalListKind#(X) p77: activate#(n__and(X1,X2)) -> and#(X1,X2) p78: activate#(n__a()) -> a#() p79: activate#(n__e()) -> e#() p80: activate#(n__i()) -> i#() p81: activate#(n__o()) -> o#() p82: 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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The estimated dependency graph contains the following SCCs: {p34, p65, p67} {p4, p6, p7, p11, p16, p17, p21, p23, p24, p28, p37, p40, p48, p53} {p36, p70, p71, p72, p73, p76, p77} {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNePal#(n____(I,__(P,I))) -> isPal#(activate(P)) p2: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V)) p3: U71#(tt(),V) -> isNePal#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The set of usable rules consists of r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isNePal#_A(x1) = max{16, x1 + 15} n_____A(x1,x2) = max{14, x1 + 11, x2} ___A(x1,x2) = max{14, x1 + 11, x2} isPal#_A(x1) = x1 + 22 activate_A(x1) = max{3, x1} U71#_A(x1,x2) = max{x1 + 9, x2 + 18} isPalListKind_A(x1) = x1 + 10 tt_A = 0 nil_A = 2 and_A(x1,x2) = max{3, x1 + 2, x2} n__nil_A = 1 n__and_A(x1,x2) = max{3, x1 + 2, x2} a_A = 2 n__a_A = 1 e_A = 2 n__e_A = 1 i_A = 2 n__i_A = 1 o_A = 1 n__o_A = 1 u_A = 2 n__u_A = 1 n__isPalListKind_A(x1) = x1 + 10 precedence: n__a > e = o = n__u > isPalListKind = n__isPalListKind > n____ = __ = and = n__and > activate > nil > n__nil > i > isPal# = n__o > isNePal# = U71# = tt > n__i = u > a = n__e partial status: pi(isNePal#) = [] pi(n____) = [1, 2] pi(__) = [1, 2] pi(isPal#) = [1] pi(activate) = [1] pi(U71#) = [1] pi(isPalListKind) = [1] pi(tt) = [] pi(nil) = [] pi(and) = [2] pi(n__nil) = [] pi(n__and) = [2] 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) = [] pi(n__isPalListKind) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: isNePal#_A(x1) = 241 n_____A(x1,x2) = max{x1 + 36, x2 + 120} ___A(x1,x2) = max{x1 + 36, x2 + 120} isPal#_A(x1) = max{241, x1 - 45} activate_A(x1) = max{50, x1 + 11} U71#_A(x1,x2) = 241 isPalListKind_A(x1) = max{49, x1 + 18} tt_A = 48 nil_A = 51 and_A(x1,x2) = max{53, x2 + 51} n__nil_A = 41 n__and_A(x1,x2) = max{43, x2 + 41} a_A = 51 n__a_A = 47 e_A = 46 n__e_A = 47 i_A = 51 n__i_A = 41 o_A = 51 n__o_A = 29 u_A = 51 n__u_A = 41 n__isPalListKind_A(x1) = max{37, x1 + 18} precedence: __ = isPal# = nil > isNePal# = activate = U71# = isPalListKind = and > n____ > tt = n__nil = n__and = a = n__a = e = n__e = i = n__i = o = n__o = u = n__u = n__isPalListKind partial status: pi(isNePal#) = [] pi(n____) = [] pi(__) = [1, 2] pi(isPal#) = [] pi(activate) = [1] pi(U71#) = [] pi(isPalListKind) = [1] pi(tt) = [] pi(nil) = [] pi(and) = [2] pi(n__nil) = [] pi(n__and) = [2] 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) = [] pi(n__isPalListKind) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V)) p2: U71#(tt(),V) -> isNePal#(activate(V)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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: U52#(tt(),V2) -> isList#(activate(V2)) p2: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p3: U21#(tt(),V1,V2) -> isList#(activate(V1)) p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p5: U11#(tt(),V) -> isNeList#(activate(V)) p6: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p7: U51#(tt(),V1,V2) -> isNeList#(activate(V1)) p8: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p9: U41#(tt(),V1,V2) -> isList#(activate(V1)) p10: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p11: U42#(tt(),V2) -> isNeList#(activate(V2)) p12: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p13: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p14: U22#(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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = max{x1 - 175, x2 + 29} tt_A = 176 isList#_A(x1) = x1 + 29 activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 308, x2} U21#_A(x1,x2,x3) = max{x2 + 309, x3 + 29} and_A(x1,x2) = max{419, x1 - 93, x2} isPalListKind_A(x1) = x1 + 368 n__isPalListKind_A(x1) = x1 + 368 U11#_A(x1,x2) = max{x1 - 367, x2 + 29} isNeList#_A(x1) = x1 + 29 U51#_A(x1,x2,x3) = max{x1 - 361, x2 + 58, x3 + 29} U41#_A(x1,x2,x3) = max{x1 - 420, x2 + 309, x3 + 29} U42#_A(x1,x2) = max{x1 - 156, x2 + 29} isList_A(x1) = max{184, x1 + 180} isNeList_A(x1) = max{201, x1 + 199} U22#_A(x1,x2) = max{x1 - 152, x2 + 29} U23_A(x1) = max{178, x1 - 184} U43_A(x1) = 177 U53_A(x1) = max{177, x1 + 1} U12_A(x1) = 177 U22_A(x1,x2) = max{178, x2 - 4} U32_A(x1) = max{4, x1 + 3} U42_A(x1,x2) = 178 U52_A(x1,x2) = max{x1 + 10, x2 + 186} isQid_A(x1) = max{2, x1 + 1} n__a_A = 177 n__e_A = 177 n__i_A = 177 n__o_A = 177 n__u_A = 177 ___A(x1,x2) = max{x1 + 308, x2} nil_A = 177 U11_A(x1,x2) = x2 + 177 U21_A(x1,x2,x3) = max{x2 + 178, x3 - 4} U31_A(x1,x2) = max{x1 - 170, x2 + 198} U41_A(x1,x2,x3) = max{x1 - 420, x2 + 179, x3} U51_A(x1,x2,x3) = max{x2 + 309, x3 + 198} n__nil_A = 177 a_A = 177 e_A = 177 i_A = 177 o_A = 177 u_A = 177 n__and_A(x1,x2) = max{419, x1 - 93, x2} precedence: isQid > n____ = __ = U41 > isPalListKind = n__isPalListKind > and = n__and > activate > o > n__o > nil > isNeList > U42 > U21 > U22 > U23 > U31 > i > n__i > U52# = isList# = U21# = U11# = isNeList# = U51# = U41# = U42# = U22# > U32 > U53 = U52 > n__nil > U43 = a > isList > U11 > u > n__u > e > n__a > U12 > tt > U51 > n__e partial status: pi(U52#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [1] pi(n____) = [1, 2] pi(U21#) = [] pi(and) = [2] pi(isPalListKind) = [1] pi(n__isPalListKind) = [1] pi(U11#) = [] pi(isNeList#) = [] pi(U51#) = [] pi(U41#) = [] pi(U42#) = [] pi(isList) = [] pi(isNeList) = [1] pi(U22#) = [] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [1, 2] pi(isQid) = [1] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [2] pi(U21) = [] pi(U31) = [2] pi(U41) = [] pi(U51) = [2, 3] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [2] 2. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = 112 tt_A = 35 isList#_A(x1) = 112 activate_A(x1) = 80 n_____A(x1,x2) = max{242, x2 + 91} U21#_A(x1,x2,x3) = 112 and_A(x1,x2) = 79 isPalListKind_A(x1) = x1 + 323 n__isPalListKind_A(x1) = 323 U11#_A(x1,x2) = 112 isNeList#_A(x1) = 112 U51#_A(x1,x2,x3) = 112 U41#_A(x1,x2,x3) = 112 U42#_A(x1,x2) = 112 isList_A(x1) = 38 isNeList_A(x1) = max{39, x1 - 77} U22#_A(x1,x2) = 112 U23_A(x1) = 36 U43_A(x1) = 36 U53_A(x1) = 36 U12_A(x1) = 36 U22_A(x1,x2) = 113 U32_A(x1) = 36 U42_A(x1,x2) = 36 U52_A(x1,x2) = 83 isQid_A(x1) = max{84, x1 - 2} n__a_A = 38 n__e_A = 38 n__i_A = 38 n__o_A = 38 n__u_A = 36 ___A(x1,x2) = max{x1 + 550, x2 + 527} nil_A = 79 U11_A(x1,x2) = 38 U21_A(x1,x2,x3) = 243 U31_A(x1,x2) = max{81, x2 + 37} U41_A(x1,x2,x3) = 37 U51_A(x1,x2,x3) = x2 + 84 n__nil_A = 0 a_A = 79 e_A = 79 i_A = 79 o_A = 79 u_A = 79 n__and_A(x1,x2) = 78 precedence: U23 > isQid > and > activate > U12 = n__a > isList = __ > U21 > U22 > n__i > n__and > i > U32 > n__u = u > U53 > tt = isPalListKind = n__isPalListKind > U42 > U52# = isList# = U21# = U11# = isNeList# = U51# = U41# = U42# = isNeList = U22# = U43 = U41 > U31 > n__o > o > a > U52 = n__e = nil = U11 = U51 = e > n__nil > n____ partial status: pi(U52#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [] pi(n____) = [2] pi(U21#) = [] pi(and) = [] pi(isPalListKind) = [1] pi(n__isPalListKind) = [] pi(U11#) = [] pi(isNeList#) = [] pi(U51#) = [] pi(U41#) = [] pi(U42#) = [] pi(isList) = [] pi(isNeList) = [] pi(U22#) = [] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [] 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(U31) = [2] pi(U41) = [] pi(U51) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [] 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: U52#(tt(),V2) -> isList#(activate(V2)) p2: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p3: U21#(tt(),V1,V2) -> isList#(activate(V1)) p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p5: U11#(tt(),V) -> isNeList#(activate(V)) p6: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p7: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p8: U41#(tt(),V1,V2) -> isList#(activate(V1)) p9: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p10: U42#(tt(),V2) -> isNeList#(activate(V2)) p11: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p12: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p13: U22#(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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U52#(tt(),V2) -> isList#(activate(V2)) p2: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p3: U11#(tt(),V) -> isNeList#(activate(V)) p4: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p5: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p6: U42#(tt(),V2) -> isNeList#(activate(V2)) p7: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p8: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p9: U41#(tt(),V1,V2) -> isList#(activate(V1)) p10: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p11: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p12: U22#(tt(),V2) -> isList#(activate(V2)) p13: U21#(tt(),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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = max{x1 + 71, x2 + 77} tt_A = 67 isList#_A(x1) = x1 + 77 activate_A(x1) = x1 U11#_A(x1,x2) = max{x1 + 28, x2 + 77} isPalListKind_A(x1) = x1 + 49 isNeList#_A(x1) = x1 + 77 n_____A(x1,x2) = max{54, x1 + 52, x2} U41#_A(x1,x2,x3) = max{x1 + 28, x2 + 129, x3 + 77} and_A(x1,x2) = max{23, x1 + 2, x2} n__isPalListKind_A(x1) = x1 + 49 U42#_A(x1,x2) = max{129, x1 + 54, x2 + 77} isList_A(x1) = x1 U51#_A(x1,x2,x3) = max{x1 - 1, x2 + 128, x3 + 77} isNeList_A(x1) = max{7, x1 - 6} U21#_A(x1,x2,x3) = max{79, x1 + 9, x2 + 78, x3 + 77} U22#_A(x1,x2) = max{79, x1 + 78, x2 + 77} U23_A(x1) = 98 U43_A(x1) = 68 U53_A(x1) = 68 U12_A(x1) = max{17, x1 + 4} U22_A(x1,x2) = x1 + 32 U32_A(x1) = x1 + 7 U42_A(x1,x2) = max{8, x1 + 1, x2 - 14} U52_A(x1,x2) = max{44, x1 + 6} isQid_A(x1) = max{0, x1 - 14} n__a_A = 82 n__e_A = 82 n__i_A = 82 n__o_A = 82 n__u_A = 82 ___A(x1,x2) = max{54, x1 + 52, x2} nil_A = 68 U11_A(x1,x2) = max{0, x1 - 49, x2 - 1} U21_A(x1,x2,x3) = x2 + 33 U31_A(x1,x2) = max{7, x2 - 6} U41_A(x1,x2,x3) = max{x1 - 58, x2 + 1, x3 - 7} U51_A(x1,x2,x3) = max{45, x2, x3 - 7} n__nil_A = 68 a_A = 82 e_A = 82 i_A = 82 o_A = 82 u_A = 82 n__and_A(x1,x2) = max{23, x1 + 2, x2} precedence: U12 > U53 > n____ = __ > isPalListKind = and = n__isPalListKind = U41 = n__and > U42 > U52 = U51 > U22 > U43 = nil = n__nil > activate = U23 = a > o > n__o > tt > U52# = isList# = U11# = isNeList# = U41# = U42# = U51# = U21# = U22# > n__a = e > isQid > i > u > n__u > n__i > isList = isNeList = U11 > U31 > U32 > n__e > U21 partial status: pi(U52#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [1] pi(U11#) = [] pi(isPalListKind) = [1] pi(isNeList#) = [] pi(n____) = [1, 2] pi(U41#) = [] pi(and) = [1, 2] pi(n__isPalListKind) = [1] pi(U42#) = [] pi(isList) = [] pi(U51#) = [] pi(isNeList) = [] pi(U21#) = [] pi(U22#) = [] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [1] pi(U32) = [1] pi(U42) = [] pi(U52) = [] 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) = [2] pi(U31) = [] pi(U41) = [] pi(U51) = [2] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [1, 2] 2. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = 10 tt_A = 22 isList#_A(x1) = 10 activate_A(x1) = max{150, x1 + 63} U11#_A(x1,x2) = 10 isPalListKind_A(x1) = max{149, x1 - 7} isNeList#_A(x1) = 10 n_____A(x1,x2) = max{x1 + 450, x2 + 158} U41#_A(x1,x2,x3) = 10 and_A(x1,x2) = max{150, x2 + 85} n__isPalListKind_A(x1) = 85 U42#_A(x1,x2) = 10 isList_A(x1) = 161 U51#_A(x1,x2,x3) = 10 isNeList_A(x1) = 269 U21#_A(x1,x2,x3) = 10 U22#_A(x1,x2) = 10 U23_A(x1) = 152 U43_A(x1) = 269 U53_A(x1) = 23 U12_A(x1) = 150 U22_A(x1,x2) = x1 + 130 U32_A(x1) = max{150, x1 + 129} U42_A(x1,x2) = 231 U52_A(x1,x2) = 6 isQid_A(x1) = 21 n__a_A = 89 n__e_A = 151 n__i_A = 89 n__o_A = 150 n__u_A = 151 ___A(x1,x2) = max{x1 + 451, x2 + 159} nil_A = 83 U11_A(x1,x2) = 151 U21_A(x1,x2,x3) = x2 + 387 U31_A(x1,x2) = 269 U41_A(x1,x2,x3) = 236 U51_A(x1,x2,x3) = max{451, x2 + 7} n__nil_A = 21 a_A = 151 e_A = 151 i_A = 151 o_A = 151 u_A = 151 n__and_A(x1,x2) = max{86, x2 + 85} precedence: isPalListKind = n____ > n__i > U22 > U23 > tt = U32 > n__u = u > U52 > U53 > U41 > U42 > __ > U51 > U52# = isList# = U11# = isNeList# = U41# = U42# = U51# = isNeList = U21# = U22# = isQid = n__e = n__o = e > activate = and = o > n__isPalListKind = U12 = a > U11 = U31 > isList = U43 = n__a = nil = n__nil = i > U21 > n__and partial status: pi(U52#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [1] pi(U11#) = [] pi(isPalListKind) = [] pi(isNeList#) = [] pi(n____) = [2] pi(U41#) = [] pi(and) = [2] pi(n__isPalListKind) = [] pi(U42#) = [] pi(isList) = [] pi(U51#) = [] pi(isNeList) = [] pi(U21#) = [] pi(U22#) = [] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [1] pi(U42) = [] pi(U52) = [] 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(U31) = [] pi(U41) = [] pi(U51) = [2] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [] 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: U52#(tt(),V2) -> isList#(activate(V2)) p2: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p3: U11#(tt(),V) -> isNeList#(activate(V)) p4: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p5: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p6: U42#(tt(),V2) -> isNeList#(activate(V2)) p7: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p8: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p9: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p10: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p11: U22#(tt(),V2) -> isList#(activate(V2)) p12: U21#(tt(),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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U52#(tt(),V2) -> isList#(activate(V2)) p2: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p3: U21#(tt(),V1,V2) -> isList#(activate(V1)) p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p5: U11#(tt(),V) -> isNeList#(activate(V)) p6: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p7: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p8: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p9: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p10: U42#(tt(),V2) -> isNeList#(activate(V2)) p11: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2)) p12: U22#(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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = max{96, x1 + 82, x2} tt_A = 16 isList#_A(x1) = max{97, x1} activate_A(x1) = max{19, x1} n_____A(x1,x2) = max{x1 + 167, x2} U21#_A(x1,x2,x3) = max{97, x1 - 24, x2 + 25, x3} and_A(x1,x2) = max{19, x1 + 4, x2} isPalListKind_A(x1) = max{19, x1} n__isPalListKind_A(x1) = x1 U11#_A(x1,x2) = max{97, x2} isNeList#_A(x1) = max{97, x1} U51#_A(x1,x2,x3) = max{167, x2 + 95, x3} isNeList_A(x1) = max{85, x1 + 13} U41#_A(x1,x2,x3) = max{112, x3} U42#_A(x1,x2) = max{112, x1 - 33, x2} isList_A(x1) = 24 U22#_A(x1,x2) = max{97, x2} U23_A(x1) = max{18, x1 - 8} U43_A(x1) = 17 U53_A(x1) = max{11, x1 + 10} U12_A(x1) = 17 U22_A(x1,x2) = 19 U32_A(x1) = max{29, x1 - 2} U42_A(x1,x2) = 19 U52_A(x1,x2) = x1 + 27 isQid_A(x1) = 30 n__a_A = 17 n__e_A = 20 n__i_A = 0 n__o_A = 19 n__u_A = 17 ___A(x1,x2) = max{x1 + 167, x2} nil_A = 18 U11_A(x1,x2) = 19 U21_A(x1,x2,x3) = 24 U31_A(x1,x2) = max{x1 + 13, x2 + 1} U41_A(x1,x2,x3) = max{12, x1 + 4, x2 - 18} U51_A(x1,x2,x3) = max{112, x1 - 1, x2 + 40, x3 + 13} n__nil_A = 17 a_A = 18 e_A = 20 i_A = 1 o_A = 19 u_A = 18 n__and_A(x1,x2) = max{19, x1 + 4, x2} precedence: n____ = __ > U41# > U42# > u > U41 > U42 > U23 = n__a > U12 > a > U51# > U52# > n__u > U21# > U22# > isList# > n__nil > U11# > and = n__and > activate = isPalListKind = o > isList > U11 > isQid = nil = U21 > i > isNeList > U51 > U53 = U52 = U31 > n__isPalListKind > e > U22 > n__e > n__i > U32 > tt = U43 = n__o > isNeList# partial status: pi(U52#) = [2] pi(tt) = [] pi(isList#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(U21#) = [3] pi(and) = [1, 2] pi(isPalListKind) = [1] pi(n__isPalListKind) = [1] pi(U11#) = [2] pi(isNeList#) = [1] pi(U51#) = [3] pi(isNeList) = [1] pi(U41#) = [3] pi(U42#) = [2] pi(isList) = [] pi(U22#) = [2] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [1] 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(U31) = [2] pi(U41) = [1] pi(U51) = [2, 3] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [1, 2] 2. weighted path order base order: max/plus interpretations on natural numbers: U52#_A(x1,x2) = 1417 tt_A = 42 isList#_A(x1) = x1 + 780 activate_A(x1) = 637 n_____A(x1,x2) = x1 + 106 U21#_A(x1,x2,x3) = 3 and_A(x1,x2) = 781 isPalListKind_A(x1) = 781 n__isPalListKind_A(x1) = 777 U11#_A(x1,x2) = 651 isNeList#_A(x1) = 22 U51#_A(x1,x2,x3) = x3 + 1418 isNeList_A(x1) = max{24, x1 - 60} U41#_A(x1,x2,x3) = max{22, x3 - 617} U42#_A(x1,x2) = 22 isList_A(x1) = 412 U22#_A(x1,x2) = max{3, x2} U23_A(x1) = 411 U43_A(x1) = 43 U53_A(x1) = 697 U12_A(x1) = 968 U22_A(x1,x2) = 412 U32_A(x1) = 43 U42_A(x1,x2) = 44 U52_A(x1,x2) = 697 isQid_A(x1) = 47 n__a_A = 148 n__e_A = 28 n__i_A = 28 n__o_A = 28 n__u_A = 28 ___A(x1,x2) = max{x1 + 106, x2 + 107} nil_A = 637 U11_A(x1,x2) = 412 U21_A(x1,x2,x3) = 412 U31_A(x1,x2) = x2 + 46 U41_A(x1,x2,x3) = 45 U51_A(x1,x2,x3) = max{x2 + 698, x3 - 1} n__nil_A = 267 a_A = 638 e_A = 29 i_A = 638 o_A = 636 u_A = 638 n__and_A(x1,x2) = 0 precedence: U43 > U11# > isList = n__u > U21 > U22 > activate = and = isPalListKind > __ > n____ > n__a > n__isPalListKind > U52 = U51 > e > n__e > nil > U31 = U41 = o > U32 > tt = U42 = n__o > U12 > i > n__i > isNeList# = U41# = U42# = U23 = U53 > U51# > U52# > isQid > isNeList > isList# > U21# > U22# > u > n__and > U11 = n__nil = a partial status: pi(U52#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [] pi(n____) = [1] pi(U21#) = [] pi(and) = [] pi(isPalListKind) = [] pi(n__isPalListKind) = [] pi(U11#) = [] pi(isNeList#) = [] pi(U51#) = [3] pi(isNeList) = [] pi(U41#) = [] pi(U42#) = [] pi(isList) = [] pi(U22#) = [2] pi(U23) = [] pi(U43) = [] pi(U53) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [] 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(U31) = [2] pi(U41) = [] pi(U51) = [2] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [] The next rules are strictly ordered: p1, p3, p4, p5, p6, p11, p12 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p2: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2)) p3: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p4: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p5: U42#(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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) p2: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2)) p3: U42#(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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: 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, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 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{1, x1} n_____A(x1,x2) = max{x1 + 24, x2} U41#_A(x1,x2,x3) = max{x1, x2 + 23, x3} and_A(x1,x2) = max{6, x1 - 20, x2} isPalListKind_A(x1) = max{5, x1} activate_A(x1) = x1 n__isPalListKind_A(x1) = max{5, x1} tt_A = 19 U42#_A(x1,x2) = max{x1 - 18, x2} isList_A(x1) = x1 + 34 U43_A(x1) = max{20, x1 - 23} U53_A(x1) = 20 U32_A(x1) = max{20, x1 + 4} U42_A(x1,x2) = max{x1 - 12, x2 + 20} isNeList_A(x1) = max{29, x1 + 25} U52_A(x1,x2) = 21 isQid_A(x1) = max{18, x1 + 16} n__a_A = 20 n__e_A = 20 n__i_A = 20 n__o_A = 20 n__u_A = 20 U23_A(x1) = max{20, x1 - 51} U31_A(x1,x2) = max{24, x1 + 2, x2 + 21} U41_A(x1,x2,x3) = max{x1 - 4, x2 + 34, x3 + 23} U51_A(x1,x2,x3) = max{x1 - 20, x2 + 24, x3 + 21} U12_A(x1) = max{27, x1} U22_A(x1,x2) = max{21, x1 - 36, x2 - 17} ___A(x1,x2) = max{x1 + 24, x2} nil_A = 20 U11_A(x1,x2) = max{28, x1 + 11, x2 + 26} U21_A(x1,x2,x3) = max{x1 - 7, x2 + 21, x3 - 1} n__nil_A = 20 a_A = 20 e_A = 20 i_A = 20 o_A = 20 u_A = 20 n__and_A(x1,x2) = max{6, x1 - 20, x2} precedence: U21 > U53 > isQid > n____ = __ > U41# > isList = U11 > U12 > U51 > n__u = u > isPalListKind = n__isPalListKind > U42# > U22 > isNeList > U23 = U31 > tt > U52 > U41 > and = activate = a = e = n__and > n__a > o > n__e > isNeList# = n__i = n__o = i > nil > U32 = n__nil > U43 = U42 partial status: pi(isNeList#) = [1] pi(n____) = [1, 2] pi(U41#) = [1, 3] pi(and) = [2] pi(isPalListKind) = [1] pi(activate) = [1] pi(n__isPalListKind) = [1] pi(tt) = [] pi(U42#) = [2] pi(isList) = [1] pi(U43) = [] pi(U53) = [] pi(U32) = [] pi(U42) = [] pi(isNeList) = [1] pi(U52) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U23) = [] pi(U31) = [1, 2] pi(U41) = [3] pi(U51) = [2, 3] pi(U12) = [] pi(U22) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [2] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [2] 2. weighted path order base order: max/plus interpretations on natural numbers: isNeList#_A(x1) = x1 + 6 n_____A(x1,x2) = 70 U41#_A(x1,x2,x3) = 70 and_A(x1,x2) = 113 isPalListKind_A(x1) = x1 + 125 activate_A(x1) = 72 n__isPalListKind_A(x1) = 1 tt_A = 3 U42#_A(x1,x2) = x2 + 78 isList_A(x1) = x1 + 109 U43_A(x1) = 180 U53_A(x1) = 180 U32_A(x1) = 121 U42_A(x1,x2) = 180 isNeList_A(x1) = x1 + 119 U52_A(x1,x2) = 181 isQid_A(x1) = 121 n__a_A = 0 n__e_A = 0 n__i_A = 0 n__o_A = 2 n__u_A = 0 U23_A(x1) = 8 U31_A(x1,x2) = max{120, x1 + 6, x2 + 54} U41_A(x1,x2,x3) = 181 U51_A(x1,x2,x3) = max{70, x3 + 43} U12_A(x1) = 2 U22_A(x1,x2) = 8 ___A(x1,x2) = 71 nil_A = 1 U11_A(x1,x2) = 1 U21_A(x1,x2,x3) = x2 + 8 n__nil_A = 0 a_A = 65 e_A = 65 i_A = 65 o_A = 67 u_A = 65 n__and_A(x1,x2) = 67 precedence: U21 > U42 = n__o = i > U32 > e > n__a > U11 > u > n__i = U22 = n__nil > nil > U42# > isPalListKind > and > activate > __ > isList > n____ > U23 > n__and > isNeList# = U41# = n__u > tt > U31 > U41 > isNeList > U51 > a > U53 > isQid > U52 = n__e = o > U43 = U12 > n__isPalListKind partial status: pi(isNeList#) = [1] pi(n____) = [] pi(U41#) = [] pi(and) = [] pi(isPalListKind) = [] pi(activate) = [] pi(n__isPalListKind) = [] pi(tt) = [] pi(U42#) = [] pi(isList) = [1] pi(U43) = [] pi(U53) = [] pi(U32) = [] pi(U42) = [] pi(isNeList) = [1] pi(U52) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U23) = [] pi(U31) = [2] pi(U41) = [] pi(U51) = [3] pi(U12) = [] pi(U22) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] pi(n__and) = [] 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: isPalListKind#(n____(V1,V2)) -> activate#(V2) p2: activate#(n__and(X1,X2)) -> and#(X1,X2) p3: and#(tt(),X) -> activate#(X) p4: activate#(n__isPalListKind(X)) -> isPalListKind#(X) p5: isPalListKind#(n____(V1,V2)) -> activate#(V1) p6: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p7: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The set of usable rules consists of r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: isPalListKind#_A(x1) = max{2, x1} n_____A(x1,x2) = max{9, x1 + 5, x2} activate#_A(x1) = x1 n__and_A(x1,x2) = max{7, x1 + 1, x2} and#_A(x1,x2) = max{6, x1 + 1, x2} tt_A = 0 n__isPalListKind_A(x1) = max{8, x1} activate_A(x1) = x1 isPalListKind_A(x1) = max{8, x1} ___A(x1,x2) = max{9, x1 + 5, x2} nil_A = 1 and_A(x1,x2) = max{7, x1 + 1, x2} n__nil_A = 1 a_A = 1 n__a_A = 1 e_A = 1 n__e_A = 1 i_A = 1 n__i_A = 1 o_A = 1 n__o_A = 1 u_A = 1 n__u_A = 1 precedence: n____ = __ > isPalListKind# = n__and = n__isPalListKind = activate = isPalListKind = and = a = u > n__a > nil > n__nil = o > e = n__e = n__o > tt = i = n__u > n__i > and# > activate# partial status: pi(isPalListKind#) = [1] pi(n____) = [1, 2] pi(activate#) = [1] pi(n__and) = [2] pi(and#) = [1, 2] pi(tt) = [] pi(n__isPalListKind) = [1] pi(activate) = [1] pi(isPalListKind) = [1] pi(__) = [1, 2] pi(nil) = [] pi(and) = [2] 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: isPalListKind#_A(x1) = x1 + 11 n_____A(x1,x2) = max{x1 + 46, x2} activate#_A(x1) = x1 + 4 n__and_A(x1,x2) = x2 + 21 and#_A(x1,x2) = x2 + 4 tt_A = 32 n__isPalListKind_A(x1) = 1 activate_A(x1) = max{31, x1 + 12} isPalListKind_A(x1) = max{10, x1 - 12} ___A(x1,x2) = max{x1 + 58, x2} nil_A = 32 and_A(x1,x2) = x2 + 33 n__nil_A = 31 a_A = 31 n__a_A = 0 e_A = 30 n__e_A = 17 i_A = 32 n__i_A = 31 o_A = 13 n__o_A = 0 u_A = 30 n__u_A = 0 precedence: o > activate# = and# = n__o = u = n__u > n__and > n__isPalListKind > activate > isPalListKind = __ > n____ > isPalListKind# > tt = nil = and = n__nil = a = n__a = e = n__e = i = n__i partial status: pi(isPalListKind#) = [1] pi(n____) = [2] pi(activate#) = [] pi(n__and) = [] pi(and#) = [2] pi(tt) = [] pi(n__isPalListKind) = [] pi(activate) = [] pi(isPalListKind) = [] pi(__) = [1, 2] pi(nil) = [] pi(and) = [2] 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, p4, p5, p6, p7 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(),V) -> U12(isNeList(activate(V))) r5: U12(tt()) -> tt() r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) r7: U22(tt(),V2) -> U23(isList(activate(V2))) r8: U23(tt()) -> tt() r9: U31(tt(),V) -> U32(isQid(activate(V))) r10: U32(tt()) -> tt() r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) r12: U42(tt(),V2) -> U43(isNeList(activate(V2))) r13: U43(tt()) -> tt() r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) r15: U52(tt(),V2) -> U53(isList(activate(V2))) r16: U53(tt()) -> tt() r17: U61(tt(),V) -> U62(isQid(activate(V))) r18: U62(tt()) -> tt() r19: U71(tt(),V) -> U72(isNePal(activate(V))) r20: U72(tt()) -> tt() r21: and(tt(),X) -> activate(X) r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r23: isList(n__nil()) -> tt() r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) r31: isPal(n__nil()) -> tt() r32: isPalListKind(n__a()) -> tt() r33: isPalListKind(n__e()) -> tt() r34: isPalListKind(n__i()) -> tt() r35: isPalListKind(n__nil()) -> tt() r36: isPalListKind(n__o()) -> tt() r37: isPalListKind(n__u()) -> tt() r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) r39: isQid(n__a()) -> tt() r40: isQid(n__e()) -> tt() r41: isQid(n__i()) -> tt() r42: isQid(n__o()) -> tt() r43: isQid(n__u()) -> tt() r44: nil() -> n__nil() r45: __(X1,X2) -> n____(X1,X2) r46: isPalListKind(X) -> n__isPalListKind(X) r47: and(X1,X2) -> n__and(X1,X2) r48: a() -> n__a() r49: e() -> n__e() r50: i() -> n__i() r51: o() -> n__o() r52: u() -> n__u() r53: activate(n__nil()) -> nil() r54: activate(n____(X1,X2)) -> __(X1,X2) r55: activate(n__isPalListKind(X)) -> isPalListKind(X) r56: activate(n__and(X1,X2)) -> and(X1,X2) r57: activate(n__a()) -> a() r58: activate(n__e()) -> e() r59: activate(n__i()) -> i() r60: activate(n__o()) -> o() r61: activate(n__u()) -> u() r62: activate(X) -> X The set of usable rules consists of r1, r2, r3, r45 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.