YES We show the termination of the TRS R: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__U11(tt(),V) -> a__U12(a__isNeList(V)) a__U12(tt()) -> tt() a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) a__U22(tt(),V2) -> a__U23(a__isList(V2)) a__U23(tt()) -> tt() a__U31(tt(),V) -> a__U32(a__isQid(V)) a__U32(tt()) -> tt() a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) a__U43(tt()) -> tt() a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) a__U52(tt(),V2) -> a__U53(a__isList(V2)) a__U53(tt()) -> tt() a__U61(tt(),V) -> a__U62(a__isQid(V)) a__U62(tt()) -> tt() a__U71(tt(),V) -> a__U72(a__isNePal(V)) a__U72(tt()) -> tt() a__and(tt(),X) -> mark(X) a__isList(V) -> a__U11(a__isPalListKind(V),V) a__isList(nil()) -> tt() a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) a__isNeList(V) -> a__U31(a__isPalListKind(V),V) a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) a__isNePal(V) -> a__U61(a__isPalListKind(V),V) a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) a__isPal(V) -> a__U71(a__isPalListKind(V),V) a__isPal(nil()) -> tt() a__isPalListKind(a()) -> tt() a__isPalListKind(e()) -> tt() a__isPalListKind(i()) -> tt() a__isPalListKind(nil()) -> tt() a__isPalListKind(o()) -> tt() a__isPalListKind(u()) -> tt() a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U12(X)) -> a__U12(mark(X)) mark(isNeList(X)) -> a__isNeList(X) mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) mark(U22(X1,X2)) -> a__U22(mark(X1),X2) mark(isList(X)) -> a__isList(X) mark(U23(X)) -> a__U23(mark(X)) mark(U31(X1,X2)) -> a__U31(mark(X1),X2) mark(U32(X)) -> a__U32(mark(X)) mark(isQid(X)) -> a__isQid(X) mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) mark(U42(X1,X2)) -> a__U42(mark(X1),X2) mark(U43(X)) -> a__U43(mark(X)) mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) mark(U52(X1,X2)) -> a__U52(mark(X1),X2) mark(U53(X)) -> a__U53(mark(X)) mark(U61(X1,X2)) -> a__U61(mark(X1),X2) mark(U62(X)) -> a__U62(mark(X)) mark(U71(X1,X2)) -> a__U71(mark(X1),X2) mark(U72(X)) -> a__U72(mark(X)) mark(isNePal(X)) -> a__isNePal(X) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isPalListKind(X)) -> a__isPalListKind(X) mark(isPal(X)) -> a__isPal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a____(X1,X2) -> __(X1,X2) a__U11(X1,X2) -> U11(X1,X2) a__U12(X) -> U12(X) a__isNeList(X) -> isNeList(X) a__U21(X1,X2,X3) -> U21(X1,X2,X3) a__U22(X1,X2) -> U22(X1,X2) a__isList(X) -> isList(X) a__U23(X) -> U23(X) a__U31(X1,X2) -> U31(X1,X2) a__U32(X) -> U32(X) a__isQid(X) -> isQid(X) a__U41(X1,X2,X3) -> U41(X1,X2,X3) a__U42(X1,X2) -> U42(X1,X2) a__U43(X) -> U43(X) a__U51(X1,X2,X3) -> U51(X1,X2,X3) a__U52(X1,X2) -> U52(X1,X2) a__U53(X) -> U53(X) a__U61(X1,X2) -> U61(X1,X2) a__U62(X) -> U62(X) a__U71(X1,X2) -> U71(X1,X2) a__U72(X) -> U72(X) a__isNePal(X) -> isNePal(X) a__and(X1,X2) -> and(X1,X2) a__isPalListKind(X) -> isPalListKind(X) a__isPal(X) -> isPal(X) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z))) p2: a____#(__(X,Y),Z) -> mark#(X) p3: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z)) p4: a____#(__(X,Y),Z) -> mark#(Y) p5: a____#(__(X,Y),Z) -> mark#(Z) p6: a____#(X,nil()) -> mark#(X) p7: a____#(nil(),X) -> mark#(X) p8: a__U11#(tt(),V) -> a__U12#(a__isNeList(V)) p9: a__U11#(tt(),V) -> a__isNeList#(V) p10: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p11: a__U21#(tt(),V1,V2) -> a__isList#(V1) p12: a__U22#(tt(),V2) -> a__U23#(a__isList(V2)) p13: a__U22#(tt(),V2) -> a__isList#(V2) p14: a__U31#(tt(),V) -> a__U32#(a__isQid(V)) p15: a__U31#(tt(),V) -> a__isQid#(V) p16: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) p17: a__U41#(tt(),V1,V2) -> a__isList#(V1) p18: a__U42#(tt(),V2) -> a__U43#(a__isNeList(V2)) p19: a__U42#(tt(),V2) -> a__isNeList#(V2) p20: a__U51#(tt(),V1,V2) -> a__U52#(a__isNeList(V1),V2) p21: a__U51#(tt(),V1,V2) -> a__isNeList#(V1) p22: a__U52#(tt(),V2) -> a__U53#(a__isList(V2)) p23: a__U52#(tt(),V2) -> a__isList#(V2) p24: a__U61#(tt(),V) -> a__U62#(a__isQid(V)) p25: a__U61#(tt(),V) -> a__isQid#(V) p26: a__U71#(tt(),V) -> a__U72#(a__isNePal(V)) p27: a__U71#(tt(),V) -> a__isNePal#(V) p28: a__and#(tt(),X) -> mark#(X) p29: a__isList#(V) -> a__U11#(a__isPalListKind(V),V) p30: a__isList#(V) -> a__isPalListKind#(V) p31: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p32: a__isList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p33: a__isList#(__(V1,V2)) -> a__isPalListKind#(V1) p34: a__isNeList#(V) -> a__U31#(a__isPalListKind(V),V) p35: a__isNeList#(V) -> a__isPalListKind#(V) p36: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p37: a__isNeList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p38: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1) p39: a__isNeList#(__(V1,V2)) -> a__U51#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p40: a__isNeList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p41: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1) p42: a__isNePal#(V) -> a__U61#(a__isPalListKind(V),V) p43: a__isNePal#(V) -> a__isPalListKind#(V) p44: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p45: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPalListKind(I)) p46: a__isNePal#(__(I,__(P,I))) -> a__isQid#(I) p47: a__isPal#(V) -> a__U71#(a__isPalListKind(V),V) p48: a__isPal#(V) -> a__isPalListKind#(V) p49: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p50: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p51: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2)) p52: mark#(__(X1,X2)) -> mark#(X1) p53: mark#(__(X1,X2)) -> mark#(X2) p54: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) p55: mark#(U11(X1,X2)) -> mark#(X1) p56: mark#(U12(X)) -> a__U12#(mark(X)) p57: mark#(U12(X)) -> mark#(X) p58: mark#(isNeList(X)) -> a__isNeList#(X) p59: mark#(U21(X1,X2,X3)) -> a__U21#(mark(X1),X2,X3) p60: mark#(U21(X1,X2,X3)) -> mark#(X1) p61: mark#(U22(X1,X2)) -> a__U22#(mark(X1),X2) p62: mark#(U22(X1,X2)) -> mark#(X1) p63: mark#(isList(X)) -> a__isList#(X) p64: mark#(U23(X)) -> a__U23#(mark(X)) p65: mark#(U23(X)) -> mark#(X) p66: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2) p67: mark#(U31(X1,X2)) -> mark#(X1) p68: mark#(U32(X)) -> a__U32#(mark(X)) p69: mark#(U32(X)) -> mark#(X) p70: mark#(isQid(X)) -> a__isQid#(X) p71: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3) p72: mark#(U41(X1,X2,X3)) -> mark#(X1) p73: mark#(U42(X1,X2)) -> a__U42#(mark(X1),X2) p74: mark#(U42(X1,X2)) -> mark#(X1) p75: mark#(U43(X)) -> a__U43#(mark(X)) p76: mark#(U43(X)) -> mark#(X) p77: mark#(U51(X1,X2,X3)) -> a__U51#(mark(X1),X2,X3) p78: mark#(U51(X1,X2,X3)) -> mark#(X1) p79: mark#(U52(X1,X2)) -> a__U52#(mark(X1),X2) p80: mark#(U52(X1,X2)) -> mark#(X1) p81: mark#(U53(X)) -> a__U53#(mark(X)) p82: mark#(U53(X)) -> mark#(X) p83: mark#(U61(X1,X2)) -> a__U61#(mark(X1),X2) p84: mark#(U61(X1,X2)) -> mark#(X1) p85: mark#(U62(X)) -> a__U62#(mark(X)) p86: mark#(U62(X)) -> mark#(X) p87: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p88: mark#(U71(X1,X2)) -> mark#(X1) p89: mark#(U72(X)) -> a__U72#(mark(X)) p90: mark#(U72(X)) -> mark#(X) p91: mark#(isNePal(X)) -> a__isNePal#(X) p92: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p93: mark#(and(X1,X2)) -> mark#(X1) p94: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p95: mark#(isPal(X)) -> a__isPal#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p9, p10, p11, p13, p16, p17, p19, p20, p21, p23, p27, p28, p29, p30, p31, p32, p33, p35, p36, p37, p38, p39, p40, p41, p43, p44, p45, p47, p48, p49, p50, p51, p52, p53, p54, p55, p57, p58, p59, p60, p61, p62, p63, p65, p67, p69, p71, p72, p73, p74, p76, p77, p78, p79, p80, p82, p84, p86, p87, p88, p90, p91, p92, p93, p94, p95} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z))) p2: a____#(nil(),X) -> mark#(X) p3: mark#(isPal(X)) -> a__isPal#(X) p4: a__isPal#(V) -> a__isPalListKind#(V) p5: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p6: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p9: mark#(and(X1,X2)) -> mark#(X1) p10: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p11: mark#(isNePal(X)) -> a__isNePal#(X) p12: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPalListKind(I)) p13: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p14: a__isNePal#(V) -> a__isPalListKind#(V) p15: mark#(U72(X)) -> mark#(X) p16: mark#(U71(X1,X2)) -> mark#(X1) p17: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p18: a__U71#(tt(),V) -> a__isNePal#(V) p19: mark#(U62(X)) -> mark#(X) p20: mark#(U61(X1,X2)) -> mark#(X1) p21: mark#(U53(X)) -> mark#(X) p22: mark#(U52(X1,X2)) -> mark#(X1) p23: mark#(U52(X1,X2)) -> a__U52#(mark(X1),X2) p24: a__U52#(tt(),V2) -> a__isList#(V2) p25: a__isList#(__(V1,V2)) -> a__isPalListKind#(V1) p26: a__isList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p27: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p28: a__U21#(tt(),V1,V2) -> a__isList#(V1) p29: a__isList#(V) -> a__isPalListKind#(V) p30: a__isList#(V) -> a__U11#(a__isPalListKind(V),V) p31: a__U11#(tt(),V) -> a__isNeList#(V) p32: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1) p33: a__isNeList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p34: a__isNeList#(__(V1,V2)) -> a__U51#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p35: a__U51#(tt(),V1,V2) -> a__isNeList#(V1) p36: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p37: a__U41#(tt(),V1,V2) -> a__isList#(V1) p38: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) p39: a__U42#(tt(),V2) -> a__isNeList#(V2) p40: a__isNeList#(V) -> a__isPalListKind#(V) p41: a__U51#(tt(),V1,V2) -> a__U52#(a__isNeList(V1),V2) p42: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p43: a__U22#(tt(),V2) -> a__isList#(V2) p44: mark#(U51(X1,X2,X3)) -> mark#(X1) p45: mark#(U51(X1,X2,X3)) -> a__U51#(mark(X1),X2,X3) p46: mark#(U43(X)) -> mark#(X) p47: mark#(U42(X1,X2)) -> mark#(X1) p48: mark#(U42(X1,X2)) -> a__U42#(mark(X1),X2) p49: mark#(U41(X1,X2,X3)) -> mark#(X1) p50: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3) p51: mark#(U32(X)) -> mark#(X) p52: mark#(U31(X1,X2)) -> mark#(X1) p53: mark#(U23(X)) -> mark#(X) p54: mark#(isList(X)) -> a__isList#(X) p55: mark#(U22(X1,X2)) -> mark#(X1) p56: mark#(U22(X1,X2)) -> a__U22#(mark(X1),X2) p57: mark#(U21(X1,X2,X3)) -> mark#(X1) p58: mark#(U21(X1,X2,X3)) -> a__U21#(mark(X1),X2,X3) p59: mark#(isNeList(X)) -> a__isNeList#(X) p60: mark#(U12(X)) -> mark#(X) p61: mark#(U11(X1,X2)) -> mark#(X1) p62: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) p63: mark#(__(X1,X2)) -> mark#(X2) p64: mark#(__(X1,X2)) -> mark#(X1) p65: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2)) p66: a____#(X,nil()) -> mark#(X) p67: a____#(__(X,Y),Z) -> mark#(Z) p68: a____#(__(X,Y),Z) -> mark#(Y) p69: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z)) p70: a____#(__(X,Y),Z) -> mark#(X) p71: a__isPal#(V) -> a__U71#(a__isPalListKind(V),V) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a____#_A(x1,x2) = x1 + x2 ___A(x1,x2) = x1 + x2 + 1 mark_A(x1) = x1 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 mark#_A(x1) = x1 + 1 isPal_A(x1) = 0 a__isPal#_A(x1) = 1 a__isPalListKind#_A(x1) = 1 a__and#_A(x1,x2) = x2 + 1 a__isPalListKind_A(x1) = 0 isPalListKind_A(x1) = 0 tt_A() = 0 and_A(x1,x2) = x1 + x2 isNePal_A(x1) = 0 a__isNePal#_A(x1) = 1 a__isQid_A(x1) = 0 a__and_A(x1,x2) = x1 + x2 U72_A(x1) = x1 U71_A(x1,x2) = x1 a__U71#_A(x1,x2) = 1 U62_A(x1) = x1 U61_A(x1,x2) = x1 U53_A(x1) = x1 U52_A(x1,x2) = x1 + x2 + 1 a__U52#_A(x1,x2) = 1 a__isList#_A(x1) = 1 a__U21#_A(x1,x2,x3) = 1 a__U11#_A(x1,x2) = 1 a__isNeList#_A(x1) = 1 a__U51#_A(x1,x2,x3) = 1 a__U41#_A(x1,x2,x3) = 1 a__U42#_A(x1,x2) = 1 a__isList_A(x1) = x1 + 1 a__isNeList_A(x1) = x1 a__U22#_A(x1,x2) = 1 U51_A(x1,x2,x3) = x1 + x2 + x3 + 1 U43_A(x1) = x1 U42_A(x1,x2) = x1 + x2 U41_A(x1,x2,x3) = x1 + x2 + x3 + 1 U32_A(x1) = x1 U31_A(x1,x2) = x1 + x2 U23_A(x1) = x1 isList_A(x1) = x1 + 1 U22_A(x1,x2) = x1 + x2 + 1 U21_A(x1,x2,x3) = x1 + x2 + x3 + 2 isNeList_A(x1) = x1 U12_A(x1) = x1 U11_A(x1,x2) = x1 + x2 a__U11_A(x1,x2) = x1 + x2 a__U12_A(x1) = x1 a__U21_A(x1,x2,x3) = x1 + x2 + x3 + 2 a__U22_A(x1,x2) = x1 + x2 + 1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x1 + x2 a__U32_A(x1) = x1 a__U41_A(x1,x2,x3) = x1 + x2 + x3 + 1 a__U42_A(x1,x2) = x1 + x2 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 1 a__U52_A(x1,x2) = x1 + x2 + 1 a__U53_A(x1) = x1 a__U61_A(x1,x2) = x1 a__U62_A(x1) = x1 a__U71_A(x1,x2) = x1 a__U72_A(x1) = x1 a__isNePal_A(x1) = 0 a__isPal_A(x1) = 0 a_A() = 0 e_A() = 0 i_A() = 1 o_A() = 0 u_A() = 0 isQid_A(x1) = 0 The next rules are strictly ordered: p22, p23, p44, p45, p49, p50, p54, p55, p56, p57, p58, p63, p64, p65, p69 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z))) p2: a____#(nil(),X) -> mark#(X) p3: mark#(isPal(X)) -> a__isPal#(X) p4: a__isPal#(V) -> a__isPalListKind#(V) p5: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p6: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p9: mark#(and(X1,X2)) -> mark#(X1) p10: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p11: mark#(isNePal(X)) -> a__isNePal#(X) p12: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPalListKind(I)) p13: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p14: a__isNePal#(V) -> a__isPalListKind#(V) p15: mark#(U72(X)) -> mark#(X) p16: mark#(U71(X1,X2)) -> mark#(X1) p17: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p18: a__U71#(tt(),V) -> a__isNePal#(V) p19: mark#(U62(X)) -> mark#(X) p20: mark#(U61(X1,X2)) -> mark#(X1) p21: mark#(U53(X)) -> mark#(X) p22: a__U52#(tt(),V2) -> a__isList#(V2) p23: a__isList#(__(V1,V2)) -> a__isPalListKind#(V1) p24: a__isList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p25: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p26: a__U21#(tt(),V1,V2) -> a__isList#(V1) p27: a__isList#(V) -> a__isPalListKind#(V) p28: a__isList#(V) -> a__U11#(a__isPalListKind(V),V) p29: a__U11#(tt(),V) -> a__isNeList#(V) p30: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1) p31: a__isNeList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p32: a__isNeList#(__(V1,V2)) -> a__U51#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p33: a__U51#(tt(),V1,V2) -> a__isNeList#(V1) p34: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p35: a__U41#(tt(),V1,V2) -> a__isList#(V1) p36: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) p37: a__U42#(tt(),V2) -> a__isNeList#(V2) p38: a__isNeList#(V) -> a__isPalListKind#(V) p39: a__U51#(tt(),V1,V2) -> a__U52#(a__isNeList(V1),V2) p40: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p41: a__U22#(tt(),V2) -> a__isList#(V2) p42: mark#(U43(X)) -> mark#(X) p43: mark#(U42(X1,X2)) -> mark#(X1) p44: mark#(U42(X1,X2)) -> a__U42#(mark(X1),X2) p45: mark#(U32(X)) -> mark#(X) p46: mark#(U31(X1,X2)) -> mark#(X1) p47: mark#(U23(X)) -> mark#(X) p48: mark#(isNeList(X)) -> a__isNeList#(X) p49: mark#(U12(X)) -> mark#(X) p50: mark#(U11(X1,X2)) -> mark#(X1) p51: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) p52: a____#(X,nil()) -> mark#(X) p53: a____#(__(X,Y),Z) -> mark#(Z) p54: a____#(__(X,Y),Z) -> mark#(Y) p55: a____#(__(X,Y),Z) -> mark#(X) p56: a__isPal#(V) -> a__U71#(a__isPalListKind(V),V) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1} {p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p56} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z))) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a____#_A(x1,x2) = x1 ___A(x1,x2) = x1 + x2 + 1 mark_A(x1) = x1 a_____A(x1,x2) = x1 + x2 + 1 a__U11_A(x1,x2) = x2 tt_A() = 0 a__U12_A(x1) = x1 a__isNeList_A(x1) = x1 a__U21_A(x1,x2,x3) = x2 + x3 a__U22_A(x1,x2) = x1 + x2 a__isList_A(x1) = x1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x2 a__U32_A(x1) = x1 a__isQid_A(x1) = x1 a__U41_A(x1,x2,x3) = x2 + x3 a__U42_A(x1,x2) = x1 + x2 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x2 + x3 a__U52_A(x1,x2) = x1 + x2 a__U53_A(x1) = x1 a__U61_A(x1,x2) = x2 a__U62_A(x1) = x1 a__U71_A(x1,x2) = x2 a__U72_A(x1) = x1 a__isNePal_A(x1) = x1 a__and_A(x1,x2) = x2 a__isPalListKind_A(x1) = x1 nil_A() = 0 isPalListKind_A(x1) = x1 and_A(x1,x2) = x2 isPal_A(x1) = x1 a__isPal_A(x1) = x1 a_A() = 0 e_A() = 0 i_A() = 0 o_A() = 0 u_A() = 0 U11_A(x1,x2) = x2 U12_A(x1) = x1 isNeList_A(x1) = x1 U21_A(x1,x2,x3) = x2 + x3 U22_A(x1,x2) = x1 + x2 isList_A(x1) = x1 U23_A(x1) = x1 U31_A(x1,x2) = x2 U32_A(x1) = x1 isQid_A(x1) = x1 U41_A(x1,x2,x3) = x2 + x3 U42_A(x1,x2) = x1 + x2 U43_A(x1) = x1 U51_A(x1,x2,x3) = x2 + x3 U52_A(x1,x2) = x1 + x2 U53_A(x1) = x1 U61_A(x1,x2) = x2 U62_A(x1) = x1 U71_A(x1,x2) = x2 U72_A(x1) = x1 isNePal_A(x1) = x1 The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(isPal(X)) -> a__isPal#(X) p2: a__isPal#(V) -> a__U71#(a__isPalListKind(V),V) p3: a__U71#(tt(),V) -> a__isNePal#(V) p4: a__isNePal#(V) -> a__isPalListKind#(V) p5: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p6: a__and#(tt(),X) -> mark#(X) p7: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) p8: a__U11#(tt(),V) -> a__isNeList#(V) p9: a__isNeList#(V) -> a__isPalListKind#(V) p10: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p11: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p12: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) p13: a__U42#(tt(),V2) -> a__isNeList#(V2) p14: a__isNeList#(__(V1,V2)) -> a__U51#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p15: a__U51#(tt(),V1,V2) -> a__U52#(a__isNeList(V1),V2) p16: a__U52#(tt(),V2) -> a__isList#(V2) p17: a__isList#(V) -> a__U11#(a__isPalListKind(V),V) p18: a__isList#(V) -> a__isPalListKind#(V) p19: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p20: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p21: a__U22#(tt(),V2) -> a__isList#(V2) p22: a__isList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p23: a__isList#(__(V1,V2)) -> a__isPalListKind#(V1) p24: a__U21#(tt(),V1,V2) -> a__isList#(V1) p25: a__U51#(tt(),V1,V2) -> a__isNeList#(V1) p26: a__isNeList#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p27: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1) p28: a__U41#(tt(),V1,V2) -> a__isList#(V1) p29: mark#(U11(X1,X2)) -> mark#(X1) p30: mark#(U12(X)) -> mark#(X) p31: mark#(isNeList(X)) -> a__isNeList#(X) p32: mark#(U23(X)) -> mark#(X) p33: mark#(U31(X1,X2)) -> mark#(X1) p34: mark#(U32(X)) -> mark#(X) p35: mark#(U42(X1,X2)) -> a__U42#(mark(X1),X2) p36: mark#(U42(X1,X2)) -> mark#(X1) p37: mark#(U43(X)) -> mark#(X) p38: mark#(U53(X)) -> mark#(X) p39: mark#(U61(X1,X2)) -> mark#(X1) p40: mark#(U62(X)) -> mark#(X) p41: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p42: mark#(U71(X1,X2)) -> mark#(X1) p43: mark#(U72(X)) -> mark#(X) p44: mark#(isNePal(X)) -> a__isNePal#(X) p45: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p46: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPalListKind(I)) p47: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p48: mark#(and(X1,X2)) -> mark#(X1) p49: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p50: a__isPal#(V) -> a__isPalListKind#(V) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: mark#_A(x1) = x1 isPal_A(x1) = x1 + 2 a__isPal#_A(x1) = x1 + 1 a__U71#_A(x1,x2) = x2 a__isPalListKind_A(x1) = 0 tt_A() = 0 a__isNePal#_A(x1) = x1 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__and#_A(x1,x2) = x2 isPalListKind_A(x1) = 0 U11_A(x1,x2) = x1 + x2 + 1 a__U11#_A(x1,x2) = x1 + x2 mark_A(x1) = x1 a__isNeList#_A(x1) = x1 a__U41#_A(x1,x2,x3) = x2 + x3 + 1 a__and_A(x1,x2) = x1 + x2 a__U42#_A(x1,x2) = x1 + x2 a__isList_A(x1) = x1 + 1 a__U51#_A(x1,x2,x3) = x2 + x3 + 1 a__U52#_A(x1,x2) = x2 + 1 a__isNeList_A(x1) = x1 + 1 a__isList#_A(x1) = x1 + 1 a__U21#_A(x1,x2,x3) = x2 + x3 + 2 a__U22#_A(x1,x2) = x1 + x2 + 1 U12_A(x1) = x1 isNeList_A(x1) = x1 + 1 U23_A(x1) = x1 U31_A(x1,x2) = x1 + x2 U32_A(x1) = x1 U42_A(x1,x2) = x1 + x2 + 1 U43_A(x1) = x1 U53_A(x1) = x1 U61_A(x1,x2) = x1 + x2 U62_A(x1) = x1 U71_A(x1,x2) = x1 + x2 U72_A(x1) = x1 isNePal_A(x1) = x1 a__isQid_A(x1) = x1 and_A(x1,x2) = x1 + x2 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x1 + x2 + 1 a__U12_A(x1) = x1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x1 + x2 a__U32_A(x1) = x1 a__U41_A(x1,x2,x3) = x2 + x3 + 2 a__U42_A(x1,x2) = x1 + x2 + 1 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x2 + x3 + 1 a__U52_A(x1,x2) = x2 + 1 a__U53_A(x1) = x1 a__U61_A(x1,x2) = x1 + x2 a__U62_A(x1) = x1 a__U71_A(x1,x2) = x1 + x2 a__U72_A(x1) = x1 a__isNePal_A(x1) = x1 a__isPal_A(x1) = x1 + 2 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 U41_A(x1,x2,x3) = x2 + x3 + 2 U51_A(x1,x2,x3) = x2 + x3 + 1 U52_A(x1,x2) = x2 + 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 isList_A(x1) = x1 + 1 isQid_A(x1) = x1 The next rules are strictly ordered: p1, p2, p7, p17, p18, p22, p23, p24, p25, p26, p27, p29, p31, p35, p36, p46, p50 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U71#(tt(),V) -> a__isNePal#(V) p2: a__isNePal#(V) -> a__isPalListKind#(V) p3: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p4: a__and#(tt(),X) -> mark#(X) p5: a__U11#(tt(),V) -> a__isNeList#(V) p6: a__isNeList#(V) -> a__isPalListKind#(V) p7: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p8: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p9: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) p10: a__U42#(tt(),V2) -> a__isNeList#(V2) p11: a__isNeList#(__(V1,V2)) -> a__U51#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p12: a__U51#(tt(),V1,V2) -> a__U52#(a__isNeList(V1),V2) p13: a__U52#(tt(),V2) -> a__isList#(V2) p14: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p15: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p16: a__U22#(tt(),V2) -> a__isList#(V2) p17: a__U41#(tt(),V1,V2) -> a__isList#(V1) p18: mark#(U12(X)) -> mark#(X) p19: mark#(U23(X)) -> mark#(X) p20: mark#(U31(X1,X2)) -> mark#(X1) p21: mark#(U32(X)) -> mark#(X) p22: mark#(U43(X)) -> mark#(X) p23: mark#(U53(X)) -> mark#(X) p24: mark#(U61(X1,X2)) -> mark#(X1) p25: mark#(U62(X)) -> mark#(X) p26: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p27: mark#(U71(X1,X2)) -> mark#(X1) p28: mark#(U72(X)) -> mark#(X) p29: mark#(isNePal(X)) -> a__isNePal#(X) p30: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p31: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p32: mark#(and(X1,X2)) -> mark#(X1) p33: mark#(isPalListKind(X)) -> a__isPalListKind#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p8, p9, p10} {p1, p2, p3, p4, p7, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33} {p14, p15, p16} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U42#(tt(),V2) -> a__isNeList#(V2) p2: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p3: a__U41#(tt(),V1,V2) -> a__U42#(a__isList(V1),V2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__U42#_A(x1,x2) = x2 + 1 tt_A() = 1 a__isNeList#_A(x1) = x1 ___A(x1,x2) = x1 + x2 + 2 a__U41#_A(x1,x2,x3) = x3 + 2 a__and_A(x1,x2) = x2 a__isPalListKind_A(x1) = 1 isPalListKind_A(x1) = 1 a__isList_A(x1) = x1 + 1 a_____A(x1,x2) = x1 + x2 + 2 mark_A(x1) = x1 nil_A() = 1 a__U12_A(x1) = 1 a__U22_A(x1,x2) = 1 a__U23_A(x1) = 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = 1 a__isQid_A(x1) = x1 + 1 a__U41_A(x1,x2,x3) = x2 + x3 + 1 a__U42_A(x1,x2) = x2 + 1 a__U43_A(x1) = 1 a__isNeList_A(x1) = x1 + 1 a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 1 a__U52_A(x1,x2) = x2 + 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = 1 a__U62_A(x1) = 1 a__U71_A(x1,x2) = 1 a__U72_A(x1) = 1 a__isNePal_A(x1) = x1 + 1 and_A(x1,x2) = x2 isPal_A(x1) = 1 a__isPal_A(x1) = 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U12_A(x1) = 1 isNeList_A(x1) = x1 + 1 U22_A(x1,x2) = 1 U23_A(x1) = 1 U31_A(x1,x2) = x2 + 1 U32_A(x1) = 1 isQid_A(x1) = x1 + 1 U41_A(x1,x2,x3) = x2 + x3 + 1 U42_A(x1,x2) = x2 + 1 U43_A(x1) = 1 U51_A(x1,x2,x3) = x1 + x2 + x3 + 1 U52_A(x1,x2) = x2 + 1 U53_A(x1) = 1 U61_A(x1,x2) = 1 U62_A(x1) = 1 U71_A(x1,x2) = 1 U72_A(x1) = 1 isNePal_A(x1) = x1 + 1 a__U11_A(x1,x2) = 1 a__U21_A(x1,x2,x3) = 1 U11_A(x1,x2) = 1 U21_A(x1,x2,x3) = 1 isList_A(x1) = x1 + 1 The next rules are strictly ordered: p1, p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__isNeList#(__(V1,V2)) -> a__U41#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(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: a__U71#(tt(),V) -> a__isNePal#(V) p2: a__isNePal#(__(I,__(P,I))) -> a__and#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) p3: a__and#(tt(),X) -> mark#(X) p4: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p5: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p6: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p7: mark#(and(X1,X2)) -> mark#(X1) p8: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p9: mark#(isNePal(X)) -> a__isNePal#(X) p10: a__isNePal#(V) -> a__isPalListKind#(V) p11: mark#(U72(X)) -> mark#(X) p12: mark#(U71(X1,X2)) -> mark#(X1) p13: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2) p14: mark#(U62(X)) -> mark#(X) p15: mark#(U61(X1,X2)) -> mark#(X1) p16: mark#(U53(X)) -> mark#(X) p17: mark#(U43(X)) -> mark#(X) p18: mark#(U32(X)) -> mark#(X) p19: mark#(U31(X1,X2)) -> mark#(X1) p20: mark#(U23(X)) -> mark#(X) p21: mark#(U12(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__U71#_A(x1,x2) = x2 + 3 tt_A() = 0 a__isNePal#_A(x1) = x1 + 1 ___A(x1,x2) = x1 + x2 + 3 a__and#_A(x1,x2) = x2 a__and_A(x1,x2) = x1 + x2 a__isQid_A(x1) = x1 + 1 isPalListKind_A(x1) = 0 and_A(x1,x2) = x1 + x2 isPal_A(x1) = x1 + 5 mark#_A(x1) = x1 a__isPalListKind#_A(x1) = 0 a__isPalListKind_A(x1) = 0 mark_A(x1) = x1 isNePal_A(x1) = x1 + 1 U72_A(x1) = x1 U71_A(x1,x2) = x1 + x2 + 5 U62_A(x1) = x1 U61_A(x1,x2) = x1 + x2 + 1 U53_A(x1) = x1 U43_A(x1) = x1 U32_A(x1) = x1 U31_A(x1,x2) = x1 + x2 + 1 U23_A(x1) = x1 U12_A(x1) = x1 a_____A(x1,x2) = x1 + x2 + 3 nil_A() = 1 a__U11_A(x1,x2) = x1 + x2 + 1 a__U12_A(x1) = x1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x1 + x2 + 1 a__U32_A(x1) = x1 a__U41_A(x1,x2,x3) = x1 + x2 + x3 + 2 a__U42_A(x1,x2) = x1 + x2 + 1 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 2 a__U52_A(x1,x2) = x1 + x2 + 1 a__U53_A(x1) = x1 a__U61_A(x1,x2) = x1 + x2 + 1 a__U62_A(x1) = x1 a__U71_A(x1,x2) = x1 + x2 + 5 a__U72_A(x1) = x1 a__isNePal_A(x1) = x1 + 1 a__isPal_A(x1) = x1 + 5 U11_A(x1,x2) = x1 + x2 + 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U41_A(x1,x2,x3) = x1 + x2 + x3 + 2 U42_A(x1,x2) = x1 + x2 + 1 U51_A(x1,x2,x3) = x1 + x2 + x3 + 2 U52_A(x1,x2) = x1 + x2 + 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 isQid_A(x1) = x1 + 1 The next rules are strictly ordered: p1, p2, p10, p12, p13, p15, p19 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(isNePal(X)) -> a__isNePal#(X) p8: mark#(U72(X)) -> mark#(X) p9: mark#(U62(X)) -> mark#(X) p10: mark#(U53(X)) -> mark#(X) p11: mark#(U43(X)) -> mark#(X) p12: mark#(U32(X)) -> mark#(X) p13: mark#(U23(X)) -> mark#(X) p14: mark#(U12(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p8, p9, p10, p11, p12, p13, p14} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(U12(X)) -> mark#(X) p3: mark#(U23(X)) -> mark#(X) p4: mark#(U32(X)) -> mark#(X) p5: mark#(U43(X)) -> mark#(X) p6: mark#(U53(X)) -> mark#(X) p7: mark#(U62(X)) -> mark#(X) p8: mark#(U72(X)) -> mark#(X) p9: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p12: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p13: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 U12_A(x1) = x1 U23_A(x1) = x1 U32_A(x1) = x1 U43_A(x1) = x1 U53_A(x1) = x1 + 1 U62_A(x1) = x1 U72_A(x1) = x1 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = x1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = x1 a__isQid_A(x1) = 0 a__U41_A(x1,x2,x3) = x2 + x3 + 1 a__U42_A(x1,x2) = x2 + 1 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x2 + x3 + 2 a__U52_A(x1,x2) = x2 + 2 a__U53_A(x1) = x1 + 1 a__U61_A(x1,x2) = 0 a__U62_A(x1) = x1 a__U71_A(x1,x2) = 0 a__U72_A(x1) = x1 a__isNePal_A(x1) = 0 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = 0 a__isPal_A(x1) = 0 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U31_A(x1,x2) = x2 + 1 isQid_A(x1) = 0 U41_A(x1,x2,x3) = x2 + x3 + 1 U42_A(x1,x2) = x2 + 1 U51_A(x1,x2,x3) = x2 + x3 + 2 U52_A(x1,x2) = x2 + 2 U61_A(x1,x2) = 0 U71_A(x1,x2) = 0 isNePal_A(x1) = 0 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: a__and#(tt(),X) -> mark#(X) p2: mark#(U12(X)) -> mark#(X) p3: mark#(U23(X)) -> mark#(X) p4: mark#(U32(X)) -> mark#(X) p5: mark#(U43(X)) -> mark#(X) p6: mark#(U62(X)) -> mark#(X) p7: mark#(U72(X)) -> mark#(X) p8: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p9: mark#(and(X1,X2)) -> mark#(X1) p10: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p11: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p12: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) p8: mark#(U62(X)) -> mark#(X) p9: mark#(U43(X)) -> mark#(X) p10: mark#(U32(X)) -> mark#(X) p11: mark#(U23(X)) -> mark#(X) p12: mark#(U12(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 U72_A(x1) = x1 U62_A(x1) = x1 U43_A(x1) = x1 U32_A(x1) = x1 U23_A(x1) = x1 + 1 U12_A(x1) = x1 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 0 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = x1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 2 a__U22_A(x1,x2) = x2 + 2 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = x1 + 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = x1 a__isQid_A(x1) = 0 a__U41_A(x1,x2,x3) = x2 + x3 + 1 a__U42_A(x1,x2) = x2 + 1 a__U43_A(x1) = x1 a__U51_A(x1,x2,x3) = x2 + 1 a__U52_A(x1,x2) = 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = 1 a__U62_A(x1) = x1 a__U71_A(x1,x2) = 1 a__U72_A(x1) = x1 a__isNePal_A(x1) = 1 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = 1 a__isPal_A(x1) = 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 2 U22_A(x1,x2) = x2 + 2 isList_A(x1) = x1 + 1 U31_A(x1,x2) = x2 + 1 isQid_A(x1) = 0 U41_A(x1,x2,x3) = x2 + x3 + 1 U42_A(x1,x2) = x2 + 1 U51_A(x1,x2,x3) = x2 + 1 U52_A(x1,x2) = 1 U53_A(x1) = 1 U61_A(x1,x2) = 1 U71_A(x1,x2) = 1 isNePal_A(x1) = 1 The next rules are strictly ordered: p11 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) p8: mark#(U62(X)) -> mark#(X) p9: mark#(U43(X)) -> mark#(X) p10: mark#(U32(X)) -> mark#(X) p11: mark#(U12(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(U12(X)) -> mark#(X) p3: mark#(U32(X)) -> mark#(X) p4: mark#(U43(X)) -> mark#(X) p5: mark#(U62(X)) -> mark#(X) p6: mark#(U72(X)) -> mark#(X) p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p8: mark#(and(X1,X2)) -> mark#(X1) p9: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p10: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p11: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 U12_A(x1) = x1 U32_A(x1) = x1 U43_A(x1) = x1 + 1 U62_A(x1) = x1 U72_A(x1) = x1 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = x1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = x1 a__isQid_A(x1) = 0 a__U41_A(x1,x2,x3) = x2 + x3 + 2 a__U42_A(x1,x2) = x2 + 2 a__U43_A(x1) = x1 + 1 a__U51_A(x1,x2,x3) = x2 + x3 + 2 a__U52_A(x1,x2) = 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = 1 a__U62_A(x1) = x1 a__U71_A(x1,x2) = 1 a__U72_A(x1) = x1 a__isNePal_A(x1) = 1 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = 1 a__isPal_A(x1) = 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U23_A(x1) = 1 U31_A(x1,x2) = x2 + 1 isQid_A(x1) = 0 U41_A(x1,x2,x3) = x2 + x3 + 2 U42_A(x1,x2) = x2 + 2 U51_A(x1,x2,x3) = x2 + x3 + 2 U52_A(x1,x2) = 1 U53_A(x1) = 1 U61_A(x1,x2) = 1 U71_A(x1,x2) = 1 isNePal_A(x1) = 1 The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(U12(X)) -> mark#(X) p3: mark#(U32(X)) -> mark#(X) p4: mark#(U62(X)) -> mark#(X) p5: mark#(U72(X)) -> mark#(X) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(and(X1,X2)) -> mark#(X1) p8: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p9: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p10: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) p8: mark#(U62(X)) -> mark#(X) p9: mark#(U32(X)) -> mark#(X) p10: mark#(U12(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 3 a__isPalListKind_A(x1) = 0 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 U72_A(x1) = x1 U62_A(x1) = x1 U32_A(x1) = x1 U12_A(x1) = x1 + 1 a_____A(x1,x2) = x1 + x2 + 3 nil_A() = 1 a__U11_A(x1,x2) = x1 + x2 + 2 a__U12_A(x1) = x1 + 1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x1 + x2 + x3 + 5 a__U22_A(x1,x2) = x1 + x2 + 3 a__isList_A(x1) = x1 + 2 a__U23_A(x1) = x1 + 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = x1 a__isQid_A(x1) = 1 a__U41_A(x1,x2,x3) = x1 + x2 + x3 + 2 a__U42_A(x1,x2) = x2 + 2 a__U43_A(x1) = x1 + 1 a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 4 a__U52_A(x1,x2) = x1 + x2 + 3 a__U53_A(x1) = x1 + 1 a__U61_A(x1,x2) = x1 + x2 + 1 a__U62_A(x1) = x1 a__U71_A(x1,x2) = x1 + x2 + 1 a__U72_A(x1) = x1 a__isNePal_A(x1) = x1 + 1 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = x1 + 1 a__isPal_A(x1) = x1 + 1 a_A() = 0 e_A() = 0 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x1 + x2 + 2 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x1 + x2 + x3 + 5 U22_A(x1,x2) = x1 + x2 + 3 isList_A(x1) = x1 + 2 U23_A(x1) = x1 + 1 U31_A(x1,x2) = x2 + 1 isQid_A(x1) = 1 U41_A(x1,x2,x3) = x1 + x2 + x3 + 2 U42_A(x1,x2) = x2 + 2 U43_A(x1) = x1 + 1 U51_A(x1,x2,x3) = x1 + x2 + x3 + 4 U52_A(x1,x2) = x1 + x2 + 3 U53_A(x1) = x1 + 1 U61_A(x1,x2) = x1 + x2 + 1 U71_A(x1,x2) = x1 + x2 + 1 isNePal_A(x1) = x1 + 1 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: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) p8: mark#(U62(X)) -> mark#(X) p9: mark#(U32(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(U32(X)) -> mark#(X) p3: mark#(U62(X)) -> mark#(X) p4: mark#(U72(X)) -> mark#(X) p5: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p6: mark#(and(X1,X2)) -> mark#(X1) p7: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p8: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p9: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 U32_A(x1) = x1 U62_A(x1) = x1 + 1 U72_A(x1) = x1 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = 1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = x1 a__isQid_A(x1) = 0 a__U41_A(x1,x2,x3) = x2 + x3 + 1 a__U42_A(x1,x2) = x2 + 1 a__U43_A(x1) = 1 a__U51_A(x1,x2,x3) = x2 + x3 + 2 a__U52_A(x1,x2) = x2 + 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = 1 a__U62_A(x1) = x1 + 1 a__U71_A(x1,x2) = 1 a__U72_A(x1) = x1 a__isNePal_A(x1) = 1 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = 1 a__isPal_A(x1) = 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 U12_A(x1) = 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U23_A(x1) = 1 U31_A(x1,x2) = x2 + 1 isQid_A(x1) = 0 U41_A(x1,x2,x3) = x2 + x3 + 1 U42_A(x1,x2) = x2 + 1 U43_A(x1) = 1 U51_A(x1,x2,x3) = x2 + x3 + 2 U52_A(x1,x2) = x2 + 1 U53_A(x1) = 1 U61_A(x1,x2) = 1 U71_A(x1,x2) = 1 isNePal_A(x1) = 1 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: a__and#(tt(),X) -> mark#(X) p2: mark#(U32(X)) -> mark#(X) p3: mark#(U72(X)) -> mark#(X) p4: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p7: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p8: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) p8: mark#(U32(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 U72_A(x1) = x1 U32_A(x1) = x1 + 1 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x2 + 3 a__U12_A(x1) = x1 + 1 a__isNeList_A(x1) = x1 + 2 a__U21_A(x1,x2,x3) = x1 + x2 + x3 + 4 a__U22_A(x1,x2) = x1 + 1 a__isList_A(x1) = x1 + 3 a__U23_A(x1) = 1 a__U31_A(x1,x2) = x2 + 2 a__U32_A(x1) = x1 + 1 a__isQid_A(x1) = x1 + 1 a__U41_A(x1,x2,x3) = x2 + x3 + 3 a__U42_A(x1,x2) = x2 + 3 a__U43_A(x1) = x1 + 1 a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 3 a__U52_A(x1,x2) = x1 + x2 + 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = x1 + x2 + 2 a__U62_A(x1) = x1 + 1 a__U71_A(x1,x2) = x2 + 2 a__U72_A(x1) = x1 a__isNePal_A(x1) = x1 + 2 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = x1 + 2 a__isPal_A(x1) = x1 + 2 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 3 U12_A(x1) = x1 + 1 isNeList_A(x1) = x1 + 2 U21_A(x1,x2,x3) = x1 + x2 + x3 + 4 U22_A(x1,x2) = x1 + 1 isList_A(x1) = x1 + 3 U23_A(x1) = 1 U31_A(x1,x2) = x2 + 2 isQid_A(x1) = x1 + 1 U41_A(x1,x2,x3) = x2 + x3 + 3 U42_A(x1,x2) = x2 + 3 U43_A(x1) = x1 + 1 U51_A(x1,x2,x3) = x1 + x2 + x3 + 3 U52_A(x1,x2) = x1 + x2 + 1 U53_A(x1) = 1 U61_A(x1,x2) = x1 + x2 + 2 U62_A(x1) = x1 + 1 U71_A(x1,x2) = x2 + 2 isNePal_A(x1) = x1 + 2 The next rules are strictly ordered: p8 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p7: mark#(U72(X)) -> mark#(X) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__and#(tt(),X) -> mark#(X) p2: mark#(U72(X)) -> mark#(X) p3: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p4: mark#(and(X1,X2)) -> mark#(X1) p5: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p6: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p7: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 tt_A() = 0 mark#_A(x1) = x1 U72_A(x1) = x1 + 1 and_A(x1,x2) = x1 + x2 mark_A(x1) = x1 isPalListKind_A(x1) = 0 a__isPalListKind#_A(x1) = 0 ___A(x1,x2) = x1 + x2 + 1 a__isPalListKind_A(x1) = 0 a_____A(x1,x2) = x1 + x2 + 1 nil_A() = 1 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = 1 a__isNeList_A(x1) = 0 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = 1 a__U31_A(x1,x2) = 0 a__U32_A(x1) = 0 a__isQid_A(x1) = 1 a__U41_A(x1,x2,x3) = 0 a__U42_A(x1,x2) = 0 a__U43_A(x1) = 0 a__U51_A(x1,x2,x3) = 0 a__U52_A(x1,x2) = 0 a__U53_A(x1) = 0 a__U61_A(x1,x2) = x2 + 1 a__U62_A(x1) = 1 a__U71_A(x1,x2) = x2 + 2 a__U72_A(x1) = x1 + 1 a__isNePal_A(x1) = x1 + 1 a__and_A(x1,x2) = x1 + x2 isPal_A(x1) = x1 + 2 a__isPal_A(x1) = x1 + 2 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 U12_A(x1) = 1 isNeList_A(x1) = 0 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U23_A(x1) = 1 U31_A(x1,x2) = 0 U32_A(x1) = 0 isQid_A(x1) = 1 U41_A(x1,x2,x3) = 0 U42_A(x1,x2) = 0 U43_A(x1) = 0 U51_A(x1,x2,x3) = 0 U52_A(x1,x2) = 0 U53_A(x1) = 0 U61_A(x1,x2) = x2 + 1 U62_A(x1) = 1 U71_A(x1,x2) = x2 + 2 isNePal_A(x1) = x1 + 1 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: a__and#(tt(),X) -> mark#(X) p2: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p3: mark#(and(X1,X2)) -> mark#(X1) p4: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p5: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p6: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(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: a__and#(tt(),X) -> mark#(X) p2: mark#(isPalListKind(X)) -> a__isPalListKind#(X) p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1) p4: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p5: mark#(and(X1,X2)) -> mark#(X1) p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__and#_A(x1,x2) = x2 + 1 tt_A() = 1 mark#_A(x1) = x1 isPalListKind_A(x1) = x1 + 1 a__isPalListKind#_A(x1) = x1 ___A(x1,x2) = x1 + x2 + 2 a__isPalListKind_A(x1) = x1 + 1 and_A(x1,x2) = x1 + x2 + 1 mark_A(x1) = x1 a_____A(x1,x2) = x1 + x2 + 2 nil_A() = 1 a__U11_A(x1,x2) = x2 + 1 a__U12_A(x1) = 1 a__isNeList_A(x1) = x1 + 1 a__U21_A(x1,x2,x3) = x2 + x3 + 1 a__U22_A(x1,x2) = x2 + 1 a__isList_A(x1) = x1 + 1 a__U23_A(x1) = 1 a__U31_A(x1,x2) = x2 + 1 a__U32_A(x1) = 1 a__isQid_A(x1) = x1 + 1 a__U41_A(x1,x2,x3) = x2 + x3 + 1 a__U42_A(x1,x2) = x2 + 1 a__U43_A(x1) = 1 a__U51_A(x1,x2,x3) = x2 + x3 + 1 a__U52_A(x1,x2) = x2 + 1 a__U53_A(x1) = 1 a__U61_A(x1,x2) = x2 + 1 a__U62_A(x1) = 1 a__U71_A(x1,x2) = 1 a__U72_A(x1) = 1 a__isNePal_A(x1) = x1 + 3 a__and_A(x1,x2) = x1 + x2 + 1 isPal_A(x1) = 1 a__isPal_A(x1) = 1 a_A() = 1 e_A() = 1 i_A() = 1 o_A() = 1 u_A() = 1 U11_A(x1,x2) = x2 + 1 U12_A(x1) = 1 isNeList_A(x1) = x1 + 1 U21_A(x1,x2,x3) = x2 + x3 + 1 U22_A(x1,x2) = x2 + 1 isList_A(x1) = x1 + 1 U23_A(x1) = 1 U31_A(x1,x2) = x2 + 1 U32_A(x1) = 1 isQid_A(x1) = x1 + 1 U41_A(x1,x2,x3) = x2 + x3 + 1 U42_A(x1,x2) = x2 + 1 U43_A(x1) = 1 U51_A(x1,x2,x3) = x2 + x3 + 1 U52_A(x1,x2) = x2 + 1 U53_A(x1) = 1 U61_A(x1,x2) = x2 + 1 U62_A(x1) = 1 U71_A(x1,x2) = 1 U72_A(x1) = 1 isNePal_A(x1) = x1 + 3 The next rules are strictly ordered: p1, p2, p3, p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__isPalListKind#(__(V1,V2)) -> a__and#(a__isPalListKind(V1),isPalListKind(V2)) p2: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(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: a__isList#(__(V1,V2)) -> a__U21#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) p2: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p3: a__U22#(tt(),V2) -> a__isList#(V2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, 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, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100 Take the reduction pair: matrix interpretations: carrier: N^1 order: standard order interpretations: a__isList#_A(x1) = x1 + 5 ___A(x1,x2) = x1 + x2 a__U21#_A(x1,x2,x3) = x1 + x2 + x3 a__and_A(x1,x2) = x2 a__isPalListKind_A(x1) = 4 isPalListKind_A(x1) = 4 tt_A() = 4 a__U22#_A(x1,x2) = x1 + x2 + 1 a__isList_A(x1) = x1 + 3 a_____A(x1,x2) = x1 + x2 mark_A(x1) = x1 nil_A() = 1 a__U12_A(x1) = x1 + 1 a__U22_A(x1,x2) = x1 + x2 a__U23_A(x1) = 4 a__U31_A(x1,x2) = x2 + 2 a__U32_A(x1) = x1 + 1 a__isQid_A(x1) = x1 + 1 a__U41_A(x1,x2,x3) = x2 + x3 + 2 a__U42_A(x1,x2) = x2 + 2 a__U43_A(x1) = x1 a__isNeList_A(x1) = x1 + 2 a__U51_A(x1,x2,x3) = x2 + x3 + 2 a__U52_A(x1,x2) = x1 + x2 a__U53_A(x1) = 4 a__U61_A(x1,x2) = x1 + x2 + 1 a__U62_A(x1) = 4 a__U71_A(x1,x2) = x2 + 4 a__U72_A(x1) = 4 a__isNePal_A(x1) = x1 + 5 and_A(x1,x2) = x2 isPal_A(x1) = x1 + 4 a__isPal_A(x1) = x1 + 4 a_A() = 3 e_A() = 3 i_A() = 3 o_A() = 3 u_A() = 3 U12_A(x1) = x1 + 1 isNeList_A(x1) = x1 + 2 U22_A(x1,x2) = x1 + x2 U23_A(x1) = 4 U31_A(x1,x2) = x2 + 2 U32_A(x1) = x1 + 1 isQid_A(x1) = x1 + 1 U41_A(x1,x2,x3) = x2 + x3 + 2 U42_A(x1,x2) = x2 + 2 U43_A(x1) = x1 U51_A(x1,x2,x3) = x2 + x3 + 2 U52_A(x1,x2) = x1 + x2 U53_A(x1) = 4 U61_A(x1,x2) = x1 + x2 + 1 U62_A(x1) = 4 U71_A(x1,x2) = x2 + 4 U72_A(x1) = 4 isNePal_A(x1) = x1 + 5 a__U11_A(x1,x2) = x2 + 3 a__U21_A(x1,x2,x3) = x2 + x3 + 3 U11_A(x1,x2) = x2 + 3 U21_A(x1,x2,x3) = x2 + x3 + 3 isList_A(x1) = x1 + 3 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: a__U21#(tt(),V1,V2) -> a__U22#(a__isList(V1),V2) p2: a__U22#(tt(),V2) -> a__isList#(V2) and R consists of: r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) r2: a____(X,nil()) -> mark(X) r3: a____(nil(),X) -> mark(X) r4: a__U11(tt(),V) -> a__U12(a__isNeList(V)) r5: a__U12(tt()) -> tt() r6: a__U21(tt(),V1,V2) -> a__U22(a__isList(V1),V2) r7: a__U22(tt(),V2) -> a__U23(a__isList(V2)) r8: a__U23(tt()) -> tt() r9: a__U31(tt(),V) -> a__U32(a__isQid(V)) r10: a__U32(tt()) -> tt() r11: a__U41(tt(),V1,V2) -> a__U42(a__isList(V1),V2) r12: a__U42(tt(),V2) -> a__U43(a__isNeList(V2)) r13: a__U43(tt()) -> tt() r14: a__U51(tt(),V1,V2) -> a__U52(a__isNeList(V1),V2) r15: a__U52(tt(),V2) -> a__U53(a__isList(V2)) r16: a__U53(tt()) -> tt() r17: a__U61(tt(),V) -> a__U62(a__isQid(V)) r18: a__U62(tt()) -> tt() r19: a__U71(tt(),V) -> a__U72(a__isNePal(V)) r20: a__U72(tt()) -> tt() r21: a__and(tt(),X) -> mark(X) r22: a__isList(V) -> a__U11(a__isPalListKind(V),V) r23: a__isList(nil()) -> tt() r24: a__isList(__(V1,V2)) -> a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r25: a__isNeList(V) -> a__U31(a__isPalListKind(V),V) r26: a__isNeList(__(V1,V2)) -> a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r27: a__isNeList(__(V1,V2)) -> a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2) r28: a__isNePal(V) -> a__U61(a__isPalListKind(V),V) r29: a__isNePal(__(I,__(P,I))) -> a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))) r30: a__isPal(V) -> a__U71(a__isPalListKind(V),V) r31: a__isPal(nil()) -> tt() r32: a__isPalListKind(a()) -> tt() r33: a__isPalListKind(e()) -> tt() r34: a__isPalListKind(i()) -> tt() r35: a__isPalListKind(nil()) -> tt() r36: a__isPalListKind(o()) -> tt() r37: a__isPalListKind(u()) -> tt() r38: a__isPalListKind(__(V1,V2)) -> a__and(a__isPalListKind(V1),isPalListKind(V2)) r39: a__isQid(a()) -> tt() r40: a__isQid(e()) -> tt() r41: a__isQid(i()) -> tt() r42: a__isQid(o()) -> tt() r43: a__isQid(u()) -> tt() r44: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) r45: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r46: mark(U12(X)) -> a__U12(mark(X)) r47: mark(isNeList(X)) -> a__isNeList(X) r48: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) r49: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r50: mark(isList(X)) -> a__isList(X) r51: mark(U23(X)) -> a__U23(mark(X)) r52: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r53: mark(U32(X)) -> a__U32(mark(X)) r54: mark(isQid(X)) -> a__isQid(X) r55: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r56: mark(U42(X1,X2)) -> a__U42(mark(X1),X2) r57: mark(U43(X)) -> a__U43(mark(X)) r58: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) r59: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r60: mark(U53(X)) -> a__U53(mark(X)) r61: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) r62: mark(U62(X)) -> a__U62(mark(X)) r63: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) r64: mark(U72(X)) -> a__U72(mark(X)) r65: mark(isNePal(X)) -> a__isNePal(X) r66: mark(and(X1,X2)) -> a__and(mark(X1),X2) r67: mark(isPalListKind(X)) -> a__isPalListKind(X) r68: mark(isPal(X)) -> a__isPal(X) r69: mark(nil()) -> nil() r70: mark(tt()) -> tt() r71: mark(a()) -> a() r72: mark(e()) -> e() r73: mark(i()) -> i() r74: mark(o()) -> o() r75: mark(u()) -> u() r76: a____(X1,X2) -> __(X1,X2) r77: a__U11(X1,X2) -> U11(X1,X2) r78: a__U12(X) -> U12(X) r79: a__isNeList(X) -> isNeList(X) r80: a__U21(X1,X2,X3) -> U21(X1,X2,X3) r81: a__U22(X1,X2) -> U22(X1,X2) r82: a__isList(X) -> isList(X) r83: a__U23(X) -> U23(X) r84: a__U31(X1,X2) -> U31(X1,X2) r85: a__U32(X) -> U32(X) r86: a__isQid(X) -> isQid(X) r87: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r88: a__U42(X1,X2) -> U42(X1,X2) r89: a__U43(X) -> U43(X) r90: a__U51(X1,X2,X3) -> U51(X1,X2,X3) r91: a__U52(X1,X2) -> U52(X1,X2) r92: a__U53(X) -> U53(X) r93: a__U61(X1,X2) -> U61(X1,X2) r94: a__U62(X) -> U62(X) r95: a__U71(X1,X2) -> U71(X1,X2) r96: a__U72(X) -> U72(X) r97: a__isNePal(X) -> isNePal(X) r98: a__and(X1,X2) -> and(X1,X2) r99: a__isPalListKind(X) -> isPalListKind(X) r100: a__isPal(X) -> isPal(X) The estimated dependency graph contains the following SCCs: (no SCCs)