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