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: max/plus interpretations on natural numbers: U82#_A(x1,x2) = max{661, x1 - 154, x2 + 292} tt_A = 663 isNePal#_A(x1) = max{660, x1 + 255} activate_A(x1) = max{220, x1 + 36} n_____A(x1,x2) = max{x1 + 226, x2 - 20} ___A(x1,x2) = max{253, x1 + 240, x2} U71#_A(x1,x2,x3) = max{482, x1 + 5, x2 - 3, x3 + 439} isQid_A(x1) = max{234, x1 + 7} U72#_A(x1,x2) = max{664, x1 - 486, x2 + 403} isPalListKind_A(x1) = max{664, x1 + 447} isPal#_A(x1) = max{663, x1 + 366} U81#_A(x1,x2) = max{662, x1 - 443, x2 + 329} U92_A(x1) = max{669, x1 - 669} nil_A = 221 U91_A(x1,x2) = max{668, x1 + 6, x2 - 1} n__nil_A = 221 a_A = 665 n__a_A = 664 e_A = 665 n__e_A = 664 i_A = 665 n__i_A = 664 o_A = 658 n__o_A = 657 u_A = 665 n__u_A = 664 precedence: isPalListKind = U92 = U91 > isNePal# > U71# = o > tt = activate = __ > n____ = U72# = e = n__o > isPal# = U81# = a = n__a = n__u > U82# > i = n__i = u > isQid = nil = n__e > n__nil partial status: pi(U82#) = [] pi(tt) = [] pi(isNePal#) = [] pi(activate) = [1] pi(n____) = [] pi(__) = [1, 2] pi(U71#) = [] pi(isQid) = [1] 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: p6 We remove them from the problem. -- SCC decomposition. 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)) 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: max/plus interpretations on natural numbers: U52#_A(x1,x2,x3) = max{286, x2 + 217, x3 - 131} tt_A = 576 U53#_A(x1,x2,x3) = max{286, x2 + 148, x3 - 131} isPalListKind_A(x1) = max{603, x1 + 486} activate_A(x1) = max{68, x1} U54#_A(x1,x2,x3) = max{11, x2 - 131, x3 - 131} isNeList#_A(x1) = max{0, x1 - 131} n_____A(x1,x2) = max{684, x1 + 485, x2} U51#_A(x1,x2,x3) = max{286, x1 - 735, x2 + 285, x3 - 131} U41#_A(x1,x2,x3) = max{x1 - 250, x2 + 287, x3 - 131} U42#_A(x1,x2,x3) = max{x1 - 552, x2 + 218, x3 - 131} U43#_A(x1,x2,x3) = max{6, x1 - 617, x2 - 43, x3 - 131} U44#_A(x1,x2,x3) = max{6, x2 - 62, x3 - 131} isList#_A(x1) = max{0, x1 - 131} U21#_A(x1,x2,x3) = max{x1 - 758, x2 + 286, x3 - 131} U22#_A(x1,x2,x3) = max{x1 - 735, x2 + 217, x3 - 131} U23#_A(x1,x2,x3) = max{x2 + 148, x3 - 131} U24#_A(x1,x2,x3) = max{x2 + 79, x3 - 131} U11#_A(x1,x2) = max{0, x2 - 131} U12#_A(x1,x2) = max{0, x1 - 735, x2 - 131} U25#_A(x1,x2) = max{x1 + 9, x2 - 131} isList_A(x1) = max{69, x1 - 72} U45#_A(x1,x2) = max{6, x1 - 640, x2 - 131} U55#_A(x1,x2) = max{0, x2 - 131} isNeList_A(x1) = max{12, x1 - 76} U26_A(x1) = 576 U46_A(x1) = 579 U56_A(x1) = 577 U25_A(x1,x2) = 577 U45_A(x1,x2) = max{578, x1 + 71} U55_A(x1,x2) = 578 U24_A(x1,x2,x3) = 578 U44_A(x1,x2,x3) = max{579, x2 - 1} U54_A(x1,x2,x3) = 605 U13_A(x1) = max{15, x1 + 1} U23_A(x1,x2,x3) = 578 U33_A(x1) = x1 + 1 U43_A(x1,x2,x3) = max{608, x2 - 1} U53_A(x1,x2,x3) = 606 isQid_A(x1) = max{1, x1 - 284} n__a_A = 861 n__e_A = 861 n__i_A = 861 n__o_A = 861 n__u_A = 861 U12_A(x1,x2) = max{14, x1 - 560, x2 - 74} U22_A(x1,x2,x3) = 579 U32_A(x1,x2) = max{2, x1 - 749, x2 - 214} U42_A(x1,x2,x3) = max{608, x2 - 1} U52_A(x1,x2,x3) = max{607, x2} U92_A(x1) = max{604, x1 - 186} ___A(x1,x2) = max{684, x1 + 485, x2} nil_A = 648 U11_A(x1,x2) = max{69, x1 - 558, x2 - 73} U21_A(x1,x2,x3) = 579 U31_A(x1,x2) = max{12, x1 - 680, x2 - 145} U41_A(x1,x2,x3) = max{608, x2 - 1} U51_A(x1,x2,x3) = max{608, x1 - 680, x2 + 409} U91_A(x1,x2) = max{604, x1 - 509, x2 + 418} n__nil_A = 648 a_A = 861 e_A = 861 i_A = 861 o_A = 861 u_A = 861 precedence: U52# = tt = U53# = isPalListKind = activate = U54# = isNeList# = n____ = U51# = U41# = U42# = U43# = U44# = isList# = U21# = U22# = U23# = U24# = U11# = U12# = U25# = isList = U45# = U55# = isNeList = U26 = U46 = U56 = U25 = U45 = U55 = U24 = U44 = U54 = U13 = U23 = U33 = U43 = U53 = isQid = n__a = n__e = n__i = n__o = n__u = U12 = U22 = U32 = U42 = U52 = U92 = __ = nil = U11 = U21 = U31 = U41 = U51 = U91 = n__nil = a = e = i = o = u partial status: pi(U52#) = [] pi(tt) = [] pi(U53#) = [] pi(isPalListKind) = [] pi(activate) = [] pi(U54#) = [] pi(isNeList#) = [] pi(n____) = [] pi(U51#) = [] pi(U41#) = [] pi(U42#) = [] pi(U43#) = [] 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) = [] 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: p10 We remove them from the problem. -- SCC decomposition. 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: 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: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23} -- 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) -> U55#(isNeList(activate(V1)),activate(V2)) p4: U55#(tt(),V2) -> isList#(activate(V2)) p5: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p6: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p7: U12#(tt(),V) -> isNeList#(activate(V)) p8: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p9: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p10: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p11: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p12: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p13: U45#(tt(),V2) -> isNeList#(activate(V2)) p14: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p15: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p16: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p17: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p18: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p19: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p20: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p21: U25#(tt(),V2) -> isList#(activate(V2)) p22: U24#(tt(),V1,V2) -> isList#(activate(V1)) p23: U54#(tt(),V1,V2) -> isNeList#(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: max/plus interpretations on natural numbers: U52#_A(x1,x2,x3) = max{x1 - 151, x2 + 515, x3} tt_A = 184 U53#_A(x1,x2,x3) = max{x1 - 158, x2 + 482, x3} isPalListKind_A(x1) = max{173, x1 + 157} activate_A(x1) = max{32, x1} U54#_A(x1,x2,x3) = max{x2 + 449, x3} U55#_A(x1,x2) = max{x1 - 135, x2} isNeList_A(x1) = max{583, x1 + 394} isList#_A(x1) = max{48, x1} U11#_A(x1,x2) = max{48, x2} U12#_A(x1,x2) = max{47, x2} isNeList#_A(x1) = max{47, x1} n_____A(x1,x2) = max{581, x1 + 549, x2} U41#_A(x1,x2,x3) = max{x1 - 174, x2 + 517, x3} U42#_A(x1,x2,x3) = max{x1 - 180, x2 + 289, x3} U43#_A(x1,x2,x3) = max{x1 - 170, x2 + 256, x3} U44#_A(x1,x2,x3) = max{255, x1 - 158, x2 + 85, x3} U45#_A(x1,x2) = max{x1 - 137, x2} isList_A(x1) = x1 + 222 U51#_A(x1,x2,x3) = max{x1 - 190, x2 + 548, x3} U21#_A(x1,x2,x3) = max{x1 + 391, x2 + 253, x3} U22#_A(x1,x2,x3) = max{x1 + 4, x2 + 222, x3} U23#_A(x1,x2,x3) = max{x1 - 171, x2 + 190, x3} U24#_A(x1,x2,x3) = max{x2 + 50, x3} U25#_A(x1,x2) = max{49, x2} U26_A(x1) = 185 U46_A(x1) = max{185, x1 - 396} U56_A(x1) = 255 U25_A(x1,x2) = 198 U45_A(x1,x2) = max{186, x1 + 33, x2 - 1} U55_A(x1,x2) = x2 + 255 U24_A(x1,x2,x3) = 198 U44_A(x1,x2,x3) = max{x2 + 255, x3 + 288} U54_A(x1,x2,x3) = max{x1 + 103, x3 + 255} U13_A(x1) = 185 U23_A(x1,x2,x3) = 199 U33_A(x1) = x1 + 35 U43_A(x1,x2,x3) = max{360, x2 + 327, x3 + 288} U53_A(x1,x2,x3) = x3 + 293 isQid_A(x1) = max{189, x1 + 155} n__a_A = 185 n__e_A = 28 n__i_A = 30 n__o_A = 30 n__u_A = 185 U12_A(x1,x2) = max{211, x1 + 27} U22_A(x1,x2,x3) = max{223, x1 - 229, x3 - 79} U32_A(x1,x2) = max{223, x1 + 40, x2 + 190} U42_A(x1,x2,x3) = max{360, x1 + 127, x2 + 327, x3 + 288} U52_A(x1,x2,x3) = max{x1 + 143, x2 + 300, x3 + 293} U92_A(x1) = max{184, x1 - 190} ___A(x1,x2) = max{581, x1 + 549, x2} nil_A = 31 U11_A(x1,x2) = max{222, x1 + 33, x2 + 190} U21_A(x1,x2,x3) = max{803, x1 - 190, x2 - 39, x3 + 222} U31_A(x1,x2) = max{583, x1 + 237, x2 + 230} U41_A(x1,x2,x3) = max{x1 + 177, x2 + 910, x3 + 361} U51_A(x1,x2,x3) = max{x1 - 182, x2 + 550, x3 + 333} U91_A(x1,x2) = max{x1 + 359, x2 + 124} n__nil_A = 30 a_A = 185 e_A = 29 i_A = 31 o_A = 31 u_A = 185 precedence: U54 = n__o > n__i > n____ = __ > U41# > U52 > U51# > U52# > U42# > U43# > U23 = U22 > U44# > isList = n__a = a > U32 > U24 = U33 = U12 = U51 > U53# > U54# > U45# > U55# > U21# > U22# > U23# > U24# > U25# > isList# > U11# > U12# > activate > nil > n__u = u > U21 > U55 > U56 > U53 > U25 > isNeList = isNeList# > isPalListKind = U41 = n__nil > isQid > U13 > U26 = U43 = U42 = i > U44 > U31 = U91 = o > U46 = U45 = U92 = U11 > tt > n__e = e partial status: pi(U52#) = [3] pi(tt) = [] pi(U53#) = [3] pi(isPalListKind) = [] pi(activate) = [1] pi(U54#) = [2, 3] pi(U55#) = [2] pi(isNeList) = [1] pi(isList#) = [1] pi(U11#) = [2] pi(U12#) = [2] pi(isNeList#) = [1] pi(n____) = [1, 2] pi(U41#) = [2, 3] pi(U42#) = [3] pi(U43#) = [3] pi(U44#) = [3] pi(U45#) = [2] pi(isList) = [] pi(U51#) = [2, 3] pi(U21#) = [1, 2, 3] pi(U22#) = [2, 3] pi(U23#) = [2, 3] pi(U24#) = [3] pi(U25#) = [2] pi(U26) = [] pi(U46) = [] pi(U56) = [] pi(U25) = [] pi(U45) = [] pi(U55) = [] pi(U24) = [] pi(U44) = [3] pi(U54) = [3] pi(U13) = [] pi(U23) = [] pi(U33) = [] pi(U43) = [] pi(U53) = [] pi(isQid) = [1] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U42) = [2, 3] pi(U52) = [3] pi(U92) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [2] 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) -> U55#(isNeList(activate(V1)),activate(V2)) p3: U55#(tt(),V2) -> isList#(activate(V2)) p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V)) p5: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V)) p6: U12#(tt(),V) -> isNeList#(activate(V)) p7: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p8: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p9: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p10: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p11: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2)) p12: U45#(tt(),V2) -> isNeList#(activate(V2)) p13: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p14: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p15: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p16: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p17: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p18: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p19: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2)) p20: U25#(tt(),V2) -> isList#(activate(V2)) p21: U24#(tt(),V1,V2) -> isList#(activate(V1)) p22: U54#(tt(),V1,V2) -> isNeList#(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: {p15, p16, p17, p18, p19, p20, p21} {p7, p8, p9, p10, p11, p12} -- 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: max/plus interpretations on natural numbers: U25#_A(x1,x2) = max{x1 - 61, x2 + 57} tt_A = 63 isList#_A(x1) = x1 + 57 activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 130, x2} U21#_A(x1,x2,x3) = max{x1 - 46, x2 + 186, x3 + 57} isPalListKind_A(x1) = x1 + 70 U22#_A(x1,x2,x3) = max{x1 - 30, x2 + 59, x3 + 57} U23#_A(x1,x2,x3) = max{x1 - 14, x2 + 59, x3 + 57} U24#_A(x1,x2,x3) = max{x1 - 64, x2 + 59, x3 + 57} isList_A(x1) = x1 + 119 U46_A(x1) = 69 U56_A(x1) = 64 U45_A(x1,x2) = max{68, x1 + 6} isNeList_A(x1) = x1 + 221 U55_A(x1,x2) = 65 U44_A(x1,x2,x3) = max{127, x2 + 125} U54_A(x1,x2,x3) = 66 U26_A(x1) = 64 U33_A(x1) = x1 + 68 U43_A(x1,x2,x3) = max{128, x1 - 80, x2 + 126, x3 - 10} U53_A(x1,x2,x3) = 67 isQid_A(x1) = 66 n__a_A = 66 n__e_A = 1 n__i_A = 62 n__o_A = 64 n__u_A = 1 U25_A(x1,x2) = x2 + 65 U32_A(x1,x2) = x1 + 86 U42_A(x1,x2,x3) = max{129, x1 - 96, x2 + 126, x3 - 9} U52_A(x1,x2,x3) = max{68, x2 - 21} U24_A(x1,x2,x3) = max{x1 - 69, x3 + 65} U31_A(x1,x2) = max{x1 + 94, x2 + 221} U41_A(x1,x2,x3) = max{131, x1 - 71, x2 + 127, x3} U51_A(x1,x2,x3) = max{47, x1 + 5, x2 + 4} U13_A(x1) = max{75, x1 - 223} U23_A(x1,x2,x3) = max{x1 + 8, x3 + 117} U12_A(x1,x2) = max{75, x2 - 2} U22_A(x1,x2,x3) = max{x1 - 79, x3 + 119} U92_A(x1) = 86 ___A(x1,x2) = max{x1 + 130, x2} nil_A = 64 U11_A(x1,x2) = max{x1 + 12, x2 - 1} U21_A(x1,x2,x3) = max{133, x1 - 71, x2 + 131, x3 + 119} U91_A(x1,x2) = max{24, x1 + 23} n__nil_A = 64 a_A = 66 e_A = 1 i_A = 62 o_A = 64 u_A = 1 precedence: isPalListKind = U32 > isQid > n__o = o > U54 = n__u = u > tt = U56 = U55 = U33 = nil = n__nil > n____ = isList = __ > activate > isNeList > U53 = U42 = U52 = U41 = U51 = U21 > U45 = U44 = U43 > U26 = U25 = U24 > U46 > U31 > U91 = e > U25# = isList# = U21# = U22# = U23# = U24# = n__a = n__e = n__i = U13 = U23 = U12 = U22 = U92 = U11 = a = i partial status: pi(U25#) = [] pi(tt) = [] pi(isList#) = [] pi(activate) = [1] pi(n____) = [1, 2] pi(U21#) = [] pi(isPalListKind) = [1] pi(U22#) = [] pi(U23#) = [] pi(U24#) = [] pi(isList) = [1] pi(U46) = [] pi(U56) = [] pi(U45) = [] pi(isNeList) = [1] pi(U55) = [] pi(U44) = [] pi(U54) = [] pi(U26) = [] pi(U33) = [1] 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) = [1] pi(U13) = [] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [3] pi(U91) = [1] pi(n__nil) = [] pi(a) = [] pi(e) = [] pi(i) = [] pi(o) = [] pi(u) = [] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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) -> 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: {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) -> 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: max/plus interpretations on natural numbers: U25#_A(x1,x2) = max{104, x1 - 37, x2} tt_A = 36 isList#_A(x1) = x1 activate_A(x1) = x1 n_____A(x1,x2) = max{x1 + 138, x2} U21#_A(x1,x2,x3) = max{x1 + 1, x2 + 127, x3} isPalListKind_A(x1) = max{15, x1 - 101} U22#_A(x1,x2,x3) = max{x1 + 23, x2 + 107, x3} U23#_A(x1,x2,x3) = max{x1 + 45, x2 + 106, x3} U24#_A(x1,x2,x3) = max{x1 + 67, x2 + 105, x3} isList_A(x1) = max{141, x1 + 13} U46_A(x1) = 37 U56_A(x1) = 36 U45_A(x1,x2) = x2 + 37 isNeList_A(x1) = x1 + 258 U55_A(x1,x2) = 36 U44_A(x1,x2,x3) = x3 + 38 U54_A(x1,x2,x3) = max{12, x1, x2 - 103, x3 - 105} U26_A(x1) = max{37, x1 - 143} U33_A(x1) = max{52, x1 + 1} U43_A(x1,x2,x3) = max{x2 - 102, x3 + 39} U53_A(x1,x2,x3) = max{13, x1 + 2, x2 - 102, x3 - 100} isQid_A(x1) = x1 + 35 n__a_A = 137 n__e_A = 137 n__i_A = 138 n__o_A = 137 n__u_A = 137 U25_A(x1,x2) = max{9, x1 + 1, x2 - 1} U32_A(x1,x2) = max{x1 + 17, x2 + 51} U42_A(x1,x2,x3) = max{x2 + 17, x3 + 53} U52_A(x1,x2,x3) = max{18, x1 - 22, x2 + 1, x3 - 99} U24_A(x1,x2,x3) = max{x1 + 107, x2 + 15, x3 + 10} U31_A(x1,x2) = max{x1 - 3, x2 + 258} U41_A(x1,x2,x3) = max{x1 - 1, x2 + 255, x3 + 255} U51_A(x1,x2,x3) = max{x2 + 139, x3 + 257} U13_A(x1) = 37 U23_A(x1,x2,x3) = max{x1 + 113, x2 + 123, x3 + 11} U12_A(x1,x2) = 150 U22_A(x1,x2,x3) = max{161, x2 + 124, x3 + 12} U92_A(x1) = 37 ___A(x1,x2) = max{x1 + 138, x2} nil_A = 138 U11_A(x1,x2) = x1 + 114 U21_A(x1,x2,x3) = max{x1 + 125, x2 + 139, x3 + 12} U91_A(x1,x2) = max{37, x1 - 115} n__nil_A = 138 a_A = 137 e_A = 137 i_A = 138 o_A = 137 u_A = 137 precedence: U41 > U43 > isPalListKind = U45 = isNeList = U44 = U51 > U42 = U52 > n____ = isList = isQid = __ = nil = n__nil > U21# > U22# > U23# > U24# = n__e = n__i = e = i > U25# > activate = n__o = o > U26 = n__a = U25 = U24 = U13 = U23 = U12 = U22 = U92 = U11 = U21 = U91 = a > U33 = n__u = U32 = U31 = u > isList# > U56 = U55 = U54 = U53 > U46 > tt partial status: pi(U25#) = [2] pi(tt) = [] pi(isList#) = [1] pi(activate) = [1] pi(n____) = [1, 2] pi(U21#) = [1, 3] pi(isPalListKind) = [] pi(U22#) = [3] pi(U23#) = [3] pi(U24#) = [3] pi(isList) = [] pi(U46) = [] pi(U56) = [] pi(U45) = [] pi(isNeList) = [1] pi(U55) = [] pi(U44) = [] pi(U54) = [] pi(U26) = [] pi(U33) = [] pi(U43) = [3] pi(U53) = [] pi(isQid) = [] pi(n__a) = [] pi(n__e) = [] pi(n__i) = [] pi(n__o) = [] pi(n__u) = [] pi(U25) = [] pi(U32) = [2] pi(U42) = [3] pi(U52) = [] pi(U24) = [] pi(U31) = [] pi(U41) = [] pi(U51) = [2, 3] pi(U13) = [] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [1, 2] pi(nil) = [] pi(U11) = [] pi(U21) = [3] 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: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p2: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2)) p3: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p4: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2)) p5: 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: 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)) p6: U45#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(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: max/plus interpretations on natural numbers: isNeList#_A(x1) = max{4, x1} n_____A(x1,x2) = max{575, x1 + 563, x2} U41#_A(x1,x2,x3) = max{x1, x2 + 243, x3} isPalListKind_A(x1) = 243 activate_A(x1) = max{12, x1} tt_A = 202 U42#_A(x1,x2,x3) = max{x1 - 21, x2 + 231, x3} U43#_A(x1,x2,x3) = max{x1 - 26, x2 + 3, x3} U44#_A(x1,x2,x3) = max{2, x1 - 190, x2 - 13, x3} U45#_A(x1,x2) = max{3, x1 - 190, x2} isList_A(x1) = x1 + 176 U46_A(x1) = 203 U56_A(x1) = 398 U45_A(x1,x2) = max{203, x1 - 196} isNeList_A(x1) = max{44, x1 - 5} U55_A(x1,x2) = max{204, x1 + 197} U44_A(x1,x2,x3) = max{x1 - 268, x2 + 203} U54_A(x1,x2,x3) = max{242, x2 + 205, x3 - 21} U26_A(x1) = 434 U33_A(x1) = max{3, x1 + 1} U43_A(x1,x2,x3) = max{244, x2 + 204} U53_A(x1,x2,x3) = max{x1 - 263, x2 + 243, x3 - 20} isQid_A(x1) = max{1, x1 - 33} n__a_A = 236 n__e_A = 236 n__i_A = 236 n__o_A = 236 n__u_A = 236 U25_A(x1,x2) = max{435, x1 + 245} U32_A(x1,x2) = max{3, x2 - 19} U42_A(x1,x2,x3) = max{244, x2 + 205} U52_A(x1,x2,x3) = max{x1 + 1, x2 + 255, x3 - 19} U24_A(x1,x2,x3) = max{x1 + 232, x2 + 465} U31_A(x1,x2) = max{1, x1 - 199, x2 - 18} U41_A(x1,x2,x3) = max{564, x1 + 16, x2 + 216} U51_A(x1,x2,x3) = max{x1 + 66, x2 + 552, x3 - 6} U13_A(x1) = max{46, x1 + 2} U23_A(x1,x2,x3) = max{x1 + 276, x2 + 476} U12_A(x1,x2) = max{45, x1 - 155, x2 - 2} U22_A(x1,x2,x3) = max{x1 + 318, x2 + 520} U92_A(x1) = max{203, x1 - 14} ___A(x1,x2) = max{575, x1 + 563, x2} nil_A = 27 U11_A(x1,x2) = max{28, x1 - 113, x2 - 1} U21_A(x1,x2,x3) = max{x1 - 68, x2 + 562} U91_A(x1,x2) = max{243, x1 - 11} n__nil_A = 27 a_A = 236 e_A = 236 i_A = 236 o_A = 236 u_A = 236 precedence: U53 = U52 > U26 > U56 > tt = isNeList = U33 = isQid = U32 = U31 = U51 > U46 = U45 = U44 = U43 = U42 > U54 > U55 > U21 > U22 > U23 > n__o = U24 = o > n____ = __ > U41# > U42# > U43# > U44# > U45# > U41 > n__i = i > isPalListKind = n__e = U25 = U92 = e > isNeList# > isList > U12 = U11 > U13 > n__u = u > U91 > nil = n__nil > activate = n__a = a partial status: pi(isNeList#) = [1] pi(n____) = [1, 2] pi(U41#) = [1, 3] pi(isPalListKind) = [] pi(activate) = [1] pi(tt) = [] pi(U42#) = [3] pi(U43#) = [3] pi(U44#) = [3] pi(U45#) = [2] 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) = [2] pi(U24) = [2] pi(U31) = [] pi(U41) = [1, 2] pi(U51) = [] pi(U13) = [1] pi(U23) = [] pi(U12) = [] pi(U22) = [] pi(U92) = [] pi(__) = [1, 2] 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: 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: U45#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt(),V) -> U12(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: max/plus interpretations on natural numbers: isPalListKind#_A(x1) = x1 + 20 n_____A(x1,x2) = max{x1 + 25, x2} U91#_A(x1,x2) = max{26, x1 - 9, x2 + 20} isPalListKind_A(x1) = x1 + 40 activate_A(x1) = max{2, x1} tt_A = 36 U92_A(x1) = max{37, x1 - 10} ___A(x1,x2) = max{x1 + 25, x2} nil_A = 37 U91_A(x1,x2) = max{x1 - 3, x2 + 37} n__nil_A = 37 a_A = 3 n__a_A = 3 e_A = 3 n__e_A = 3 i_A = 3 n__i_A = 3 o_A = 37 n__o_A = 37 u_A = 1 n__u_A = 0 precedence: isPalListKind# = U91# = activate > isPalListKind > n____ = tt = U92 = __ = nil = U91 = n__nil = a = e = n__e = i = n__i > n__a = o = n__o = u = n__u partial status: pi(isPalListKind#) = [] pi(n____) = [1, 2] pi(U91#) = [] pi(isPalListKind) = [1] pi(activate) = [1] pi(tt) = [] pi(U92) = [] pi(__) = [1, 2] 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: p3 We remove them from the problem. -- SCC decomposition. 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)) 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, p2} -- 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)) 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: max/plus interpretations on natural numbers: isPalListKind#_A(x1) = x1 n_____A(x1,x2) = max{x1 + 11, x2} U91#_A(x1,x2) = max{11, x1 + 1, x2} isPalListKind_A(x1) = max{9, x1 + 5} activate_A(x1) = max{2, x1} tt_A = 4 U92_A(x1) = max{5, x1 - 14} ___A(x1,x2) = max{x1 + 11, x2} nil_A = 3 U91_A(x1,x2) = max{16, x1 - 8, x2 - 3} n__nil_A = 3 a_A = 1 n__a_A = 0 e_A = 3 n__e_A = 3 i_A = 1 n__i_A = 0 o_A = 3 n__o_A = 3 u_A = 1 n__u_A = 1 precedence: o = n__o = u > isPalListKind = tt = U92 = n__u > n____ = __ > U91# > isPalListKind# = activate = nil = U91 = n__nil = a = n__a = e = n__e = i = n__i partial status: pi(isPalListKind#) = [1] pi(n____) = [1, 2] pi(U91#) = [1, 2] pi(isPalListKind) = [1] pi(activate) = [1] pi(tt) = [] pi(U92) = [] pi(__) = [1, 2] 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: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isPalListKind#(n____(V1,V2)) -> U91#(isPalListKind(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: __#(__(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: max/plus interpretations on natural numbers: __#_A(x1,x2) = max{0, x1 - 5} ___A(x1,x2) = max{6, x1 + 4, x2} nil_A = 0 n_____A(x1,x2) = max{x1 + 1, x2} precedence: __# = __ = nil = n____ partial status: pi(__#) = [] pi(__) = [1, 2] pi(nil) = [] pi(n____) = [1] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(Y,Z) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: 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) -> __#(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 (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: __#_A(x1,x2) = max{x1 + 1, x2 + 1} ___A(x1,x2) = x2 precedence: __# = __ partial status: pi(__#) = [1] pi(__) = [2] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.