YES proof of Transformed_CSR_04_PALINDROME_complete_noand_iGM.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished Termination w.r.t. Q of the given QTRS could be proven: (0) QTRS (1) QTRSRRRProof [EQUIVALENT, 869 ms] (2) QTRS (3) QTRSRRRProof [EQUIVALENT, 148 ms] (4) QTRS (5) QTRSRRRProof [EQUIVALENT, 151 ms] (6) QTRS (7) QTRSRRRProof [EQUIVALENT, 0 ms] (8) QTRS (9) RisEmptyProof [EQUIVALENT, 0 ms] (10) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) active(__(X, nil)) -> mark(X) active(__(nil, X)) -> mark(X) active(U11(tt, V)) -> mark(U12(isPalListKind(V), V)) active(U12(tt, V)) -> mark(U13(isNeList(V))) active(U13(tt)) -> mark(tt) active(U21(tt, V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) active(U22(tt, V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) active(U23(tt, V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) active(U24(tt, V1, V2)) -> mark(U25(isList(V1), V2)) active(U25(tt, V2)) -> mark(U26(isList(V2))) active(U26(tt)) -> mark(tt) active(U31(tt, V)) -> mark(U32(isPalListKind(V), V)) active(U32(tt, V)) -> mark(U33(isQid(V))) active(U33(tt)) -> mark(tt) active(U41(tt, V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) active(U42(tt, V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) active(U43(tt, V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) active(U44(tt, V1, V2)) -> mark(U45(isList(V1), V2)) active(U45(tt, V2)) -> mark(U46(isNeList(V2))) active(U46(tt)) -> mark(tt) active(U51(tt, V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) active(U52(tt, V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) active(U53(tt, V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) active(U54(tt, V1, V2)) -> mark(U55(isNeList(V1), V2)) active(U55(tt, V2)) -> mark(U56(isList(V2))) active(U56(tt)) -> mark(tt) active(U61(tt, V)) -> mark(U62(isPalListKind(V), V)) active(U62(tt, V)) -> mark(U63(isQid(V))) active(U63(tt)) -> mark(tt) active(U71(tt, I, P)) -> mark(U72(isPalListKind(I), P)) active(U72(tt, P)) -> mark(U73(isPal(P), P)) active(U73(tt, P)) -> mark(U74(isPalListKind(P))) active(U74(tt)) -> mark(tt) active(U81(tt, V)) -> mark(U82(isPalListKind(V), V)) active(U82(tt, V)) -> mark(U83(isNePal(V))) active(U83(tt)) -> mark(tt) active(U91(tt, V2)) -> mark(U92(isPalListKind(V2))) active(U92(tt)) -> mark(tt) active(isList(V)) -> mark(U11(isPalListKind(V), V)) active(isList(nil)) -> mark(tt) active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) active(isPal(V)) -> mark(U81(isPalListKind(V), V)) active(isPal(nil)) -> mark(tt) active(isPalListKind(a)) -> mark(tt) active(isPalListKind(e)) -> mark(tt) active(isPalListKind(i)) -> mark(tt) active(isPalListKind(nil)) -> mark(tt) active(isPalListKind(o)) -> mark(tt) active(isPalListKind(u)) -> mark(tt) active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) active(isQid(a)) -> mark(tt) active(isQid(e)) -> mark(tt) active(isQid(i)) -> mark(tt) active(isQid(o)) -> mark(tt) active(isQid(u)) -> mark(tt) mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) mark(nil) -> active(nil) mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) mark(tt) -> active(tt) mark(U12(X1, X2)) -> active(U12(mark(X1), X2)) mark(isPalListKind(X)) -> active(isPalListKind(X)) mark(U13(X)) -> active(U13(mark(X))) mark(isNeList(X)) -> active(isNeList(X)) mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)) mark(U22(X1, X2, X3)) -> active(U22(mark(X1), X2, X3)) mark(U23(X1, X2, X3)) -> active(U23(mark(X1), X2, X3)) mark(U24(X1, X2, X3)) -> active(U24(mark(X1), X2, X3)) mark(U25(X1, X2)) -> active(U25(mark(X1), X2)) mark(isList(X)) -> active(isList(X)) mark(U26(X)) -> active(U26(mark(X))) mark(U31(X1, X2)) -> active(U31(mark(X1), X2)) mark(U32(X1, X2)) -> active(U32(mark(X1), X2)) mark(U33(X)) -> active(U33(mark(X))) mark(isQid(X)) -> active(isQid(X)) mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)) mark(U42(X1, X2, X3)) -> active(U42(mark(X1), X2, X3)) mark(U43(X1, X2, X3)) -> active(U43(mark(X1), X2, X3)) mark(U44(X1, X2, X3)) -> active(U44(mark(X1), X2, X3)) mark(U45(X1, X2)) -> active(U45(mark(X1), X2)) mark(U46(X)) -> active(U46(mark(X))) mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)) mark(U52(X1, X2, X3)) -> active(U52(mark(X1), X2, X3)) mark(U53(X1, X2, X3)) -> active(U53(mark(X1), X2, X3)) mark(U54(X1, X2, X3)) -> active(U54(mark(X1), X2, X3)) mark(U55(X1, X2)) -> active(U55(mark(X1), X2)) mark(U56(X)) -> active(U56(mark(X))) mark(U61(X1, X2)) -> active(U61(mark(X1), X2)) mark(U62(X1, X2)) -> active(U62(mark(X1), X2)) mark(U63(X)) -> active(U63(mark(X))) mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)) mark(U72(X1, X2)) -> active(U72(mark(X1), X2)) mark(U73(X1, X2)) -> active(U73(mark(X1), X2)) mark(isPal(X)) -> active(isPal(X)) mark(U74(X)) -> active(U74(mark(X))) mark(U81(X1, X2)) -> active(U81(mark(X1), X2)) mark(U82(X1, X2)) -> active(U82(mark(X1), X2)) mark(U83(X)) -> active(U83(mark(X))) mark(isNePal(X)) -> active(isNePal(X)) mark(U91(X1, X2)) -> active(U91(mark(X1), X2)) mark(U92(X)) -> active(U92(mark(X))) mark(a) -> active(a) mark(e) -> active(e) mark(i) -> active(i) mark(o) -> active(o) mark(u) -> active(u) __(mark(X1), X2) -> __(X1, X2) __(X1, mark(X2)) -> __(X1, X2) __(active(X1), X2) -> __(X1, X2) __(X1, active(X2)) -> __(X1, X2) U11(mark(X1), X2) -> U11(X1, X2) U11(X1, mark(X2)) -> U11(X1, X2) U11(active(X1), X2) -> U11(X1, X2) U11(X1, active(X2)) -> U11(X1, X2) U12(mark(X1), X2) -> U12(X1, X2) U12(X1, mark(X2)) -> U12(X1, X2) U12(active(X1), X2) -> U12(X1, X2) U12(X1, active(X2)) -> U12(X1, X2) isPalListKind(mark(X)) -> isPalListKind(X) isPalListKind(active(X)) -> isPalListKind(X) U13(mark(X)) -> U13(X) U13(active(X)) -> U13(X) isNeList(mark(X)) -> isNeList(X) isNeList(active(X)) -> isNeList(X) U21(mark(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, mark(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, mark(X3)) -> U21(X1, X2, X3) U21(active(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, active(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, active(X3)) -> U21(X1, X2, X3) U22(mark(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, mark(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, mark(X3)) -> U22(X1, X2, X3) U22(active(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, active(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, active(X3)) -> U22(X1, X2, X3) U23(mark(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, mark(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, mark(X3)) -> U23(X1, X2, X3) U23(active(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, active(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, active(X3)) -> U23(X1, X2, X3) U24(mark(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, mark(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, mark(X3)) -> U24(X1, X2, X3) U24(active(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, active(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, active(X3)) -> U24(X1, X2, X3) U25(mark(X1), X2) -> U25(X1, X2) U25(X1, mark(X2)) -> U25(X1, X2) U25(active(X1), X2) -> U25(X1, X2) U25(X1, active(X2)) -> U25(X1, X2) isList(mark(X)) -> isList(X) isList(active(X)) -> isList(X) U26(mark(X)) -> U26(X) U26(active(X)) -> U26(X) U31(mark(X1), X2) -> U31(X1, X2) U31(X1, mark(X2)) -> U31(X1, X2) U31(active(X1), X2) -> U31(X1, X2) U31(X1, active(X2)) -> U31(X1, X2) U32(mark(X1), X2) -> U32(X1, X2) U32(X1, mark(X2)) -> U32(X1, X2) U32(active(X1), X2) -> U32(X1, X2) U32(X1, active(X2)) -> U32(X1, X2) U33(mark(X)) -> U33(X) U33(active(X)) -> U33(X) isQid(mark(X)) -> isQid(X) isQid(active(X)) -> isQid(X) U41(mark(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, mark(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, mark(X3)) -> U41(X1, X2, X3) U41(active(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, active(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, active(X3)) -> U41(X1, X2, X3) U42(mark(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, mark(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, mark(X3)) -> U42(X1, X2, X3) U42(active(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, active(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, active(X3)) -> U42(X1, X2, X3) U43(mark(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, mark(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, mark(X3)) -> U43(X1, X2, X3) U43(active(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, active(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, active(X3)) -> U43(X1, X2, X3) U44(mark(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, mark(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, mark(X3)) -> U44(X1, X2, X3) U44(active(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, active(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, active(X3)) -> U44(X1, X2, X3) U45(mark(X1), X2) -> U45(X1, X2) U45(X1, mark(X2)) -> U45(X1, X2) U45(active(X1), X2) -> U45(X1, X2) U45(X1, active(X2)) -> U45(X1, X2) U46(mark(X)) -> U46(X) U46(active(X)) -> U46(X) U51(mark(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, mark(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, mark(X3)) -> U51(X1, X2, X3) U51(active(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, active(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, active(X3)) -> U51(X1, X2, X3) U52(mark(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, mark(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, mark(X3)) -> U52(X1, X2, X3) U52(active(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, active(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, active(X3)) -> U52(X1, X2, X3) U53(mark(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, mark(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, mark(X3)) -> U53(X1, X2, X3) U53(active(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, active(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, active(X3)) -> U53(X1, X2, X3) U54(mark(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, mark(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, mark(X3)) -> U54(X1, X2, X3) U54(active(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, active(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, active(X3)) -> U54(X1, X2, X3) U55(mark(X1), X2) -> U55(X1, X2) U55(X1, mark(X2)) -> U55(X1, X2) U55(active(X1), X2) -> U55(X1, X2) U55(X1, active(X2)) -> U55(X1, X2) U56(mark(X)) -> U56(X) U56(active(X)) -> U56(X) U61(mark(X1), X2) -> U61(X1, X2) U61(X1, mark(X2)) -> U61(X1, X2) U61(active(X1), X2) -> U61(X1, X2) U61(X1, active(X2)) -> U61(X1, X2) U62(mark(X1), X2) -> U62(X1, X2) U62(X1, mark(X2)) -> U62(X1, X2) U62(active(X1), X2) -> U62(X1, X2) U62(X1, active(X2)) -> U62(X1, X2) U63(mark(X)) -> U63(X) U63(active(X)) -> U63(X) U71(mark(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, mark(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, mark(X3)) -> U71(X1, X2, X3) U71(active(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, active(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, active(X3)) -> U71(X1, X2, X3) U72(mark(X1), X2) -> U72(X1, X2) U72(X1, mark(X2)) -> U72(X1, X2) U72(active(X1), X2) -> U72(X1, X2) U72(X1, active(X2)) -> U72(X1, X2) U73(mark(X1), X2) -> U73(X1, X2) U73(X1, mark(X2)) -> U73(X1, X2) U73(active(X1), X2) -> U73(X1, X2) U73(X1, active(X2)) -> U73(X1, X2) isPal(mark(X)) -> isPal(X) isPal(active(X)) -> isPal(X) U74(mark(X)) -> U74(X) U74(active(X)) -> U74(X) U81(mark(X1), X2) -> U81(X1, X2) U81(X1, mark(X2)) -> U81(X1, X2) U81(active(X1), X2) -> U81(X1, X2) U81(X1, active(X2)) -> U81(X1, X2) U82(mark(X1), X2) -> U82(X1, X2) U82(X1, mark(X2)) -> U82(X1, X2) U82(active(X1), X2) -> U82(X1, X2) U82(X1, active(X2)) -> U82(X1, X2) U83(mark(X)) -> U83(X) U83(active(X)) -> U83(X) isNePal(mark(X)) -> isNePal(X) isNePal(active(X)) -> isNePal(X) U91(mark(X1), X2) -> U91(X1, X2) U91(X1, mark(X2)) -> U91(X1, X2) U91(active(X1), X2) -> U91(X1, X2) U91(X1, active(X2)) -> U91(X1, X2) U92(mark(X)) -> U92(X) U92(active(X)) -> U92(X) Q is empty. ---------------------------------------- (1) QTRSRRRProof (EQUIVALENT) Used ordering: active/1)YES( __/2(YES,YES) mark/1)YES( nil/0) U11/2(YES,YES) tt/0) U12/2(YES,YES) isPalListKind/1)YES( U13/1(YES) isNeList/1(YES) U21/3(YES,YES,YES) U22/3(YES,YES,YES) U23/3(YES,YES,YES) U24/3(YES,YES,YES) U25/2(YES,YES) isList/1(YES) U26/1(YES) U31/2(YES,YES) U32/2(YES,YES) U33/1(YES) isQid/1)YES( U41/3(YES,YES,YES) U42/3(YES,YES,YES) U43/3(YES,YES,YES) U44/3(YES,YES,YES) U45/2(YES,YES) U46/1(YES) U51/3(YES,YES,YES) U52/3(YES,YES,YES) U53/3(YES,YES,YES) U54/3(YES,YES,YES) U55/2(YES,YES) U56/1(YES) U61/2(YES,YES) U62/2(YES,YES) U63/1)YES( U71/3(YES,YES,YES) U72/2(YES,YES) U73/2(YES,YES) isPal/1(YES) U74/1(YES) U81/2(YES,YES) U82/2(YES,YES) U83/1(YES) isNePal/1(YES) U91/2(YES,YES) U92/1)YES( a/0) e/0) i/0) o/0) u/0) Quasi precedence: ___2 > U21_3 > U22_3 > U23_3 > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U21_3 > U22_3 > U23_3 > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U41_3 > U42_3 > U43_3 > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U41_3 > U42_3 > U43_3 > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U41_3 > U42_3 > U43_3 > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U41_3 > U42_3 > U43_3 > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U41_3 > U42_3 > U43_3 > U44_3 > U45_2 > U46_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U51_3 > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U51_3 > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U51_3 > U52_3 > U53_3 > U54_3 > U55_2 > U56_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U71_3 > [U72_2, isPal_1] > U81_2 > U82_2 > U83_1 > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U71_3 > [U72_2, isPal_1] > U81_2 > U82_2 > isNePal_1 > U61_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] ___2 > U91_2 > [U32_2, U33_1, U62_2, U73_2, U74_1] nil > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] a > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] i > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] o > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] u > [tt, e] > U26_1 > [U32_2, U33_1, U62_2, U73_2, U74_1] Status: ___2: [1,2] nil: multiset status U11_2: [2,1] tt: multiset status U12_2: multiset status U13_1: multiset status isNeList_1: multiset status U21_3: [2,3,1] U22_3: [1,3,2] U23_3: [1,2,3] U24_3: [2,1,3] U25_2: multiset status isList_1: multiset status U26_1: multiset status U31_2: [2,1] U32_2: [2,1] U33_1: [1] U41_3: [3,1,2] U42_3: [1,3,2] U43_3: [1,2,3] U44_3: [2,3,1] U45_2: [1,2] U46_1: [1] U51_3: [2,3,1] U52_3: [3,1,2] U53_3: [2,3,1] U54_3: [1,3,2] U55_2: [2,1] U56_1: [1] U61_2: [2,1] U62_2: [1,2] U71_3: [1,3,2] U72_2: multiset status U73_2: multiset status isPal_1: multiset status U74_1: multiset status U81_2: [2,1] U82_2: multiset status U83_1: multiset status isNePal_1: multiset status U91_2: multiset status a: multiset status e: multiset status i: multiset status o: multiset status u: multiset status With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) active(__(X, nil)) -> mark(X) active(__(nil, X)) -> mark(X) active(U11(tt, V)) -> mark(U12(isPalListKind(V), V)) active(U12(tt, V)) -> mark(U13(isNeList(V))) active(U13(tt)) -> mark(tt) active(U21(tt, V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) active(U22(tt, V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) active(U23(tt, V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) active(U24(tt, V1, V2)) -> mark(U25(isList(V1), V2)) active(U25(tt, V2)) -> mark(U26(isList(V2))) active(U26(tt)) -> mark(tt) active(U31(tt, V)) -> mark(U32(isPalListKind(V), V)) active(U32(tt, V)) -> mark(U33(isQid(V))) active(U33(tt)) -> mark(tt) active(U41(tt, V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) active(U42(tt, V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) active(U43(tt, V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) active(U44(tt, V1, V2)) -> mark(U45(isList(V1), V2)) active(U45(tt, V2)) -> mark(U46(isNeList(V2))) active(U46(tt)) -> mark(tt) active(U51(tt, V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) active(U52(tt, V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) active(U53(tt, V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) active(U54(tt, V1, V2)) -> mark(U55(isNeList(V1), V2)) active(U55(tt, V2)) -> mark(U56(isList(V2))) active(U56(tt)) -> mark(tt) active(U61(tt, V)) -> mark(U62(isPalListKind(V), V)) active(U62(tt, V)) -> mark(U63(isQid(V))) active(U71(tt, I, P)) -> mark(U72(isPalListKind(I), P)) active(U72(tt, P)) -> mark(U73(isPal(P), P)) active(U73(tt, P)) -> mark(U74(isPalListKind(P))) active(U74(tt)) -> mark(tt) active(U81(tt, V)) -> mark(U82(isPalListKind(V), V)) active(U82(tt, V)) -> mark(U83(isNePal(V))) active(U83(tt)) -> mark(tt) active(U91(tt, V2)) -> mark(U92(isPalListKind(V2))) active(isList(V)) -> mark(U11(isPalListKind(V), V)) active(isList(nil)) -> mark(tt) active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) active(isPal(V)) -> mark(U81(isPalListKind(V), V)) active(isPal(nil)) -> mark(tt) active(isPalListKind(a)) -> mark(tt) active(isPalListKind(i)) -> mark(tt) active(isPalListKind(nil)) -> mark(tt) active(isPalListKind(o)) -> mark(tt) active(isPalListKind(u)) -> mark(tt) active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) active(isQid(a)) -> mark(tt) active(isQid(i)) -> mark(tt) active(isQid(o)) -> mark(tt) active(isQid(u)) -> mark(tt) ---------------------------------------- (2) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: active(U63(tt)) -> mark(tt) active(U92(tt)) -> mark(tt) active(isPalListKind(e)) -> mark(tt) active(isQid(e)) -> mark(tt) mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) mark(nil) -> active(nil) mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) mark(tt) -> active(tt) mark(U12(X1, X2)) -> active(U12(mark(X1), X2)) mark(isPalListKind(X)) -> active(isPalListKind(X)) mark(U13(X)) -> active(U13(mark(X))) mark(isNeList(X)) -> active(isNeList(X)) mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)) mark(U22(X1, X2, X3)) -> active(U22(mark(X1), X2, X3)) mark(U23(X1, X2, X3)) -> active(U23(mark(X1), X2, X3)) mark(U24(X1, X2, X3)) -> active(U24(mark(X1), X2, X3)) mark(U25(X1, X2)) -> active(U25(mark(X1), X2)) mark(isList(X)) -> active(isList(X)) mark(U26(X)) -> active(U26(mark(X))) mark(U31(X1, X2)) -> active(U31(mark(X1), X2)) mark(U32(X1, X2)) -> active(U32(mark(X1), X2)) mark(U33(X)) -> active(U33(mark(X))) mark(isQid(X)) -> active(isQid(X)) mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)) mark(U42(X1, X2, X3)) -> active(U42(mark(X1), X2, X3)) mark(U43(X1, X2, X3)) -> active(U43(mark(X1), X2, X3)) mark(U44(X1, X2, X3)) -> active(U44(mark(X1), X2, X3)) mark(U45(X1, X2)) -> active(U45(mark(X1), X2)) mark(U46(X)) -> active(U46(mark(X))) mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)) mark(U52(X1, X2, X3)) -> active(U52(mark(X1), X2, X3)) mark(U53(X1, X2, X3)) -> active(U53(mark(X1), X2, X3)) mark(U54(X1, X2, X3)) -> active(U54(mark(X1), X2, X3)) mark(U55(X1, X2)) -> active(U55(mark(X1), X2)) mark(U56(X)) -> active(U56(mark(X))) mark(U61(X1, X2)) -> active(U61(mark(X1), X2)) mark(U62(X1, X2)) -> active(U62(mark(X1), X2)) mark(U63(X)) -> active(U63(mark(X))) mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)) mark(U72(X1, X2)) -> active(U72(mark(X1), X2)) mark(U73(X1, X2)) -> active(U73(mark(X1), X2)) mark(isPal(X)) -> active(isPal(X)) mark(U74(X)) -> active(U74(mark(X))) mark(U81(X1, X2)) -> active(U81(mark(X1), X2)) mark(U82(X1, X2)) -> active(U82(mark(X1), X2)) mark(U83(X)) -> active(U83(mark(X))) mark(isNePal(X)) -> active(isNePal(X)) mark(U91(X1, X2)) -> active(U91(mark(X1), X2)) mark(U92(X)) -> active(U92(mark(X))) mark(a) -> active(a) mark(e) -> active(e) mark(i) -> active(i) mark(o) -> active(o) mark(u) -> active(u) __(mark(X1), X2) -> __(X1, X2) __(X1, mark(X2)) -> __(X1, X2) __(active(X1), X2) -> __(X1, X2) __(X1, active(X2)) -> __(X1, X2) U11(mark(X1), X2) -> U11(X1, X2) U11(X1, mark(X2)) -> U11(X1, X2) U11(active(X1), X2) -> U11(X1, X2) U11(X1, active(X2)) -> U11(X1, X2) U12(mark(X1), X2) -> U12(X1, X2) U12(X1, mark(X2)) -> U12(X1, X2) U12(active(X1), X2) -> U12(X1, X2) U12(X1, active(X2)) -> U12(X1, X2) isPalListKind(mark(X)) -> isPalListKind(X) isPalListKind(active(X)) -> isPalListKind(X) U13(mark(X)) -> U13(X) U13(active(X)) -> U13(X) isNeList(mark(X)) -> isNeList(X) isNeList(active(X)) -> isNeList(X) U21(mark(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, mark(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, mark(X3)) -> U21(X1, X2, X3) U21(active(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, active(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, active(X3)) -> U21(X1, X2, X3) U22(mark(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, mark(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, mark(X3)) -> U22(X1, X2, X3) U22(active(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, active(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, active(X3)) -> U22(X1, X2, X3) U23(mark(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, mark(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, mark(X3)) -> U23(X1, X2, X3) U23(active(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, active(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, active(X3)) -> U23(X1, X2, X3) U24(mark(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, mark(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, mark(X3)) -> U24(X1, X2, X3) U24(active(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, active(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, active(X3)) -> U24(X1, X2, X3) U25(mark(X1), X2) -> U25(X1, X2) U25(X1, mark(X2)) -> U25(X1, X2) U25(active(X1), X2) -> U25(X1, X2) U25(X1, active(X2)) -> U25(X1, X2) isList(mark(X)) -> isList(X) isList(active(X)) -> isList(X) U26(mark(X)) -> U26(X) U26(active(X)) -> U26(X) U31(mark(X1), X2) -> U31(X1, X2) U31(X1, mark(X2)) -> U31(X1, X2) U31(active(X1), X2) -> U31(X1, X2) U31(X1, active(X2)) -> U31(X1, X2) U32(mark(X1), X2) -> U32(X1, X2) U32(X1, mark(X2)) -> U32(X1, X2) U32(active(X1), X2) -> U32(X1, X2) U32(X1, active(X2)) -> U32(X1, X2) U33(mark(X)) -> U33(X) U33(active(X)) -> U33(X) isQid(mark(X)) -> isQid(X) isQid(active(X)) -> isQid(X) U41(mark(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, mark(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, mark(X3)) -> U41(X1, X2, X3) U41(active(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, active(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, active(X3)) -> U41(X1, X2, X3) U42(mark(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, mark(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, mark(X3)) -> U42(X1, X2, X3) U42(active(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, active(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, active(X3)) -> U42(X1, X2, X3) U43(mark(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, mark(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, mark(X3)) -> U43(X1, X2, X3) U43(active(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, active(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, active(X3)) -> U43(X1, X2, X3) U44(mark(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, mark(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, mark(X3)) -> U44(X1, X2, X3) U44(active(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, active(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, active(X3)) -> U44(X1, X2, X3) U45(mark(X1), X2) -> U45(X1, X2) U45(X1, mark(X2)) -> U45(X1, X2) U45(active(X1), X2) -> U45(X1, X2) U45(X1, active(X2)) -> U45(X1, X2) U46(mark(X)) -> U46(X) U46(active(X)) -> U46(X) U51(mark(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, mark(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, mark(X3)) -> U51(X1, X2, X3) U51(active(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, active(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, active(X3)) -> U51(X1, X2, X3) U52(mark(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, mark(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, mark(X3)) -> U52(X1, X2, X3) U52(active(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, active(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, active(X3)) -> U52(X1, X2, X3) U53(mark(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, mark(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, mark(X3)) -> U53(X1, X2, X3) U53(active(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, active(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, active(X3)) -> U53(X1, X2, X3) U54(mark(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, mark(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, mark(X3)) -> U54(X1, X2, X3) U54(active(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, active(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, active(X3)) -> U54(X1, X2, X3) U55(mark(X1), X2) -> U55(X1, X2) U55(X1, mark(X2)) -> U55(X1, X2) U55(active(X1), X2) -> U55(X1, X2) U55(X1, active(X2)) -> U55(X1, X2) U56(mark(X)) -> U56(X) U56(active(X)) -> U56(X) U61(mark(X1), X2) -> U61(X1, X2) U61(X1, mark(X2)) -> U61(X1, X2) U61(active(X1), X2) -> U61(X1, X2) U61(X1, active(X2)) -> U61(X1, X2) U62(mark(X1), X2) -> U62(X1, X2) U62(X1, mark(X2)) -> U62(X1, X2) U62(active(X1), X2) -> U62(X1, X2) U62(X1, active(X2)) -> U62(X1, X2) U63(mark(X)) -> U63(X) U63(active(X)) -> U63(X) U71(mark(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, mark(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, mark(X3)) -> U71(X1, X2, X3) U71(active(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, active(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, active(X3)) -> U71(X1, X2, X3) U72(mark(X1), X2) -> U72(X1, X2) U72(X1, mark(X2)) -> U72(X1, X2) U72(active(X1), X2) -> U72(X1, X2) U72(X1, active(X2)) -> U72(X1, X2) U73(mark(X1), X2) -> U73(X1, X2) U73(X1, mark(X2)) -> U73(X1, X2) U73(active(X1), X2) -> U73(X1, X2) U73(X1, active(X2)) -> U73(X1, X2) isPal(mark(X)) -> isPal(X) isPal(active(X)) -> isPal(X) U74(mark(X)) -> U74(X) U74(active(X)) -> U74(X) U81(mark(X1), X2) -> U81(X1, X2) U81(X1, mark(X2)) -> U81(X1, X2) U81(active(X1), X2) -> U81(X1, X2) U81(X1, active(X2)) -> U81(X1, X2) U82(mark(X1), X2) -> U82(X1, X2) U82(X1, mark(X2)) -> U82(X1, X2) U82(active(X1), X2) -> U82(X1, X2) U82(X1, active(X2)) -> U82(X1, X2) U83(mark(X)) -> U83(X) U83(active(X)) -> U83(X) isNePal(mark(X)) -> isNePal(X) isNePal(active(X)) -> isNePal(X) U91(mark(X1), X2) -> U91(X1, X2) U91(X1, mark(X2)) -> U91(X1, X2) U91(active(X1), X2) -> U91(X1, X2) U91(X1, active(X2)) -> U91(X1, X2) U92(mark(X)) -> U92(X) U92(active(X)) -> U92(X) Q is empty. ---------------------------------------- (3) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1, x_2)) = 1 + x_1 + x_2 POL(U12(x_1, x_2)) = 1 + x_1 + x_2 POL(U13(x_1)) = 1 + x_1 POL(U21(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U22(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U23(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U24(x_1, x_2, x_3)) = 1 + x_1 + x_2 + 2*x_3 POL(U25(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(U26(x_1)) = 2 + x_1 POL(U31(x_1, x_2)) = 1 + x_1 + x_2 POL(U32(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(U33(x_1)) = 1 + x_1 POL(U41(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U42(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + 2*x_3 POL(U43(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + x_3 POL(U44(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + 2*x_3 POL(U45(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(U46(x_1)) = 1 + x_1 POL(U51(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + x_3 POL(U52(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U53(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + x_3 POL(U54(x_1, x_2, x_3)) = 1 + x_1 + 2*x_2 + x_3 POL(U55(x_1, x_2)) = 1 + x_1 + x_2 POL(U56(x_1)) = 1 + 2*x_1 POL(U61(x_1, x_2)) = 1 + x_1 + x_2 POL(U62(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(U63(x_1)) = 1 + x_1 POL(U71(x_1, x_2, x_3)) = 1 + 2*x_1 + x_2 + x_3 POL(U72(x_1, x_2)) = 1 + x_1 + x_2 POL(U73(x_1, x_2)) = 1 + 2*x_1 + x_2 POL(U74(x_1)) = 1 + x_1 POL(U81(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(U82(x_1, x_2)) = 1 + 2*x_1 + 2*x_2 POL(U83(x_1)) = 1 + x_1 POL(U91(x_1, x_2)) = 1 + 2*x_1 + x_2 POL(U92(x_1)) = 1 + x_1 POL(__(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 POL(a) = 1 POL(active(x_1)) = 1 + x_1 POL(e) = 2 POL(i) = 2 POL(isList(x_1)) = 1 + 2*x_1 POL(isNeList(x_1)) = 1 + x_1 POL(isNePal(x_1)) = 2 + x_1 POL(isPal(x_1)) = 2 + x_1 POL(isPalListKind(x_1)) = 2 + x_1 POL(isQid(x_1)) = 2 + x_1 POL(mark(x_1)) = 2*x_1 POL(nil) = 1 POL(o) = 2 POL(tt) = 2 POL(u) = 1 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: active(isPalListKind(e)) -> mark(tt) active(isQid(e)) -> mark(tt) mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) mark(tt) -> active(tt) mark(isPalListKind(X)) -> active(isPalListKind(X)) mark(U26(X)) -> active(U26(mark(X))) mark(isQid(X)) -> active(isQid(X)) mark(isPal(X)) -> active(isPal(X)) mark(isNePal(X)) -> active(isNePal(X)) mark(e) -> active(e) mark(i) -> active(i) mark(o) -> active(o) __(active(X1), X2) -> __(X1, X2) __(X1, active(X2)) -> __(X1, X2) U11(active(X1), X2) -> U11(X1, X2) U11(X1, active(X2)) -> U11(X1, X2) U12(active(X1), X2) -> U12(X1, X2) U12(X1, active(X2)) -> U12(X1, X2) isPalListKind(active(X)) -> isPalListKind(X) U13(active(X)) -> U13(X) isNeList(active(X)) -> isNeList(X) U21(active(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, active(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, active(X3)) -> U21(X1, X2, X3) U22(active(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, active(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, active(X3)) -> U22(X1, X2, X3) U23(active(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, active(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, active(X3)) -> U23(X1, X2, X3) U24(active(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, active(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, active(X3)) -> U24(X1, X2, X3) U25(active(X1), X2) -> U25(X1, X2) U25(X1, active(X2)) -> U25(X1, X2) isList(active(X)) -> isList(X) U26(active(X)) -> U26(X) U31(active(X1), X2) -> U31(X1, X2) U31(X1, active(X2)) -> U31(X1, X2) U32(active(X1), X2) -> U32(X1, X2) U32(X1, active(X2)) -> U32(X1, X2) U33(active(X)) -> U33(X) isQid(active(X)) -> isQid(X) U41(active(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, active(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, active(X3)) -> U41(X1, X2, X3) U42(active(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, active(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, active(X3)) -> U42(X1, X2, X3) U43(active(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, active(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, active(X3)) -> U43(X1, X2, X3) U44(active(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, active(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, active(X3)) -> U44(X1, X2, X3) U45(active(X1), X2) -> U45(X1, X2) U45(X1, active(X2)) -> U45(X1, X2) U46(active(X)) -> U46(X) U51(active(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, active(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, active(X3)) -> U51(X1, X2, X3) U52(active(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, active(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, active(X3)) -> U52(X1, X2, X3) U53(active(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, active(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, active(X3)) -> U53(X1, X2, X3) U54(active(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, active(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, active(X3)) -> U54(X1, X2, X3) U55(active(X1), X2) -> U55(X1, X2) U55(X1, active(X2)) -> U55(X1, X2) U56(active(X)) -> U56(X) U61(active(X1), X2) -> U61(X1, X2) U61(X1, active(X2)) -> U61(X1, X2) U62(active(X1), X2) -> U62(X1, X2) U62(X1, active(X2)) -> U62(X1, X2) U63(active(X)) -> U63(X) U71(active(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, active(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, active(X3)) -> U71(X1, X2, X3) U72(active(X1), X2) -> U72(X1, X2) U72(X1, active(X2)) -> U72(X1, X2) U73(active(X1), X2) -> U73(X1, X2) U73(X1, active(X2)) -> U73(X1, X2) isPal(active(X)) -> isPal(X) U74(active(X)) -> U74(X) U81(active(X1), X2) -> U81(X1, X2) U81(X1, active(X2)) -> U81(X1, X2) U82(active(X1), X2) -> U82(X1, X2) U82(X1, active(X2)) -> U82(X1, X2) U83(active(X)) -> U83(X) isNePal(active(X)) -> isNePal(X) U91(active(X1), X2) -> U91(X1, X2) U91(X1, active(X2)) -> U91(X1, X2) U92(active(X)) -> U92(X) ---------------------------------------- (4) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: active(U63(tt)) -> mark(tt) active(U92(tt)) -> mark(tt) mark(nil) -> active(nil) mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) mark(U12(X1, X2)) -> active(U12(mark(X1), X2)) mark(U13(X)) -> active(U13(mark(X))) mark(isNeList(X)) -> active(isNeList(X)) mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)) mark(U22(X1, X2, X3)) -> active(U22(mark(X1), X2, X3)) mark(U23(X1, X2, X3)) -> active(U23(mark(X1), X2, X3)) mark(U24(X1, X2, X3)) -> active(U24(mark(X1), X2, X3)) mark(U25(X1, X2)) -> active(U25(mark(X1), X2)) mark(isList(X)) -> active(isList(X)) mark(U31(X1, X2)) -> active(U31(mark(X1), X2)) mark(U32(X1, X2)) -> active(U32(mark(X1), X2)) mark(U33(X)) -> active(U33(mark(X))) mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)) mark(U42(X1, X2, X3)) -> active(U42(mark(X1), X2, X3)) mark(U43(X1, X2, X3)) -> active(U43(mark(X1), X2, X3)) mark(U44(X1, X2, X3)) -> active(U44(mark(X1), X2, X3)) mark(U45(X1, X2)) -> active(U45(mark(X1), X2)) mark(U46(X)) -> active(U46(mark(X))) mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)) mark(U52(X1, X2, X3)) -> active(U52(mark(X1), X2, X3)) mark(U53(X1, X2, X3)) -> active(U53(mark(X1), X2, X3)) mark(U54(X1, X2, X3)) -> active(U54(mark(X1), X2, X3)) mark(U55(X1, X2)) -> active(U55(mark(X1), X2)) mark(U56(X)) -> active(U56(mark(X))) mark(U61(X1, X2)) -> active(U61(mark(X1), X2)) mark(U62(X1, X2)) -> active(U62(mark(X1), X2)) mark(U63(X)) -> active(U63(mark(X))) mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)) mark(U72(X1, X2)) -> active(U72(mark(X1), X2)) mark(U73(X1, X2)) -> active(U73(mark(X1), X2)) mark(U74(X)) -> active(U74(mark(X))) mark(U81(X1, X2)) -> active(U81(mark(X1), X2)) mark(U82(X1, X2)) -> active(U82(mark(X1), X2)) mark(U83(X)) -> active(U83(mark(X))) mark(U91(X1, X2)) -> active(U91(mark(X1), X2)) mark(U92(X)) -> active(U92(mark(X))) mark(a) -> active(a) mark(u) -> active(u) __(mark(X1), X2) -> __(X1, X2) __(X1, mark(X2)) -> __(X1, X2) U11(mark(X1), X2) -> U11(X1, X2) U11(X1, mark(X2)) -> U11(X1, X2) U12(mark(X1), X2) -> U12(X1, X2) U12(X1, mark(X2)) -> U12(X1, X2) isPalListKind(mark(X)) -> isPalListKind(X) U13(mark(X)) -> U13(X) isNeList(mark(X)) -> isNeList(X) U21(mark(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, mark(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, mark(X3)) -> U21(X1, X2, X3) U22(mark(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, mark(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, mark(X3)) -> U22(X1, X2, X3) U23(mark(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, mark(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, mark(X3)) -> U23(X1, X2, X3) U24(mark(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, mark(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, mark(X3)) -> U24(X1, X2, X3) U25(mark(X1), X2) -> U25(X1, X2) U25(X1, mark(X2)) -> U25(X1, X2) isList(mark(X)) -> isList(X) U26(mark(X)) -> U26(X) U31(mark(X1), X2) -> U31(X1, X2) U31(X1, mark(X2)) -> U31(X1, X2) U32(mark(X1), X2) -> U32(X1, X2) U32(X1, mark(X2)) -> U32(X1, X2) U33(mark(X)) -> U33(X) isQid(mark(X)) -> isQid(X) U41(mark(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, mark(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, mark(X3)) -> U41(X1, X2, X3) U42(mark(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, mark(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, mark(X3)) -> U42(X1, X2, X3) U43(mark(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, mark(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, mark(X3)) -> U43(X1, X2, X3) U44(mark(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, mark(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, mark(X3)) -> U44(X1, X2, X3) U45(mark(X1), X2) -> U45(X1, X2) U45(X1, mark(X2)) -> U45(X1, X2) U46(mark(X)) -> U46(X) U51(mark(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, mark(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, mark(X3)) -> U51(X1, X2, X3) U52(mark(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, mark(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, mark(X3)) -> U52(X1, X2, X3) U53(mark(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, mark(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, mark(X3)) -> U53(X1, X2, X3) U54(mark(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, mark(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, mark(X3)) -> U54(X1, X2, X3) U55(mark(X1), X2) -> U55(X1, X2) U55(X1, mark(X2)) -> U55(X1, X2) U56(mark(X)) -> U56(X) U61(mark(X1), X2) -> U61(X1, X2) U61(X1, mark(X2)) -> U61(X1, X2) U62(mark(X1), X2) -> U62(X1, X2) U62(X1, mark(X2)) -> U62(X1, X2) U63(mark(X)) -> U63(X) U71(mark(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, mark(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, mark(X3)) -> U71(X1, X2, X3) U72(mark(X1), X2) -> U72(X1, X2) U72(X1, mark(X2)) -> U72(X1, X2) U73(mark(X1), X2) -> U73(X1, X2) U73(X1, mark(X2)) -> U73(X1, X2) isPal(mark(X)) -> isPal(X) U74(mark(X)) -> U74(X) U81(mark(X1), X2) -> U81(X1, X2) U81(X1, mark(X2)) -> U81(X1, X2) U82(mark(X1), X2) -> U82(X1, X2) U82(X1, mark(X2)) -> U82(X1, X2) U83(mark(X)) -> U83(X) isNePal(mark(X)) -> isNePal(X) U91(mark(X1), X2) -> U91(X1, X2) U91(X1, mark(X2)) -> U91(X1, X2) U92(mark(X)) -> U92(X) Q is empty. ---------------------------------------- (5) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1, x_2)) = 2 + 2*x_1 + x_2 POL(U12(x_1, x_2)) = 1 + x_1 + x_2 POL(U13(x_1)) = 1 + x_1 POL(U21(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U22(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U23(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U24(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U25(x_1, x_2)) = 1 + x_1 + x_2 POL(U26(x_1)) = x_1 POL(U31(x_1, x_2)) = 1 + x_1 + x_2 POL(U32(x_1, x_2)) = 1 + x_1 + x_2 POL(U33(x_1)) = 1 + x_1 POL(U41(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U42(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U43(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U44(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U45(x_1, x_2)) = 1 + x_1 + x_2 POL(U46(x_1)) = 1 + x_1 POL(U51(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U52(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U53(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U54(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U55(x_1, x_2)) = 1 + x_1 + x_2 POL(U56(x_1)) = 1 + x_1 POL(U61(x_1, x_2)) = 1 + x_1 + x_2 POL(U62(x_1, x_2)) = 1 + x_1 + x_2 POL(U63(x_1)) = 1 + x_1 POL(U71(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3 POL(U72(x_1, x_2)) = 1 + x_1 + x_2 POL(U73(x_1, x_2)) = 1 + x_1 + x_2 POL(U74(x_1)) = 1 + x_1 POL(U81(x_1, x_2)) = 1 + x_1 + x_2 POL(U82(x_1, x_2)) = 1 + x_1 + x_2 POL(U83(x_1)) = 1 + x_1 POL(U91(x_1, x_2)) = 1 + x_1 + x_2 POL(U92(x_1)) = 1 + x_1 POL(__(x_1, x_2)) = x_1 + x_2 POL(a) = 2 POL(active(x_1)) = x_1 POL(isList(x_1)) = 2 + x_1 POL(isNeList(x_1)) = 2 + x_1 POL(isNePal(x_1)) = x_1 POL(isPal(x_1)) = x_1 POL(isPalListKind(x_1)) = x_1 POL(isQid(x_1)) = x_1 POL(mark(x_1)) = 1 + 2*x_1 POL(nil) = 2 POL(tt) = 0 POL(u) = 2 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: mark(nil) -> active(nil) mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) mark(U12(X1, X2)) -> active(U12(mark(X1), X2)) mark(U13(X)) -> active(U13(mark(X))) mark(isNeList(X)) -> active(isNeList(X)) mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)) mark(U22(X1, X2, X3)) -> active(U22(mark(X1), X2, X3)) mark(U23(X1, X2, X3)) -> active(U23(mark(X1), X2, X3)) mark(U24(X1, X2, X3)) -> active(U24(mark(X1), X2, X3)) mark(U25(X1, X2)) -> active(U25(mark(X1), X2)) mark(isList(X)) -> active(isList(X)) mark(U31(X1, X2)) -> active(U31(mark(X1), X2)) mark(U32(X1, X2)) -> active(U32(mark(X1), X2)) mark(U33(X)) -> active(U33(mark(X))) mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)) mark(U42(X1, X2, X3)) -> active(U42(mark(X1), X2, X3)) mark(U43(X1, X2, X3)) -> active(U43(mark(X1), X2, X3)) mark(U44(X1, X2, X3)) -> active(U44(mark(X1), X2, X3)) mark(U45(X1, X2)) -> active(U45(mark(X1), X2)) mark(U46(X)) -> active(U46(mark(X))) mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)) mark(U52(X1, X2, X3)) -> active(U52(mark(X1), X2, X3)) mark(U53(X1, X2, X3)) -> active(U53(mark(X1), X2, X3)) mark(U54(X1, X2, X3)) -> active(U54(mark(X1), X2, X3)) mark(U55(X1, X2)) -> active(U55(mark(X1), X2)) mark(U56(X)) -> active(U56(mark(X))) mark(U61(X1, X2)) -> active(U61(mark(X1), X2)) mark(U62(X1, X2)) -> active(U62(mark(X1), X2)) mark(U63(X)) -> active(U63(mark(X))) mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)) mark(U72(X1, X2)) -> active(U72(mark(X1), X2)) mark(U73(X1, X2)) -> active(U73(mark(X1), X2)) mark(U74(X)) -> active(U74(mark(X))) mark(U81(X1, X2)) -> active(U81(mark(X1), X2)) mark(U82(X1, X2)) -> active(U82(mark(X1), X2)) mark(U83(X)) -> active(U83(mark(X))) mark(U91(X1, X2)) -> active(U91(mark(X1), X2)) mark(U92(X)) -> active(U92(mark(X))) mark(a) -> active(a) mark(u) -> active(u) __(mark(X1), X2) -> __(X1, X2) __(X1, mark(X2)) -> __(X1, X2) U11(mark(X1), X2) -> U11(X1, X2) U11(X1, mark(X2)) -> U11(X1, X2) U12(mark(X1), X2) -> U12(X1, X2) U12(X1, mark(X2)) -> U12(X1, X2) isPalListKind(mark(X)) -> isPalListKind(X) U13(mark(X)) -> U13(X) isNeList(mark(X)) -> isNeList(X) U21(mark(X1), X2, X3) -> U21(X1, X2, X3) U21(X1, mark(X2), X3) -> U21(X1, X2, X3) U21(X1, X2, mark(X3)) -> U21(X1, X2, X3) U22(mark(X1), X2, X3) -> U22(X1, X2, X3) U22(X1, mark(X2), X3) -> U22(X1, X2, X3) U22(X1, X2, mark(X3)) -> U22(X1, X2, X3) U23(mark(X1), X2, X3) -> U23(X1, X2, X3) U23(X1, mark(X2), X3) -> U23(X1, X2, X3) U23(X1, X2, mark(X3)) -> U23(X1, X2, X3) U24(mark(X1), X2, X3) -> U24(X1, X2, X3) U24(X1, mark(X2), X3) -> U24(X1, X2, X3) U24(X1, X2, mark(X3)) -> U24(X1, X2, X3) U25(mark(X1), X2) -> U25(X1, X2) U25(X1, mark(X2)) -> U25(X1, X2) isList(mark(X)) -> isList(X) U26(mark(X)) -> U26(X) U31(mark(X1), X2) -> U31(X1, X2) U31(X1, mark(X2)) -> U31(X1, X2) U32(mark(X1), X2) -> U32(X1, X2) U32(X1, mark(X2)) -> U32(X1, X2) U33(mark(X)) -> U33(X) isQid(mark(X)) -> isQid(X) U41(mark(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, mark(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, mark(X3)) -> U41(X1, X2, X3) U42(mark(X1), X2, X3) -> U42(X1, X2, X3) U42(X1, mark(X2), X3) -> U42(X1, X2, X3) U42(X1, X2, mark(X3)) -> U42(X1, X2, X3) U43(mark(X1), X2, X3) -> U43(X1, X2, X3) U43(X1, mark(X2), X3) -> U43(X1, X2, X3) U43(X1, X2, mark(X3)) -> U43(X1, X2, X3) U44(mark(X1), X2, X3) -> U44(X1, X2, X3) U44(X1, mark(X2), X3) -> U44(X1, X2, X3) U44(X1, X2, mark(X3)) -> U44(X1, X2, X3) U45(mark(X1), X2) -> U45(X1, X2) U45(X1, mark(X2)) -> U45(X1, X2) U46(mark(X)) -> U46(X) U51(mark(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, mark(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, mark(X3)) -> U51(X1, X2, X3) U52(mark(X1), X2, X3) -> U52(X1, X2, X3) U52(X1, mark(X2), X3) -> U52(X1, X2, X3) U52(X1, X2, mark(X3)) -> U52(X1, X2, X3) U53(mark(X1), X2, X3) -> U53(X1, X2, X3) U53(X1, mark(X2), X3) -> U53(X1, X2, X3) U53(X1, X2, mark(X3)) -> U53(X1, X2, X3) U54(mark(X1), X2, X3) -> U54(X1, X2, X3) U54(X1, mark(X2), X3) -> U54(X1, X2, X3) U54(X1, X2, mark(X3)) -> U54(X1, X2, X3) U55(mark(X1), X2) -> U55(X1, X2) U55(X1, mark(X2)) -> U55(X1, X2) U56(mark(X)) -> U56(X) U61(mark(X1), X2) -> U61(X1, X2) U61(X1, mark(X2)) -> U61(X1, X2) U62(mark(X1), X2) -> U62(X1, X2) U62(X1, mark(X2)) -> U62(X1, X2) U63(mark(X)) -> U63(X) U71(mark(X1), X2, X3) -> U71(X1, X2, X3) U71(X1, mark(X2), X3) -> U71(X1, X2, X3) U71(X1, X2, mark(X3)) -> U71(X1, X2, X3) U72(mark(X1), X2) -> U72(X1, X2) U72(X1, mark(X2)) -> U72(X1, X2) U73(mark(X1), X2) -> U73(X1, X2) U73(X1, mark(X2)) -> U73(X1, X2) isPal(mark(X)) -> isPal(X) U74(mark(X)) -> U74(X) U81(mark(X1), X2) -> U81(X1, X2) U81(X1, mark(X2)) -> U81(X1, X2) U82(mark(X1), X2) -> U82(X1, X2) U82(X1, mark(X2)) -> U82(X1, X2) U83(mark(X)) -> U83(X) isNePal(mark(X)) -> isNePal(X) U91(mark(X1), X2) -> U91(X1, X2) U91(X1, mark(X2)) -> U91(X1, X2) U92(mark(X)) -> U92(X) ---------------------------------------- (6) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: active(U63(tt)) -> mark(tt) active(U92(tt)) -> mark(tt) Q is empty. ---------------------------------------- (7) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U63(x_1)) = x_1 POL(U92(x_1)) = x_1 POL(active(x_1)) = 2 + 2*x_1 POL(mark(x_1)) = 2 + x_1 POL(tt) = 1 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: active(U63(tt)) -> mark(tt) active(U92(tt)) -> mark(tt) ---------------------------------------- (8) Obligation: Q restricted rewrite system: R is empty. Q is empty. ---------------------------------------- (9) RisEmptyProof (EQUIVALENT) The TRS R is empty. Hence, termination is trivially proven. ---------------------------------------- (10) YES