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(isPalListKind(activate(V)),activate(V)) U12(tt(),V) -> U13(isNeList(activate(V))) U13(tt()) -> tt() U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) U25(tt(),V2) -> U26(isList(activate(V2))) U26(tt()) -> tt() U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isQid(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNeList(activate(V2))) U46(tt()) -> tt() U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) U55(tt(),V2) -> U56(isList(activate(V2))) U56(tt()) -> tt() U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) U62(tt(),V) -> U63(isQid(activate(V))) U63(tt()) -> tt() U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) U73(tt(),P) -> U74(isPalListKind(activate(P))) U74(tt()) -> tt() U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) U82(tt(),V) -> U83(isNePal(activate(V))) U83(tt()) -> tt() U91(tt(),V2) -> U92(isPalListKind(activate(V2))) U92(tt()) -> tt() isList(V) -> U11(isPalListKind(activate(V)),activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) isPal(V) -> U81(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)) -> U91(isPalListKind(activate(V1)),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) 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__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#(isPalListKind(activate(V)),activate(V)) p4: U11#(tt(),V) -> isPalListKind#(activate(V)) p5: U11#(tt(),V) -> activate#(V) p6: U12#(tt(),V) -> U13#(isNeList(activate(V))) p7: U12#(tt(),V) -> isNeList#(activate(V)) p8: U12#(tt(),V) -> activate#(V) p9: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p10: U21#(tt(),V1,V2) -> isPalListKind#(activate(V1)) p11: U21#(tt(),V1,V2) -> activate#(V1) p12: U21#(tt(),V1,V2) -> activate#(V2) p13: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p14: U22#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p15: U22#(tt(),V1,V2) -> activate#(V2) p16: U22#(tt(),V1,V2) -> activate#(V1) p17: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p18: U23#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p19: U23#(tt(),V1,V2) -> activate#(V2) p20: U23#(tt(),V1,V2) -> activate#(V1) p21: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p22: U24#(tt(),V1,V2) -> isList#(activate(V1)) p23: U24#(tt(),V1,V2) -> activate#(V1) p24: U24#(tt(),V1,V2) -> activate#(V2) p25: U25#(tt(),V2) -> U26#(isList(activate(V2))) p26: U25#(tt(),V2) -> isList#(activate(V2)) p27: U25#(tt(),V2) -> activate#(V2) p28: U31#(tt(),V) -> U32#(isPalListKind(activate(V)),activate(V)) p29: U31#(tt(),V) -> isPalListKind#(activate(V)) p30: U31#(tt(),V) -> activate#(V) p31: U32#(tt(),V) -> U33#(isQid(activate(V))) p32: U32#(tt(),V) -> isQid#(activate(V)) p33: U32#(tt(),V) -> activate#(V) p34: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p35: U41#(tt(),V1,V2) -> isPalListKind#(activate(V1)) p36: U41#(tt(),V1,V2) -> activate#(V1) p37: U41#(tt(),V1,V2) -> activate#(V2) p38: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p39: U42#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p40: U42#(tt(),V1,V2) -> activate#(V2) p41: U42#(tt(),V1,V2) -> activate#(V1) p42: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p43: U43#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p44: U43#(tt(),V1,V2) -> activate#(V2) p45: U43#(tt(),V1,V2) -> activate#(V1) p46: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p47: U44#(tt(),V1,V2) -> isList#(activate(V1)) p48: U44#(tt(),V1,V2) -> activate#(V1) p49: U44#(tt(),V1,V2) -> activate#(V2) p50: U45#(tt(),V2) -> U46#(isNeList(activate(V2))) p51: U45#(tt(),V2) -> isNeList#(activate(V2)) p52: U45#(tt(),V2) -> activate#(V2) p53: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p54: U51#(tt(),V1,V2) -> isPalListKind#(activate(V1)) p55: U51#(tt(),V1,V2) -> activate#(V1) p56: U51#(tt(),V1,V2) -> activate#(V2) p57: U52#(tt(),V1,V2) -> U53#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p58: U52#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p59: U52#(tt(),V1,V2) -> activate#(V2) p60: U52#(tt(),V1,V2) -> activate#(V1) p61: U53#(tt(),V1,V2) -> U54#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p62: U53#(tt(),V1,V2) -> isPalListKind#(activate(V2)) p63: U53#(tt(),V1,V2) -> activate#(V2) p64: U53#(tt(),V1,V2) -> activate#(V1) p65: U54#(tt(),V1,V2) -> U55#(isNeList(activate(V1)),activate(V2)) p66: U54#(tt(),V1,V2) -> isNeList#(activate(V1)) p67: U54#(tt(),V1,V2) -> activate#(V1) p68: U54#(tt(),V1,V2) -> activate#(V2) p69: U55#(tt(),V2) -> U56#(isList(activate(V2))) p70: U55#(tt(),V2) -> isList#(activate(V2)) p71: U55#(tt(),V2) -> activate#(V2) p72: U61#(tt(),V) -> U62#(isPalListKind(activate(V)),activate(V)) p73: U61#(tt(),V) -> isPalListKind#(activate(V)) p74: U61#(tt(),V) -> activate#(V) p75: U62#(tt(),V) -> U63#(isQid(activate(V))) p76: U62#(tt(),V) -> isQid#(activate(V)) p77: U62#(tt(),V) -> activate#(V) p78: U71#(tt(),I,P) -> U72#(isPalListKind(activate(I)),activate(P)) p79: U71#(tt(),I,P) -> isPalListKind#(activate(I)) p80: U71#(tt(),I,P) -> activate#(I) p81: U71#(tt(),I,P) -> activate#(P) p82: U72#(tt(),P) -> U73#(isPal(activate(P)),activate(P)) p83: U72#(tt(),P) -> isPal#(activate(P)) p84: U72#(tt(),P) -> activate#(P) p85: U73#(tt(),P) -> U74#(isPalListKind(activate(P))) p86: U73#(tt(),P) -> isPalListKind#(activate(P)) p87: U73#(tt(),P) -> activate#(P) p88: U81#(tt(),V) -> U82#(isPalListKind(activate(V)),activate(V)) p89: U81#(tt(),V) -> isPalListKind#(activate(V)) p90: U81#(tt(),V) -> activate#(V) p91: U82#(tt(),V) -> U83#(isNePal(activate(V))) p92: U82#(tt(),V) -> isNePal#(activate(V)) p93: U82#(tt(),V) -> activate#(V) p94: U91#(tt(),V2) -> U92#(isPalListKind(activate(V2))) p95: U91#(tt(),V2) -> isPalListKind#(activate(V2)) p96: U91#(tt(),V2) -> activate#(V2) p97: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p98: isList#(V) -> isPalListKind#(activate(V)) p99: isList#(V) -> activate#(V) p100: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p101: isList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p102: isList#(n____(V1,V2)) -> activate#(V1) p103: isList#(n____(V1,V2)) -> activate#(V2) p104: isNeList#(V) -> U31#(isPalListKind(activate(V)),activate(V)) p105: isNeList#(V) -> isPalListKind#(activate(V)) p106: isNeList#(V) -> activate#(V) p107: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p108: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p109: isNeList#(n____(V1,V2)) -> activate#(V1) p110: isNeList#(n____(V1,V2)) -> activate#(V2) p111: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p112: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p113: isNeList#(n____(V1,V2)) -> activate#(V1) p114: isNeList#(n____(V1,V2)) -> activate#(V2) p115: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V)) p116: isNePal#(V) -> isPalListKind#(activate(V)) p117: isNePal#(V) -> activate#(V) p118: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(I),activate(P)) p119: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) p120: isNePal#(n____(I,__(P,I))) -> activate#(I) p121: isNePal#(n____(I,__(P,I))) -> activate#(P) p122: isPal#(V) -> U81#(isPalListKind(activate(V)),activate(V)) p123: isPal#(V) -> isPalListKind#(activate(V)) p124: isPal#(V) -> activate#(V) p125: isPalListKind#(n____(V1,V2)) -> U91#(isPalListKind(activate(V1)),activate(V2)) p126: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1)) p127: isPalListKind#(n____(V1,V2)) -> activate#(V1) p128: isPalListKind#(n____(V1,V2)) -> activate#(V2) p129: activate#(n__nil()) -> nil#() p130: activate#(n____(X1,X2)) -> __#(X1,X2) p131: activate#(n__a()) -> a#() p132: activate#(n__e()) -> e#() p133: activate#(n__i()) -> i#() p134: activate#(n__o()) -> o#() p135: 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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The estimated dependency graph contains the following SCCs: {p78, p83, p88, p92, p118, p122} {p3, p7, p9, p13, p17, p21, p22, p26, p34, p38, p42, p46, p47, p51, p53, p57, p61, p65, p66, p70, p97, p100, p107, p111} {p95, p125, p126} {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U82#(tt(),V) -> isNePal#(activate(V)) p2: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(I),activate(P)) p3: U71#(tt(),I,P) -> U72#(isPalListKind(activate(I)),activate(P)) p4: U72#(tt(),P) -> isPal#(activate(P)) p5: isPal#(V) -> U81#(isPalListKind(activate(V)),activate(V)) p6: U81#(tt(),V) -> U82#(isPalListKind(activate(V)),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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r38, r39, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U82#_A(x1,x2) = ((1,0),(0,0)) x2 + (13,22) tt_A() = (22,25) isNePal#_A(x1) = ((1,0),(1,0)) x1 + (10,10) activate_A(x1) = x1 + (2,28) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (0,2) ___A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (0,29) U71#_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x3 + (4,5) isQid_A(x1) = ((1,0),(1,0)) x1 + (1,1) U72#_A(x1,x2) = ((1,0),(0,0)) x2 + (22,26) isPalListKind_A(x1) = ((1,0),(0,0)) x1 + (23,1) isPal#_A(x1) = ((1,0),(0,0)) x1 + (19,24) U81#_A(x1,x2) = ((1,0),(0,0)) x2 + (16,23) U92_A(x1) = (22,26) nil_A() = (23,30) U91_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (22,5) n__nil_A() = (23,1) a_A() = (26,27) n__a_A() = (25,26) e_A() = (26,54) n__e_A() = (25,26) i_A() = (24,30) n__i_A() = (23,1) o_A() = (23,1) n__o_A() = (23,1) u_A() = (23,29) n__u_A() = (23,1) precedence: isQid = isPal# > U82# = U81# > tt = isNePal# = activate = __ = U71# = U72# = isPalListKind = U92 = U91 = n__nil = n__a = n__e = i > n____ = nil = u = n__u > n__i > a > o > e > n__o partial status: pi(U82#) = [] pi(tt) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n____) = [] pi(__) = [] pi(U71#) = [] pi(isQid) = [] pi(U72#) = [] pi(isPalListKind) = [] pi(isPal#) = [] pi(U81#) = [] pi(U92) = [] pi(nil) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(I),activate(P)) p2: U71#(tt(),I,P) -> U72#(isPalListKind(activate(I)),activate(P)) p3: U72#(tt(),P) -> isPal#(activate(P)) p4: isPal#(V) -> U81#(isPalListKind(activate(V)),activate(V)) p5: U81#(tt(),V) -> U82#(isPalListKind(activate(V)),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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: 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(),V1,V2) -> U53#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p2: U53#(tt(),V1,V2) -> U54#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p3: U54#(tt(),V1,V2) -> isNeList#(activate(V1)) p4: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p5: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p6: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p7: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p8: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p9: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p10: U44#(tt(),V1,V2) -> isList#(activate(V1)) p11: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p12: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p13: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p14: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p15: U24#(tt(),V1,V2) -> isList#(activate(V1)) p16: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p17: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p18: U12#(tt(),V) -> isNeList#(activate(V)) p19: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p20: U25#(tt(),V2) -> isList#(activate(V2)) p21: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p22: U45#(tt(),V2) -> isNeList#(activate(V2)) p23: U54#(tt(),V1,V2) -> U55#(isNeList(activate(V1)),activate(V2)) p24: U55#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U52#_A(x1,x2,x3) = x1 + ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (40,205) tt_A() = (79,207) U53#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + x3 + (100,128) isPalListKind_A(x1) = ((0,0),(1,0)) x1 + (120,141) activate_A(x1) = ((1,0),(1,0)) x1 + (9,154) U54#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (81,77) isNeList#_A(x1) = x1 + (1,1) n_____A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (200,151) U51#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (179,132) U41#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (61,154) U42#_A(x1,x2,x3) = x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (1,0) U43#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (60,192) U44#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (41,173) isList#_A(x1) = ((1,0),(1,0)) x1 + (31,143) U21#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (212,335) U22#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (193,214) U23#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (121,172) U24#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (81,130) U11#_A(x1,x2) = ((1,0),(0,0)) x2 + (21,142) U12#_A(x1,x2) = ((1,0),(1,0)) x2 + (11,199) U25#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (71,122) isList_A(x1) = ((0,0),(1,0)) x1 + (86,331) U45#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (11,77) U55#_A(x1,x2) = ((1,0),(0,0)) x2 + (71,153) isNeList_A(x1) = ((1,0),(1,1)) x1 + (172,149) U26_A(x1) = (80,208) U46_A(x1) = (80,206) U56_A(x1) = ((1,0),(0,0)) x1 + (1,1) U25_A(x1,x2) = ((0,0),(1,0)) x2 + (81,209) U45_A(x1,x2) = (81,208) U55_A(x1,x2) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (9,18) U24_A(x1,x2,x3) = (82,150) U44_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (3,130) U54_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((0,0),(1,0)) x3 + (191,209) U13_A(x1) = ((0,0),(1,0)) x1 + (80,129) U23_A(x1,x2,x3) = (83,151) U33_A(x1) = ((1,0),(1,1)) x1 + (1,1) U43_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (124,70) U53_A(x1,x2,x3) = x2 + ((0,0),(1,0)) x3 + (292,45) isQid_A(x1) = ((1,0),(0,0)) x1 + (80,239) n__a_A() = (80,0) n__e_A() = (0,0) n__i_A() = (80,0) n__o_A() = (80,0) n__u_A() = (80,0) U12_A(x1,x2) = ((0,0),(1,0)) x2 + (81,311) U22_A(x1,x2,x3) = (84,152) U32_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (91,159) U42_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (125,155) U52_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((0,0),(1,0)) x3 + (302,209) U92_A(x1) = (80,208) ___A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (201,152) nil_A() = (68,221) U11_A(x1,x2) = ((0,0),(1,0)) x2 + (85,321) U21_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (85,153) U31_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (42,1) U41_A(x1,x2,x3) = x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (63,1) U51_A(x1,x2,x3) = x1 + ((1,0),(0,0)) x2 + x3 + (233,1) U91_A(x1,x2) = (81,209) n__nil_A() = (67,0) a_A() = (80,0) e_A() = (1,155) i_A() = (80,0) o_A() = (81,1) u_A() = (80,0) precedence: U31 > U56 > U41# > U42# = n__nil = a > U51# > U52# = isList > U12 > U44 > n__a > U21# = U22# = U23# > U55# > U11 > __ > activate = o > U25 > nil > isNeList > U41 > U42 > isPalListKind = U45 = U43 = isQid = U91 > tt > U43# = U44# = U45# > n____ > n__o > U24# > u > U25# > U11# = U12# > isList# > isNeList# > U26 = U13 > U51 > U92 > n__u > n__e = U52 = e > U53 > U54 > U23 > U55 > n__i = U32 = i > U46 > U53# = U54# > U24 = U33 = U22 = U21 partial status: pi(U52#) = [3] pi(tt) = [] pi(U53#) = [3] pi(isPalListKind) = [] pi(activate) = [] pi(U54#) = [] pi(isNeList#) = [1] pi(n____) = [] pi(U51#) = [] pi(U41#) = [] pi(U42#) = [1] pi(U43#) = [3] pi(U44#) = [] pi(isList#) = [] pi(U21#) = [] pi(U22#) = [] pi(U23#) = [] pi(U24#) = [] pi(U11#) = [] pi(U12#) = [] pi(U25#) = [] pi(isList) = [] pi(U45#) = [] pi(U55#) = [] pi(isNeList) = [] pi(U26) = [] pi(U46) = [] pi(U56) = [] pi(U25) = [] pi(U45) = [] pi(U55) = [] pi(U24) = [] pi(U44) = [] pi(U54) = [] pi(U13) = [] pi(U23) = [] pi(U33) = [] pi(U43) = [] pi(U53) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [2] pi(U92) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U53#(tt(),V1,V2) -> U54#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p2: U54#(tt(),V1,V2) -> isNeList#(activate(V1)) p3: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p5: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p6: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p7: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p8: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p9: U44#(tt(),V1,V2) -> isList#(activate(V1)) p10: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p11: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p12: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p13: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p14: U24#(tt(),V1,V2) -> isList#(activate(V1)) p15: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p16: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p17: U12#(tt(),V) -> isNeList#(activate(V)) p18: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p19: U25#(tt(),V2) -> isList#(activate(V2)) p20: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p21: U45#(tt(),V2) -> isNeList#(activate(V2)) p22: U54#(tt(),V1,V2) -> U55#(isNeList(activate(V1)),activate(V2)) p23: U55#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The estimated dependency graph contains the following SCCs: {p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U45#(tt(),V2) -> isNeList#(activate(V2)) p2: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p6: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p7: U44#(tt(),V1,V2) -> isList#(activate(V1)) p8: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p9: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p10: U12#(tt(),V) -> isNeList#(activate(V)) p11: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p12: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p13: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p14: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p15: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p16: U25#(tt(),V2) -> isList#(activate(V2)) p17: U24#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U45#_A(x1,x2) = ((1,0),(1,0)) x2 + (55,85) tt_A() = (0,0) isNeList#_A(x1) = x1 + (1,75) activate_A(x1) = ((1,0),(1,0)) x1 + (5,9) n_____A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (105,83) U41#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (94,152) isPalListKind_A(x1) = ((1,0),(0,0)) x1 + (43,85) U42#_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (83,142) U43#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (72,122) U44#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (61,102) isList_A(x1) = ((1,0),(0,0)) x1 + (0,192) isList#_A(x1) = ((1,0),(1,0)) x1 + (55,96) U11#_A(x1,x2) = x2 + (49,86) U12#_A(x1,x2) = ((1,0),(0,0)) x2 + (7,85) U21#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (150,195) U22#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (87,195) U23#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (77,194) U24#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (66,193) U25#_A(x1,x2) = ((1,0),(0,0)) x2 + (61,102) U46_A(x1) = (1,1) U56_A(x1) = (1,1) U45_A(x1,x2) = (26,2) isNeList_A(x1) = ((1,0),(1,0)) x1 + (20,92) U55_A(x1,x2) = (2,2) U44_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (27,3) U54_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (6,3) U26_A(x1) = ((0,0),(1,0)) x1 + (1,1) U33_A(x1) = ((1,0),(1,0)) x1 + (1,1) U43_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (48,86) U53_A(x1,x2,x3) = ((1,0),(1,0)) x3 + (55,4) isQid_A(x1) = ((1,0),(0,0)) x1 + (1,9) n__a_A() = (1,1) n__e_A() = (1,0) n__i_A() = (1,1) n__o_A() = (1,1) n__u_A() = (1,1) U25_A(x1,x2) = ((0,0),(1,0)) x2 + (2,7) U32_A(x1,x2) = ((1,0),(1,0)) x2 + (8,8) U42_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (93,92) U52_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x3 + (61,86) U24_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (3,13) U31_A(x1,x2) = ((1,0),(1,0)) x2 + (14,86) U41_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (94,8) U51_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (101,191) U13_A(x1) = (0,1) U23_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (4,86) U12_A(x1,x2) = (0,2) U22_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x3 + (6,92) U92_A(x1) = ((0,0),(1,0)) x1 + (1,37) ___A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (109,84) nil_A() = (1,0) U11_A(x1,x2) = (0,3) U21_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (7,146) U91_A(x1,x2) = (2,84) n__nil_A() = (0,0) a_A() = (2,2) e_A() = (2,11) i_A() = (2,2) o_A() = (5,2) u_A() = (2,9) precedence: n__a = U92 > e > U25# > nil > U21# = U22# > U45# = U41# = U42# = U43# = U44# = n__o > n__i > n__u > activate > isList > U21 > U54 > U56 = U55 > U11 > U24# > U23# > n____ > __ > U31 = U91 > isPalListKind > U23 > U22 > n__nil > tt = U33 = isQid = U32 > isNeList > U24 = U51 = i > U11# = U12# > isNeList# = U13 = U12 > U44 = U43 > isList# = U42 > U46 = U45 > U41 > U52 > U53 = a = o > n__e = u > U26 = U25 partial status: pi(U45#) = [] pi(tt) = [] pi(isNeList#) = [] pi(activate) = [] pi(n____) = [] pi(U41#) = [] pi(isPalListKind) = [] pi(U42#) = [] pi(U43#) = [] pi(U44#) = [] pi(isList) = [] pi(isList#) = [] pi(U11#) = [2] pi(U12#) = [] pi(U21#) = [] pi(U22#) = [] pi(U23#) = [] pi(U24#) = [] pi(U25#) = [] pi(U46) = [] pi(U56) = [] pi(U45) = [] pi(isNeList) = [] pi(U55) = [] pi(U44) = [] pi(U54) = [] pi(U26) = [] pi(U33) = [] pi(U43) = [] pi(U53) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U25) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [] pi(U24) = [] pi(U31) = [] pi(U41) = [3] pi(U51) = [] pi(U13) = [] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p7 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U45#(tt(),V2) -> isNeList#(activate(V2)) p2: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p6: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p7: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p8: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p9: U12#(tt(),V) -> isNeList#(activate(V)) p10: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p11: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p12: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p13: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p14: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p15: U25#(tt(),V2) -> isList#(activate(V2)) p16: U24#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The estimated dependency graph contains the following SCCs: {p10, p11, p12, p13, p14, p15, p16} {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U25#(tt(),V2) -> isList#(activate(V2)) p2: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p6: U24#(tt(),V1,V2) -> isList#(activate(V1)) p7: U24#(tt(),V1,V2) -> U25#(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(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U25#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (4,1) tt_A() = (12,34) isList#_A(x1) = x1 + (14,18) activate_A(x1) = x1 + (0,2) n_____A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (7,17) U21#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (21,34) isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (1,16) U22#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (21,33) U23#_A(x1,x2,x3) = x2 + x3 + (14,28) U24#_A(x1,x2,x3) = x2 + x3 + (14,23) isList_A(x1) = x1 + (9,20) U46_A(x1) = (13,35) U56_A(x1) = ((0,0),(1,0)) x1 + (13,26) U45_A(x1,x2) = (14,36) isNeList_A(x1) = ((1,0),(1,0)) x1 + (5,35) U55_A(x1,x2) = x1 + (8,2) U44_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (15,34) U54_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (14,38) U26_A(x1) = ((0,0),(1,0)) x1 + (13,26) U33_A(x1) = (13,35) U43_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (16,36) U53_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (3,39) isQid_A(x1) = ((1,0),(1,0)) x1 + (13,47) n__a_A() = (11,7) n__e_A() = (11,7) n__i_A() = (13,0) n__o_A() = (11,8) n__u_A() = (11,7) U25_A(x1,x2) = x1 + (2,13) U32_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (14,34) U42_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x3 + (5,37) U52_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (5,40) U24_A(x1,x2,x3) = x2 + (13,36) U31_A(x1,x2) = x1 + (3,2) U41_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((0,0),(1,0)) x3 + (8,26) U51_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (8,41) U13_A(x1) = ((1,0),(0,0)) x1 + (1,35) U23_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + (9,39) U12_A(x1,x2) = x2 + (7,3) U22_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (11,42) U92_A(x1) = (13,35) ___A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (7,19) nil_A() = (13,5) U11_A(x1,x2) = ((1,0),(0,0)) x2 + (8,19) U21_A(x1,x2,x3) = ((0,0),(1,0)) x1 + x2 + ((1,0),(1,0)) x3 + (12,33) U91_A(x1,x2) = ((1,0),(0,0)) x1 + (2,1) n__nil_A() = (13,4) a_A() = (11,7) e_A() = (11,7) i_A() = (13,0) o_A() = (11,8) u_A() = (11,8) precedence: U31 = U11 > activate = isPalListKind = n__i = e = i = u > U22# > U23# = U24# = U53 = o > U45 = U44 = U54 = U92 > U13 = U12 > isQid > n____ = U55 = U22 = __ = nil = U21 = n__nil = a > isList > U26 = U33 = U25 = U32 = U24 = U23 > U46 = U56 = n__e = n__u > tt = isNeList = n__a = U52 = U41 = U51 > U25# = isList# > U21# > U43 = n__o = U42 = U91 partial status: pi(U25#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [1] pi(n____) = [] pi(U21#) = [] pi(isPalListKind) = [] pi(U22#) = [] pi(U23#) = [3] pi(U24#) = [] pi(isList) = [1] pi(U46) = [] pi(U56) = [] pi(U45) = [] pi(isNeList) = [] pi(U55) = [] pi(U44) = [] pi(U54) = [] pi(U26) = [] pi(U33) = [] pi(U43) = [] pi(U53) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U25) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [] pi(U24) = [2] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(U13) = [] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U25#(tt(),V2) -> isList#(activate(V2)) p2: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U24#(tt(),V1,V2) -> isList#(activate(V1)) p6: U24#(tt(),V1,V2) -> U25#(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(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: 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: U45#(tt(),V2) -> isNeList#(activate(V2)) p2: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p4: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p6: U44#(tt(),V1,V2) -> U45#(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(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U45#_A(x1,x2) = ((1,0),(0,0)) x2 + (21,41) tt_A() = (19,39) isNeList#_A(x1) = x1 + (18,19) activate_A(x1) = ((1,0),(1,1)) x1 + (2,21) n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (33,27) U41#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (30,45) isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (4,6) U42#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x3 + (12,44) U43#_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (27,43) U44#_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (24,42) isList_A(x1) = ((1,0),(0,0)) x1 + (20,20) U46_A(x1) = (20,40) U56_A(x1) = (20,40) U45_A(x1,x2) = ((0,0),(1,0)) x2 + (21,61) isNeList_A(x1) = ((1,0),(1,1)) x1 + (10,37) U55_A(x1,x2) = (23,41) U44_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (23,64) U54_A(x1,x2,x3) = (24,42) U26_A(x1) = (20,40) U33_A(x1) = ((1,0),(1,1)) x1 U43_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (24,48) U53_A(x1,x2,x3) = (25,43) isQid_A(x1) = ((0,0),(1,0)) x1 + (20,22) n__a_A() = (18,16) n__e_A() = (34,0) n__i_A() = (34,0) n__o_A() = (16,17) n__u_A() = (20,1) U25_A(x1,x2) = (21,41) U32_A(x1,x2) = (21,19) U42_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (25,40) U52_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x3 + (12,1) U24_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (23,42) U31_A(x1,x2) = ((1,0),(1,0)) x1 + (3,1) U41_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (28,22) U51_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (21,20) U13_A(x1) = (20,60) U23_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + ((0,0),(1,0)) x3 + (12,43) U12_A(x1,x2) = ((1,0),(1,1)) x1 + (2,1) U22_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (21,48) U92_A(x1) = ((1,0),(0,0)) x1 + (14,1) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (33,28) nil_A() = (22,1) U11_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (9,1) U21_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (30,22) U91_A(x1,x2) = ((1,0),(0,0)) x2 + (32,28) n__nil_A() = (20,0) a_A() = (19,17) e_A() = (35,56) i_A() = (35,1) o_A() = (18,18) u_A() = (21,41) precedence: U32 > U91 > U31 > U45# = U26 = U25 > U45 > isNeList > U53 > U56 = U55 = U54 > activate = U52 > U24 > n__nil > U43 > U44 > isQid > n__o > o > U92 > u > n__u = __ > U42# > isNeList# > U41# = isList > U11 > U43# = U44# > U21 > U13 > U22 > isPalListKind > tt > U46 > n____ > U23 > i > e > n__e > U41 > U42 > U33 = n__i = U51 = U12 = nil = a > n__a partial status: pi(U45#) = [] pi(tt) = [] pi(isNeList#) = [] pi(activate) = [1] pi(n____) = [2] pi(U41#) = [] pi(isPalListKind) = [] pi(U42#) = [] pi(U43#) = [] pi(U44#) = [] pi(isList) = [] pi(U46) = [] pi(U56) = [] pi(U45) = [] pi(isNeList) = [1] pi(U55) = [] pi(U44) = [] pi(U54) = [] pi(U26) = [] pi(U33) = [] pi(U43) = [] pi(U53) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U25) = [] pi(U32) = [] pi(U42) = [] pi(U52) = [] pi(U24) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [] pi(U13) = [] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p2: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p4: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: U44#(tt(),V1,V2) -> U45#(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(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: 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: isPalListKind#(n____(V1,V2)) -> U91#(isPalListKind(activate(V1)),activate(V2)) p2: U91#(tt(),V2) -> isPalListKind#(activate(V2)) p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r38, r39, r50, r51, r52, r53, r54, r55, r56, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isPalListKind#_A(x1) = x1 + (1,2) n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (13,16) U91#_A(x1,x2) = ((1,0),(1,1)) x2 + (7,20) isPalListKind_A(x1) = (4,15) activate_A(x1) = x1 + (5,19) tt_A() = (1,16) U92_A(x1) = (2,0) ___A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (14,15) nil_A() = (3,1) U91_A(x1,x2) = (3,14) n__nil_A() = (2,17) a_A() = (3,0) n__a_A() = (2,17) e_A() = (3,0) n__e_A() = (2,1) i_A() = (3,18) n__i_A() = (2,17) o_A() = (3,0) n__o_A() = (2,17) u_A() = (3,16) n__u_A() = (2,17) precedence: __ > activate = u = n__u > e > o > n__e > i > a > n____ = U91# > n__a > isPalListKind = tt = n__nil = n__i = n__o > isPalListKind# > U92 = U91 > nil partial status: pi(isPalListKind#) = [1] pi(n____) = [] pi(U91#) = [] pi(isPalListKind) = [] pi(activate) = [1] pi(tt) = [] pi(U92) = [] pi(__) = [] pi(nil) = [] pi(U91) = [] pi(n__nil) = [] pi(a) = [] pi(n__a) = [] pi(e) = [] pi(n__e) = [] pi(i) = [] pi(n__i) = [] pi(o) = [] pi(n__o) = [] pi(u) = [] pi(n__u) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U91#(tt(),V2) -> isPalListKind#(activate(V2)) p2: isPalListKind#(n____(V1,V2)) -> isPalListKind#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPalListKind#(n____(V1,V2)) -> isPalListKind#(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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: isPalListKind#_A(x1) = x1 + (1,2) n_____A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (4,3) activate_A(x1) = x1 + (2,2) ___A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (5,5) nil_A() = (2,2) n__nil_A() = (1,1) a_A() = (2,0) n__a_A() = (1,1) e_A() = (2,2) n__e_A() = (1,1) i_A() = (2,2) n__i_A() = (1,1) o_A() = (2,2) n__o_A() = (1,1) u_A() = (1,1) n__u_A() = (1,1) precedence: n____ = activate = __ > isPalListKind# = n__nil = a = e = n__i > i > n__a = o > nil = n__o > n__e = u = n__u partial status: pi(isPalListKind#) = [1] pi(n____) = [] pi(activate) = [] 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 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(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r63 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: __#_A(x1,x2) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x2 + (1,1) ___A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (2,0) nil_A() = (1,1) n_____A(x1,x2) = (1,0) precedence: __ > __# = nil = n____ partial status: pi(__#) = [1] pi(__) = [] pi(nil) = [] pi(n____) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V)) r5: U12(tt(),V) -> U13(isNeList(activate(V))) r6: U13(tt()) -> tt() r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) r11: U25(tt(),V2) -> U26(isList(activate(V2))) r12: U26(tt()) -> tt() r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) r14: U32(tt(),V) -> U33(isQid(activate(V))) r15: U33(tt()) -> tt() r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) r20: U45(tt(),V2) -> U46(isNeList(activate(V2))) r21: U46(tt()) -> tt() r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) r26: U55(tt(),V2) -> U56(isList(activate(V2))) r27: U56(tt()) -> tt() r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) r29: U62(tt(),V) -> U63(isQid(activate(V))) r30: U63(tt()) -> tt() r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) r33: U73(tt(),P) -> U74(isPalListKind(activate(P))) r34: U74(tt()) -> tt() r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) r36: U82(tt(),V) -> U83(isNePal(activate(V))) r37: U83(tt()) -> tt() r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2))) r39: U92(tt()) -> tt() r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) r41: isList(n__nil()) -> tt() r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) r47: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V)) r49: isPal(n__nil()) -> tt() r50: isPalListKind(n__a()) -> tt() r51: isPalListKind(n__e()) -> tt() r52: isPalListKind(n__i()) -> tt() r53: isPalListKind(n__nil()) -> tt() r54: isPalListKind(n__o()) -> tt() r55: isPalListKind(n__u()) -> tt() r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2)) r57: isQid(n__a()) -> tt() r58: isQid(n__e()) -> tt() r59: isQid(n__i()) -> tt() r60: isQid(n__o()) -> tt() r61: isQid(n__u()) -> tt() r62: nil() -> n__nil() r63: __(X1,X2) -> n____(X1,X2) r64: a() -> n__a() r65: e() -> n__e() r66: i() -> n__i() r67: o() -> n__o() r68: u() -> n__u() r69: activate(n__nil()) -> nil() r70: activate(n____(X1,X2)) -> __(X1,X2) r71: activate(n__a()) -> a() r72: activate(n__e()) -> e() r73: activate(n__i()) -> i() r74: activate(n__o()) -> o() r75: activate(n__u()) -> u() r76: activate(X) -> X The set of usable rules consists of r1, r2, r3, r63 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: __#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (1,2) ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,1) nil_A() = (1,1) n_____A(x1,x2) = (1,2) precedence: __# = __ = n____ > nil partial status: pi(__#) = [] pi(__) = [] pi(nil) = [] pi(n____) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.