YES proof of Transformed_CSR_04_PALINDROME_complete-noand_FR.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, 362 ms] (2) QTRS (3) QTRSRRRProof [EQUIVALENT, 2 ms] (4) QTRS (5) RisEmptyProof [EQUIVALENT, 0 ms] (6) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: __(__(X, Y), Z) -> __(X, __(Y, Z)) __(X, nil) -> X __(nil, X) -> X U11(tt, V) -> U12(isPalListKind(activate(V)), activate(V)) U12(tt, V) -> U13(isNeList(activate(V))) U13(tt) -> tt U21(tt, V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) U22(tt, V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) U23(tt, V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) U24(tt, V1, V2) -> U25(isList(activate(V1)), activate(V2)) U25(tt, V2) -> U26(isList(activate(V2))) U26(tt) -> tt U31(tt, V) -> U32(isPalListKind(activate(V)), activate(V)) U32(tt, V) -> U33(isQid(activate(V))) U33(tt) -> tt U41(tt, V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) U42(tt, V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) U43(tt, V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) U44(tt, V1, V2) -> U45(isList(activate(V1)), activate(V2)) U45(tt, V2) -> U46(isNeList(activate(V2))) U46(tt) -> tt U51(tt, V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) U52(tt, V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) U53(tt, V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) U54(tt, V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) U55(tt, V2) -> U56(isList(activate(V2))) U56(tt) -> tt U61(tt, V) -> U62(isPalListKind(activate(V)), activate(V)) U62(tt, V) -> U63(isQid(activate(V))) U63(tt) -> tt U71(tt, I, P) -> U72(isPalListKind(activate(I)), activate(P)) U72(tt, P) -> U73(isPal(activate(P)), activate(P)) U73(tt, P) -> U74(isPalListKind(activate(P))) U74(tt) -> tt U81(tt, V) -> U82(isPalListKind(activate(V)), activate(V)) U82(tt, V) -> U83(isNePal(activate(V))) U83(tt) -> tt U91(tt, V2) -> U92(isPalListKind(activate(V2))) U92(tt) -> tt isList(V) -> U11(isPalListKind(activate(V)), activate(V)) isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) isNePal(n____(I, n____(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) isPal(n__nil) -> tt isPalListKind(n__a) -> tt isPalListKind(n__e) -> tt isPalListKind(n__i) -> tt isPalListKind(n__nil) -> tt isPalListKind(n__o) -> tt isPalListKind(n__u) -> tt isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) isQid(n__a) -> tt isQid(n__e) -> tt isQid(n__i) -> tt isQid(n__o) -> tt isQid(n__u) -> tt nil -> n__nil __(X1, X2) -> n____(X1, X2) a -> n__a e -> n__e i -> n__i o -> n__o u -> n__u activate(n__nil) -> nil activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) activate(n__a) -> a activate(n__e) -> e activate(n__i) -> i activate(n__o) -> o activate(n__u) -> u activate(X) -> X Q is empty. ---------------------------------------- (1) QTRSRRRProof (EQUIVALENT) Used ordering: __/2(YES,YES) nil/0) U11/2(YES,YES) tt/0) U12/2(YES,YES) isPalListKind/1)YES( activate/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( n__nil/0) n____/2(YES,YES) n__a/0) n__e/0) n__i/0) n__o/0) n__u/0) a/0) e/0) i/0) o/0) u/0) Quasi precedence: [___2, n_____2] > U21_3 > U22_3 > U23_3 > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U21_3 > U22_3 > U23_3 > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U41_3 > U42_3 > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U51_3 > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____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, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > U73_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U71_3 > U72_2 > isPal_1 > U81_2 > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [___2, n_____2] > U91_2 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [nil, n__nil] > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__a, a] > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__e, e] > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__o, o] > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U24_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U44_3 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U44_3 > U45_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U13_1 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > U52_3 > U53_3 > U54_3 > U55_2 > [U25_2, isList_1] > U11_2 > [U12_2, isNeList_1] > U31_2 > [U32_2, isQid_1, U62_2] [n__u, u] > [tt, U43_3, n__i, i] > [U82_2, isNePal_1] > U61_2 > [U32_2, isQid_1, U62_2] Status: ___2: [1,2] nil: multiset status U11_2: multiset status tt: multiset status U12_2: multiset status U13_1: [1] isNeList_1: multiset status U21_3: [1,2,3] U22_3: [1,2,3] U23_3: [2,1,3] U24_3: [3,2,1] U25_2: multiset status isList_1: multiset status U31_2: [1,2] U32_2: multiset status isQid_1: multiset status U41_3: [3,1,2] U42_3: multiset status U43_3: [2,3,1] U44_3: [2,3,1] U45_2: multiset status U51_3: multiset status U52_3: [3,2,1] U53_3: multiset status U54_3: [3,2,1] U55_2: [2,1] U61_2: [1,2] U62_2: multiset status U71_3: [3,1,2] U72_2: multiset status U73_2: multiset status isPal_1: multiset status U81_2: [1,2] U82_2: multiset status isNePal_1: multiset status U91_2: [1,2] n__nil: multiset status n_____2: [1,2] n__a: multiset status n__e: multiset status n__i: multiset status n__o: multiset status n__u: 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: __(__(X, Y), Z) -> __(X, __(Y, Z)) __(X, nil) -> X __(nil, X) -> X U11(tt, V) -> U12(isPalListKind(activate(V)), activate(V)) U12(tt, V) -> U13(isNeList(activate(V))) U13(tt) -> tt U21(tt, V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) U22(tt, V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) U23(tt, V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) U24(tt, V1, V2) -> U25(isList(activate(V1)), activate(V2)) U25(tt, V2) -> U26(isList(activate(V2))) U31(tt, V) -> U32(isPalListKind(activate(V)), activate(V)) U32(tt, V) -> U33(isQid(activate(V))) U41(tt, V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) U42(tt, V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) U43(tt, V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) U44(tt, V1, V2) -> U45(isList(activate(V1)), activate(V2)) U45(tt, V2) -> U46(isNeList(activate(V2))) U51(tt, V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) U52(tt, V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) U53(tt, V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) U54(tt, V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) U55(tt, V2) -> U56(isList(activate(V2))) U61(tt, V) -> U62(isPalListKind(activate(V)), activate(V)) U62(tt, V) -> U63(isQid(activate(V))) U71(tt, I, P) -> U72(isPalListKind(activate(I)), activate(P)) U72(tt, P) -> U73(isPal(activate(P)), activate(P)) U73(tt, P) -> U74(isPalListKind(activate(P))) U81(tt, V) -> U82(isPalListKind(activate(V)), activate(V)) U82(tt, V) -> U83(isNePal(activate(V))) U91(tt, V2) -> U92(isPalListKind(activate(V2))) isList(V) -> U11(isPalListKind(activate(V)), activate(V)) isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) isNePal(n____(I, n____(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) isPal(n__nil) -> tt isPalListKind(n__a) -> tt isPalListKind(n__e) -> tt isPalListKind(n__nil) -> tt isPalListKind(n__o) -> tt isPalListKind(n__u) -> tt isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) isQid(n__a) -> tt isQid(n__e) -> tt isQid(n__i) -> tt isQid(n__o) -> tt isQid(n__u) -> tt ---------------------------------------- (2) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: U26(tt) -> tt U33(tt) -> tt U46(tt) -> tt U56(tt) -> tt U63(tt) -> tt U74(tt) -> tt U83(tt) -> tt U92(tt) -> tt isPalListKind(n__i) -> tt nil -> n__nil __(X1, X2) -> n____(X1, X2) a -> n__a e -> n__e i -> n__i o -> n__o u -> n__u activate(n__nil) -> nil activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) activate(n__a) -> a activate(n__e) -> e activate(n__i) -> i activate(n__o) -> o activate(n__u) -> u activate(X) -> X Q is empty. ---------------------------------------- (3) QTRSRRRProof (EQUIVALENT) Used ordering: Knuth-Bendix order [KBO] with precedence:activate_1 > u > n__u > o > n__o > i > e > n__e > a > n__a > ___2 > n_____2 > nil > n__nil > U26_1 > n__i > isPalListKind_1 > U83_1 > U74_1 > U46_1 > U92_1 > U63_1 > U56_1 > U33_1 > tt and weight map: tt=2 n__i=1 nil=1 n__nil=1 a=1 n__a=1 e=1 n__e=1 i=1 o=1 n__o=1 u=1 n__u=1 U26_1=1 U33_1=1 U46_1=1 U56_1=1 U63_1=1 U74_1=1 U83_1=1 U92_1=1 isPalListKind_1=1 activate_1=0 ___2=0 n_____2=0 The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: U26(tt) -> tt U33(tt) -> tt U46(tt) -> tt U56(tt) -> tt U63(tt) -> tt U74(tt) -> tt U83(tt) -> tt U92(tt) -> tt isPalListKind(n__i) -> tt nil -> n__nil __(X1, X2) -> n____(X1, X2) a -> n__a e -> n__e i -> n__i o -> n__o u -> n__u activate(n__nil) -> nil activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) activate(n__a) -> a activate(n__e) -> e activate(n__i) -> i activate(n__o) -> o activate(n__u) -> u activate(X) -> X ---------------------------------------- (4) Obligation: Q restricted rewrite system: R is empty. Q is empty. ---------------------------------------- (5) RisEmptyProof (EQUIVALENT) The TRS R is empty. Hence, termination is trivially proven. ---------------------------------------- (6) YES