YES We show the termination of the TRS R: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(tt()) active(U21(tt(),V2)) -> mark(U22(isList(V2))) active(U22(tt())) -> mark(tt()) active(U31(tt())) -> mark(tt()) active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) active(U42(tt())) -> mark(tt()) active(U51(tt(),V2)) -> mark(U52(isList(V2))) active(U52(tt())) -> mark(tt()) active(U61(tt())) -> mark(tt()) active(U71(tt(),P)) -> mark(U72(isPal(P))) active(U72(tt())) -> mark(tt()) active(U81(tt())) -> mark(tt()) active(isList(V)) -> mark(U11(isNeList(V))) active(isList(nil())) -> mark(tt()) active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) active(isNeList(V)) -> mark(U31(isQid(V))) active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) active(isNePal(V)) -> mark(U61(isQid(V))) active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) active(isPal(V)) -> mark(U81(isNePal(V))) active(isPal(nil())) -> mark(tt()) active(isQid(a())) -> mark(tt()) active(isQid(e())) -> mark(tt()) active(isQid(i())) -> mark(tt()) active(isQid(o())) -> mark(tt()) active(isQid(u())) -> mark(tt()) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U21(X1,X2)) -> U21(active(X1),X2) active(U22(X)) -> U22(active(X)) active(U31(X)) -> U31(active(X)) active(U41(X1,X2)) -> U41(active(X1),X2) active(U42(X)) -> U42(active(X)) active(U51(X1,X2)) -> U51(active(X1),X2) active(U52(X)) -> U52(active(X)) active(U61(X)) -> U61(active(X)) active(U71(X1,X2)) -> U71(active(X1),X2) active(U72(X)) -> U72(active(X)) active(U81(X)) -> U81(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U21(mark(X1),X2) -> mark(U21(X1,X2)) U22(mark(X)) -> mark(U22(X)) U31(mark(X)) -> mark(U31(X)) U41(mark(X1),X2) -> mark(U41(X1,X2)) U42(mark(X)) -> mark(U42(X)) U51(mark(X1),X2) -> mark(U51(X1,X2)) U52(mark(X)) -> mark(U52(X)) U61(mark(X)) -> mark(U61(X)) U71(mark(X1),X2) -> mark(U71(X1,X2)) U72(mark(X)) -> mark(U72(X)) U81(mark(X)) -> mark(U81(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) proper(U22(X)) -> U22(proper(X)) proper(isList(X)) -> isList(proper(X)) proper(U31(X)) -> U31(proper(X)) proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) proper(U42(X)) -> U42(proper(X)) proper(isNeList(X)) -> isNeList(proper(X)) proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) proper(U52(X)) -> U52(proper(X)) proper(U61(X)) -> U61(proper(X)) proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) proper(U72(X)) -> U72(proper(X)) proper(isPal(X)) -> isPal(proper(X)) proper(U81(X)) -> U81(proper(X)) proper(isQid(X)) -> isQid(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) proper(a()) -> ok(a()) proper(e()) -> ok(e()) proper(i()) -> ok(i()) proper(o()) -> ok(o()) proper(u()) -> ok(u()) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) U22(ok(X)) -> ok(U22(X)) isList(ok(X)) -> ok(isList(X)) U31(ok(X)) -> ok(U31(X)) U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) U42(ok(X)) -> ok(U42(X)) isNeList(ok(X)) -> ok(isNeList(X)) U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) U52(ok(X)) -> ok(U52(X)) U61(ok(X)) -> ok(U61(X)) U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) U72(ok(X)) -> ok(U72(X)) isPal(ok(X)) -> ok(isPal(X)) U81(ok(X)) -> ok(U81(X)) isQid(ok(X)) -> ok(isQid(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) p2: active#(__(__(X,Y),Z)) -> __#(Y,Z) p3: active#(U21(tt(),V2)) -> U22#(isList(V2)) p4: active#(U21(tt(),V2)) -> isList#(V2) p5: active#(U41(tt(),V2)) -> U42#(isNeList(V2)) p6: active#(U41(tt(),V2)) -> isNeList#(V2) p7: active#(U51(tt(),V2)) -> U52#(isList(V2)) p8: active#(U51(tt(),V2)) -> isList#(V2) p9: active#(U71(tt(),P)) -> U72#(isPal(P)) p10: active#(U71(tt(),P)) -> isPal#(P) p11: active#(isList(V)) -> U11#(isNeList(V)) p12: active#(isList(V)) -> isNeList#(V) p13: active#(isList(__(V1,V2))) -> U21#(isList(V1),V2) p14: active#(isList(__(V1,V2))) -> isList#(V1) p15: active#(isNeList(V)) -> U31#(isQid(V)) p16: active#(isNeList(V)) -> isQid#(V) p17: active#(isNeList(__(V1,V2))) -> U41#(isList(V1),V2) p18: active#(isNeList(__(V1,V2))) -> isList#(V1) p19: active#(isNeList(__(V1,V2))) -> U51#(isNeList(V1),V2) p20: active#(isNeList(__(V1,V2))) -> isNeList#(V1) p21: active#(isNePal(V)) -> U61#(isQid(V)) p22: active#(isNePal(V)) -> isQid#(V) p23: active#(isNePal(__(I,__(P,I)))) -> U71#(isQid(I),P) p24: active#(isNePal(__(I,__(P,I)))) -> isQid#(I) p25: active#(isPal(V)) -> U81#(isNePal(V)) p26: active#(isPal(V)) -> isNePal#(V) p27: active#(__(X1,X2)) -> __#(active(X1),X2) p28: active#(__(X1,X2)) -> active#(X1) p29: active#(__(X1,X2)) -> __#(X1,active(X2)) p30: active#(__(X1,X2)) -> active#(X2) p31: active#(U11(X)) -> U11#(active(X)) p32: active#(U11(X)) -> active#(X) p33: active#(U21(X1,X2)) -> U21#(active(X1),X2) p34: active#(U21(X1,X2)) -> active#(X1) p35: active#(U22(X)) -> U22#(active(X)) p36: active#(U22(X)) -> active#(X) p37: active#(U31(X)) -> U31#(active(X)) p38: active#(U31(X)) -> active#(X) p39: active#(U41(X1,X2)) -> U41#(active(X1),X2) p40: active#(U41(X1,X2)) -> active#(X1) p41: active#(U42(X)) -> U42#(active(X)) p42: active#(U42(X)) -> active#(X) p43: active#(U51(X1,X2)) -> U51#(active(X1),X2) p44: active#(U51(X1,X2)) -> active#(X1) p45: active#(U52(X)) -> U52#(active(X)) p46: active#(U52(X)) -> active#(X) p47: active#(U61(X)) -> U61#(active(X)) p48: active#(U61(X)) -> active#(X) p49: active#(U71(X1,X2)) -> U71#(active(X1),X2) p50: active#(U71(X1,X2)) -> active#(X1) p51: active#(U72(X)) -> U72#(active(X)) p52: active#(U72(X)) -> active#(X) p53: active#(U81(X)) -> U81#(active(X)) p54: active#(U81(X)) -> active#(X) p55: __#(mark(X1),X2) -> __#(X1,X2) p56: __#(X1,mark(X2)) -> __#(X1,X2) p57: U11#(mark(X)) -> U11#(X) p58: U21#(mark(X1),X2) -> U21#(X1,X2) p59: U22#(mark(X)) -> U22#(X) p60: U31#(mark(X)) -> U31#(X) p61: U41#(mark(X1),X2) -> U41#(X1,X2) p62: U42#(mark(X)) -> U42#(X) p63: U51#(mark(X1),X2) -> U51#(X1,X2) p64: U52#(mark(X)) -> U52#(X) p65: U61#(mark(X)) -> U61#(X) p66: U71#(mark(X1),X2) -> U71#(X1,X2) p67: U72#(mark(X)) -> U72#(X) p68: U81#(mark(X)) -> U81#(X) p69: proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) p70: proper#(__(X1,X2)) -> proper#(X1) p71: proper#(__(X1,X2)) -> proper#(X2) p72: proper#(U11(X)) -> U11#(proper(X)) p73: proper#(U11(X)) -> proper#(X) p74: proper#(U21(X1,X2)) -> U21#(proper(X1),proper(X2)) p75: proper#(U21(X1,X2)) -> proper#(X1) p76: proper#(U21(X1,X2)) -> proper#(X2) p77: proper#(U22(X)) -> U22#(proper(X)) p78: proper#(U22(X)) -> proper#(X) p79: proper#(isList(X)) -> isList#(proper(X)) p80: proper#(isList(X)) -> proper#(X) p81: proper#(U31(X)) -> U31#(proper(X)) p82: proper#(U31(X)) -> proper#(X) p83: proper#(U41(X1,X2)) -> U41#(proper(X1),proper(X2)) p84: proper#(U41(X1,X2)) -> proper#(X1) p85: proper#(U41(X1,X2)) -> proper#(X2) p86: proper#(U42(X)) -> U42#(proper(X)) p87: proper#(U42(X)) -> proper#(X) p88: proper#(isNeList(X)) -> isNeList#(proper(X)) p89: proper#(isNeList(X)) -> proper#(X) p90: proper#(U51(X1,X2)) -> U51#(proper(X1),proper(X2)) p91: proper#(U51(X1,X2)) -> proper#(X1) p92: proper#(U51(X1,X2)) -> proper#(X2) p93: proper#(U52(X)) -> U52#(proper(X)) p94: proper#(U52(X)) -> proper#(X) p95: proper#(U61(X)) -> U61#(proper(X)) p96: proper#(U61(X)) -> proper#(X) p97: proper#(U71(X1,X2)) -> U71#(proper(X1),proper(X2)) p98: proper#(U71(X1,X2)) -> proper#(X1) p99: proper#(U71(X1,X2)) -> proper#(X2) p100: proper#(U72(X)) -> U72#(proper(X)) p101: proper#(U72(X)) -> proper#(X) p102: proper#(isPal(X)) -> isPal#(proper(X)) p103: proper#(isPal(X)) -> proper#(X) p104: proper#(U81(X)) -> U81#(proper(X)) p105: proper#(U81(X)) -> proper#(X) p106: proper#(isQid(X)) -> isQid#(proper(X)) p107: proper#(isQid(X)) -> proper#(X) p108: proper#(isNePal(X)) -> isNePal#(proper(X)) p109: proper#(isNePal(X)) -> proper#(X) p110: __#(ok(X1),ok(X2)) -> __#(X1,X2) p111: U11#(ok(X)) -> U11#(X) p112: U21#(ok(X1),ok(X2)) -> U21#(X1,X2) p113: U22#(ok(X)) -> U22#(X) p114: isList#(ok(X)) -> isList#(X) p115: U31#(ok(X)) -> U31#(X) p116: U41#(ok(X1),ok(X2)) -> U41#(X1,X2) p117: U42#(ok(X)) -> U42#(X) p118: isNeList#(ok(X)) -> isNeList#(X) p119: U51#(ok(X1),ok(X2)) -> U51#(X1,X2) p120: U52#(ok(X)) -> U52#(X) p121: U61#(ok(X)) -> U61#(X) p122: U71#(ok(X1),ok(X2)) -> U71#(X1,X2) p123: U72#(ok(X)) -> U72#(X) p124: isPal#(ok(X)) -> isPal#(X) p125: U81#(ok(X)) -> U81#(X) p126: isQid#(ok(X)) -> isQid#(X) p127: isNePal#(ok(X)) -> isNePal#(X) p128: top#(mark(X)) -> top#(proper(X)) p129: top#(mark(X)) -> proper#(X) p130: top#(ok(X)) -> top#(active(X)) p131: top#(ok(X)) -> active#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The estimated dependency graph contains the following SCCs: {p128, p130} {p28, p30, p32, p34, p36, p38, p40, p42, p44, p46, p48, p50, p52, p54} {p70, p71, p73, p75, p76, p78, p80, p82, p84, p85, p87, p89, p91, p92, p94, p96, p98, p99, p101, p103, p105, p107, p109} {p55, p56, p110} {p59, p113} {p114} {p62, p117} {p118} {p64, p120} {p67, p123} {p124} {p57, p111} {p58, p112} {p60, p115} {p126} {p61, p116} {p63, p119} {p65, p121} {p66, p122} {p68, p125} {p127} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: top#(ok(X)) -> top#(active(X)) p2: top#(mark(X)) -> top#(proper(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(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, r101 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: top#_A(x1) = ((1,1),(0,0)) x1 ok_A(x1) = ((0,1),(1,0)) x1 active_A(x1) = x1 mark_A(x1) = x1 + (1,1) proper_A(x1) = ((0,1),(1,0)) x1 ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (14,14) U11_A(x1) = x1 + (2,2) U21_A(x1,x2) = x1 + x2 + (12,12) U22_A(x1) = x1 + (2,2) U31_A(x1) = ((0,1),(1,0)) x1 + (2,2) U41_A(x1,x2) = x1 + x2 + (8,8) U42_A(x1) = x1 + (2,2) U51_A(x1,x2) = ((0,1),(1,0)) x1 + x2 + (12,12) U52_A(x1) = x1 + (2,2) U61_A(x1) = ((0,1),(1,0)) x1 + (2,2) U71_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (12,12) U72_A(x1) = x1 + (2,2) U81_A(x1) = ((0,1),(1,0)) x1 + (2,2) isList_A(x1) = x1 + (9,9) isNeList_A(x1) = x1 + (5,5) isPal_A(x1) = ((1,1),(1,1)) x1 + (9,9) isQid_A(x1) = ((0,1),(1,0)) x1 + (1,1) isNePal_A(x1) = ((1,1),(1,1)) x1 + (5,5) nil_A() = (1,1) tt_A() = (1,1) a_A() = (1,2) e_A() = (1,2) i_A() = (1,2) o_A() = (1,2) u_A() = (1,2) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: top#_A(x1) = (0,0) ok_A(x1) = (1,1) active_A(x1) = x1 + (1,1) mark_A(x1) = ((0,0),(1,0)) x1 + (4,1) proper_A(x1) = (8,10) ___A(x1,x2) = ((0,0),(1,0)) x2 + (5,2) U11_A(x1) = ((0,0),(1,0)) x1 + (5,2) U21_A(x1,x2) = (5,6) U22_A(x1) = x1 U31_A(x1) = (5,6) U41_A(x1,x2) = (5,6) U42_A(x1) = ((0,0),(1,0)) x1 + (4,1) U51_A(x1,x2) = (5,6) U52_A(x1) = (4,5) U61_A(x1) = (5,6) U71_A(x1,x2) = (4,5) U72_A(x1) = x1 U81_A(x1) = (5,6) isList_A(x1) = (7,1) isNeList_A(x1) = (2,1) isPal_A(x1) = (2,1) isQid_A(x1) = (4,1) isNePal_A(x1) = x1 + (4,0) nil_A() = (1,1) tt_A() = (2,0) a_A() = (1,0) e_A() = (1,0) i_A() = (1,0) o_A() = (0,0) u_A() = (1,0) 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: top#(ok(X)) -> top#(active(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: top#(ok(X)) -> top#(active(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(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, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: top#_A(x1) = ((0,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,0)) x1 + (4,3) active_A(x1) = ((1,1),(1,0)) x1 + (2,1) ___A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(1,0)) x2 + (3,2) mark_A(x1) = (1,1) U11_A(x1) = x1 U21_A(x1,x2) = ((1,1),(1,0)) x2 + (2,2) U22_A(x1) = x1 U31_A(x1) = ((1,1),(1,0)) x1 + (3,2) U41_A(x1,x2) = ((1,1),(1,0)) x2 + (2,1) U42_A(x1) = ((1,1),(1,0)) x1 + (3,2) U51_A(x1,x2) = ((1,1),(1,0)) x2 + (2,1) U52_A(x1) = ((1,1),(1,0)) x1 + (3,2) U61_A(x1) = ((1,1),(1,0)) x1 + (3,2) U71_A(x1,x2) = ((1,1),(1,0)) x2 + (2,1) U72_A(x1) = x1 U81_A(x1) = ((1,1),(1,0)) x1 + (3,2) isList_A(x1) = ((1,1),(1,0)) x1 + (1,1) isNeList_A(x1) = x1 isPal_A(x1) = x1 isQid_A(x1) = ((1,1),(1,0)) x1 + (1,0) isNePal_A(x1) = ((1,1),(1,0)) x1 + (1,1) nil_A() = (0,1) tt_A() = (1,1) a_A() = (0,1) e_A() = (0,1) i_A() = (0,1) o_A() = (0,1) u_A() = (0,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: top#_A(x1) = (0,0) ok_A(x1) = ((1,0),(1,0)) x1 + (3,2) active_A(x1) = x1 + (7,7) ___A(x1,x2) = x1 + ((0,1),(0,1)) x2 + (6,3) mark_A(x1) = (2,18) U11_A(x1) = x1 U21_A(x1,x2) = (6,18) U22_A(x1) = x1 + (0,1) U31_A(x1) = x1 + (2,1) U41_A(x1,x2) = (0,0) U42_A(x1) = (0,1) U51_A(x1,x2) = x2 + (3,0) U52_A(x1) = (1,18) U61_A(x1) = ((1,1),(1,0)) x1 + (3,1) U71_A(x1,x2) = (8,0) U72_A(x1) = ((1,0),(1,0)) x1 + (0,16) U81_A(x1) = (1,10) isList_A(x1) = ((1,0),(1,1)) x1 + (0,1) isNeList_A(x1) = x1 + (1,7) isPal_A(x1) = x1 + (1,1) isQid_A(x1) = ((0,0),(1,0)) x1 isNePal_A(x1) = (1,0) nil_A() = (1,8) tt_A() = (1,1) a_A() = (0,1) e_A() = (0,1) i_A() = (0,1) o_A() = (0,1) u_A() = (1,1) 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: active#(U81(X)) -> active#(X) p2: active#(U72(X)) -> active#(X) p3: active#(U71(X1,X2)) -> active#(X1) p4: active#(U61(X)) -> active#(X) p5: active#(U52(X)) -> active#(X) p6: active#(U51(X1,X2)) -> active#(X1) p7: active#(U42(X)) -> active#(X) p8: active#(U41(X1,X2)) -> active#(X1) p9: active#(U31(X)) -> active#(X) p10: active#(U22(X)) -> active#(X) p11: active#(U21(X1,X2)) -> active#(X1) p12: active#(U11(X)) -> active#(X) p13: active#(__(X1,X2)) -> active#(X2) p14: active#(__(X1,X2)) -> active#(X1) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((1,1),(1,1)) x1 U81_A(x1) = ((1,1),(1,1)) x1 + (1,1) U72_A(x1) = ((1,1),(1,1)) x1 + (1,1) U71_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U61_A(x1) = ((1,1),(1,1)) x1 + (1,1) U52_A(x1) = ((1,1),(1,1)) x1 + (1,1) U51_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U42_A(x1) = ((1,1),(1,1)) x1 + (1,1) U41_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U31_A(x1) = ((1,1),(1,1)) x1 + (1,1) U22_A(x1) = ((1,1),(1,1)) x1 + (1,1) U21_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U11_A(x1) = ((1,1),(1,1)) x1 + (1,1) ___A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: active#_A(x1) = ((1,1),(1,0)) x1 U81_A(x1) = ((1,1),(1,1)) x1 + (1,1) U72_A(x1) = ((1,1),(1,1)) x1 + (1,1) U71_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U61_A(x1) = ((1,1),(1,1)) x1 + (1,1) U52_A(x1) = ((1,1),(1,1)) x1 + (1,1) U51_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U42_A(x1) = ((1,1),(1,1)) x1 + (1,1) U41_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U31_A(x1) = ((1,1),(1,1)) x1 + (1,1) U22_A(x1) = ((1,1),(1,1)) x1 + (1,1) U21_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U11_A(x1) = ((1,1),(1,1)) x1 + (1,1) ___A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14 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, r101, r102, r103 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: proper#(isNePal(X)) -> proper#(X) p2: proper#(isQid(X)) -> proper#(X) p3: proper#(U81(X)) -> proper#(X) p4: proper#(isPal(X)) -> proper#(X) p5: proper#(U72(X)) -> proper#(X) p6: proper#(U71(X1,X2)) -> proper#(X2) p7: proper#(U71(X1,X2)) -> proper#(X1) p8: proper#(U61(X)) -> proper#(X) p9: proper#(U52(X)) -> proper#(X) p10: proper#(U51(X1,X2)) -> proper#(X2) p11: proper#(U51(X1,X2)) -> proper#(X1) p12: proper#(isNeList(X)) -> proper#(X) p13: proper#(U42(X)) -> proper#(X) p14: proper#(U41(X1,X2)) -> proper#(X2) p15: proper#(U41(X1,X2)) -> proper#(X1) p16: proper#(U31(X)) -> proper#(X) p17: proper#(isList(X)) -> proper#(X) p18: proper#(U22(X)) -> proper#(X) p19: proper#(U21(X1,X2)) -> proper#(X2) p20: proper#(U21(X1,X2)) -> proper#(X1) p21: proper#(U11(X)) -> proper#(X) p22: proper#(__(X1,X2)) -> proper#(X2) p23: proper#(__(X1,X2)) -> proper#(X1) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: proper#_A(x1) = x1 isNePal_A(x1) = ((1,1),(1,1)) x1 + (1,1) isQid_A(x1) = ((1,1),(1,1)) x1 + (1,1) U81_A(x1) = ((1,1),(1,1)) x1 + (1,1) isPal_A(x1) = ((1,1),(1,1)) x1 + (1,1) U72_A(x1) = ((1,1),(1,1)) x1 + (1,1) U71_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U61_A(x1) = ((1,1),(1,1)) x1 + (1,1) U52_A(x1) = ((1,1),(1,1)) x1 + (1,1) U51_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) isNeList_A(x1) = ((1,1),(1,1)) x1 + (1,1) U42_A(x1) = ((1,1),(1,1)) x1 + (1,1) U41_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U31_A(x1) = ((1,1),(1,1)) x1 + (1,1) isList_A(x1) = ((1,1),(1,1)) x1 + (1,1) U22_A(x1) = ((1,1),(1,1)) x1 + (1,1) U21_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U11_A(x1) = ((1,1),(1,1)) x1 + (1,1) ___A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: proper#_A(x1) = ((1,1),(1,1)) x1 isNePal_A(x1) = ((1,1),(0,1)) x1 + (1,1) isQid_A(x1) = ((1,0),(1,0)) x1 + (1,1) U81_A(x1) = ((1,1),(1,1)) x1 + (1,1) isPal_A(x1) = ((0,1),(1,1)) x1 + (1,1) U72_A(x1) = ((1,1),(1,1)) x1 + (1,1) U71_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U61_A(x1) = ((1,1),(1,1)) x1 + (1,1) U52_A(x1) = ((1,1),(1,1)) x1 + (1,1) U51_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) isNeList_A(x1) = ((1,1),(1,1)) x1 + (1,1) U42_A(x1) = ((0,1),(1,1)) x1 + (1,1) U41_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U31_A(x1) = ((1,1),(1,1)) x1 + (1,1) isList_A(x1) = ((1,1),(1,1)) x1 + (1,1) U22_A(x1) = ((1,1),(1,1)) x1 + (1,1) U21_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) U11_A(x1) = ((1,1),(1,1)) x1 + (1,1) ___A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23 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(X1),X2) -> __#(X1,X2) p2: __#(ok(X1),ok(X2)) -> __#(X1,X2) p3: __#(X1,mark(X2)) -> __#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: __#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: __#_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((0,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2, p3 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U22#(mark(X)) -> U22#(X) p2: U22#(ok(X)) -> U22#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U22#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U22#_A(x1) = ((0,1),(1,1)) x1 mark_A(x1) = ((1,0),(1,1)) x1 + (1,1) ok_A(x1) = ((0,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isList#(ok(X)) -> isList#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isList#_A(x1) = ((1,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isList#_A(x1) = ((0,1),(1,1)) x1 ok_A(x1) = ((1,0),(1,1)) x1 + (1,1) 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: U42#(mark(X)) -> U42#(X) p2: U42#(ok(X)) -> U42#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U42#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U42#_A(x1) = ((1,1),(0,1)) x1 mark_A(x1) = ((0,0),(1,0)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(ok(X)) -> isNeList#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = ((1,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = ((0,1),(1,1)) x1 ok_A(x1) = ((1,0),(1,1)) x1 + (1,1) 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: U52#(mark(X)) -> U52#(X) p2: U52#(ok(X)) -> U52#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U52#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U52#_A(x1) = ((0,1),(1,1)) x1 mark_A(x1) = ((0,0),(1,0)) x1 + (1,1) ok_A(x1) = ((0,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U72#(mark(X)) -> U72#(X) p2: U72#(ok(X)) -> U72#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U72#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U72#_A(x1) = ((1,1),(0,1)) x1 mark_A(x1) = x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(ok(X)) -> isPal#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isPal#_A(x1) = ((1,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isPal#_A(x1) = ((0,0),(1,0)) x1 ok_A(x1) = ((1,1),(0,0)) x1 + (1,1) 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: U11#(mark(X)) -> U11#(X) p2: U11#(ok(X)) -> U11#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U11#_A(x1) = ((1,1),(0,1)) x1 mark_A(x1) = ((1,0),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 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, r101, r102, r103 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: U21#(mark(X1),X2) -> U21#(X1,X2) p2: U21#(ok(X1),ok(X2)) -> U21#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U21#_A(x1,x2) = ((1,0),(1,0)) x1 + ((0,1),(1,1)) x2 mark_A(x1) = ((1,1),(0,0)) x1 + (1,1) ok_A(x1) = ((1,1),(0,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U31#(mark(X)) -> U31#(X) p2: U31#(ok(X)) -> U31#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U31#_A(x1) = ((0,1),(1,0)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U31#_A(x1) = (0,0) mark_A(x1) = (1,1) ok_A(x1) = (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isQid#(ok(X)) -> isQid#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isQid#_A(x1) = ((1,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isQid#_A(x1) = ((0,1),(1,1)) x1 ok_A(x1) = ((1,0),(1,1)) x1 + (1,1) 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: U41#(mark(X1),X2) -> U41#(X1,X2) p2: U41#(ok(X1),ok(X2)) -> U41#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U41#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(0,0)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U41#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,1),(1,1)) x2 mark_A(x1) = ((1,1),(0,0)) x1 + (1,1) ok_A(x1) = x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U51#(mark(X1),X2) -> U51#(X1,X2) p2: U51#(ok(X1),ok(X2)) -> U51#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U51#_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U51#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,1)) x2 mark_A(x1) = ((0,1),(0,0)) x1 + (1,0) ok_A(x1) = ((1,0),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U61#(mark(X)) -> U61#(X) p2: U61#(ok(X)) -> U61#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U61#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U61#_A(x1) = ((0,1),(1,1)) x1 mark_A(x1) = ((0,1),(1,0)) x1 + (1,1) ok_A(x1) = ((0,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U71#(mark(X1),X2) -> U71#(X1,X2) p2: U71#(ok(X1),ok(X2)) -> U71#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U71#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(0,0)) x2 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U71#_A(x1,x2) = x1 + ((0,0),(1,1)) x2 mark_A(x1) = ((0,0),(1,0)) x1 + (1,1) ok_A(x1) = ((0,0),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U81#(mark(X)) -> U81#(X) p2: U81#(ok(X)) -> U81#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: U81#_A(x1) = ((1,1),(1,1)) x1 mark_A(x1) = ((1,1),(1,1)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: U81#_A(x1) = ((1,1),(0,1)) x1 mark_A(x1) = ((0,1),(1,0)) x1 + (1,1) ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNePal#(ok(X)) -> isNePal#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(U11(tt())) -> mark(tt()) r5: active(U21(tt(),V2)) -> mark(U22(isList(V2))) r6: active(U22(tt())) -> mark(tt()) r7: active(U31(tt())) -> mark(tt()) r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2))) r9: active(U42(tt())) -> mark(tt()) r10: active(U51(tt(),V2)) -> mark(U52(isList(V2))) r11: active(U52(tt())) -> mark(tt()) r12: active(U61(tt())) -> mark(tt()) r13: active(U71(tt(),P)) -> mark(U72(isPal(P))) r14: active(U72(tt())) -> mark(tt()) r15: active(U81(tt())) -> mark(tt()) r16: active(isList(V)) -> mark(U11(isNeList(V))) r17: active(isList(nil())) -> mark(tt()) r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) r19: active(isNeList(V)) -> mark(U31(isQid(V))) r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) r22: active(isNePal(V)) -> mark(U61(isQid(V))) r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) r24: active(isPal(V)) -> mark(U81(isNePal(V))) r25: active(isPal(nil())) -> mark(tt()) r26: active(isQid(a())) -> mark(tt()) r27: active(isQid(e())) -> mark(tt()) r28: active(isQid(i())) -> mark(tt()) r29: active(isQid(o())) -> mark(tt()) r30: active(isQid(u())) -> mark(tt()) r31: active(__(X1,X2)) -> __(active(X1),X2) r32: active(__(X1,X2)) -> __(X1,active(X2)) r33: active(U11(X)) -> U11(active(X)) r34: active(U21(X1,X2)) -> U21(active(X1),X2) r35: active(U22(X)) -> U22(active(X)) r36: active(U31(X)) -> U31(active(X)) r37: active(U41(X1,X2)) -> U41(active(X1),X2) r38: active(U42(X)) -> U42(active(X)) r39: active(U51(X1,X2)) -> U51(active(X1),X2) r40: active(U52(X)) -> U52(active(X)) r41: active(U61(X)) -> U61(active(X)) r42: active(U71(X1,X2)) -> U71(active(X1),X2) r43: active(U72(X)) -> U72(active(X)) r44: active(U81(X)) -> U81(active(X)) r45: __(mark(X1),X2) -> mark(__(X1,X2)) r46: __(X1,mark(X2)) -> mark(__(X1,X2)) r47: U11(mark(X)) -> mark(U11(X)) r48: U21(mark(X1),X2) -> mark(U21(X1,X2)) r49: U22(mark(X)) -> mark(U22(X)) r50: U31(mark(X)) -> mark(U31(X)) r51: U41(mark(X1),X2) -> mark(U41(X1,X2)) r52: U42(mark(X)) -> mark(U42(X)) r53: U51(mark(X1),X2) -> mark(U51(X1,X2)) r54: U52(mark(X)) -> mark(U52(X)) r55: U61(mark(X)) -> mark(U61(X)) r56: U71(mark(X1),X2) -> mark(U71(X1,X2)) r57: U72(mark(X)) -> mark(U72(X)) r58: U81(mark(X)) -> mark(U81(X)) r59: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r60: proper(nil()) -> ok(nil()) r61: proper(U11(X)) -> U11(proper(X)) r62: proper(tt()) -> ok(tt()) r63: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) r64: proper(U22(X)) -> U22(proper(X)) r65: proper(isList(X)) -> isList(proper(X)) r66: proper(U31(X)) -> U31(proper(X)) r67: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) r68: proper(U42(X)) -> U42(proper(X)) r69: proper(isNeList(X)) -> isNeList(proper(X)) r70: proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) r71: proper(U52(X)) -> U52(proper(X)) r72: proper(U61(X)) -> U61(proper(X)) r73: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) r74: proper(U72(X)) -> U72(proper(X)) r75: proper(isPal(X)) -> isPal(proper(X)) r76: proper(U81(X)) -> U81(proper(X)) r77: proper(isQid(X)) -> isQid(proper(X)) r78: proper(isNePal(X)) -> isNePal(proper(X)) r79: proper(a()) -> ok(a()) r80: proper(e()) -> ok(e()) r81: proper(i()) -> ok(i()) r82: proper(o()) -> ok(o()) r83: proper(u()) -> ok(u()) r84: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r85: U11(ok(X)) -> ok(U11(X)) r86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) r87: U22(ok(X)) -> ok(U22(X)) r88: isList(ok(X)) -> ok(isList(X)) r89: U31(ok(X)) -> ok(U31(X)) r90: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) r91: U42(ok(X)) -> ok(U42(X)) r92: isNeList(ok(X)) -> ok(isNeList(X)) r93: U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) r94: U52(ok(X)) -> ok(U52(X)) r95: U61(ok(X)) -> ok(U61(X)) r96: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) r97: U72(ok(X)) -> ok(U72(X)) r98: isPal(ok(X)) -> ok(isPal(X)) r99: U81(ok(X)) -> ok(U81(X)) r100: isQid(ok(X)) -> ok(isQid(X)) r101: isNePal(ok(X)) -> ok(isNePal(X)) r102: top(mark(X)) -> top(proper(X)) r103: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isNePal#_A(x1) = ((1,1),(1,1)) x1 ok_A(x1) = ((1,1),(1,1)) x1 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isNePal#_A(x1) = ((0,1),(1,1)) x1 ok_A(x1) = ((1,0),(1,1)) x1 + (1,1) The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.