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