YES proof of Transformed_CSR_04_PALINDROME_nokinds-noand_Z.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, 149 ms] (2) QTRS (3) QTRSRRRProof [EQUIVALENT, 0 ms] (4) QTRS (5) QTRSRRRProof [EQUIVALENT, 9 ms] (6) QTRS (7) QTRSRRRProof [EQUIVALENT, 0 ms] (8) QTRS (9) QTRSRRRProof [EQUIVALENT, 2 ms] (10) QTRS (11) RisEmptyProof [EQUIVALENT, 0 ms] (12) 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) -> tt U21(tt, V2) -> U22(isList(activate(V2))) U22(tt) -> tt U31(tt) -> tt U41(tt, V2) -> U42(isNeList(activate(V2))) U42(tt) -> tt U51(tt, V2) -> U52(isList(activate(V2))) U52(tt) -> tt U61(tt) -> tt U71(tt, P) -> U72(isPal(activate(P))) U72(tt) -> tt U81(tt) -> tt isList(V) -> U11(isNeList(activate(V))) isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil) -> tt 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)) -> __(X1, 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: Polynomial interpretation [POLO]: POL(U11(x_1)) = x_1 POL(U21(x_1, x_2)) = x_1 + x_2 POL(U22(x_1)) = 1 + x_1 POL(U31(x_1)) = 1 + x_1 POL(U41(x_1, x_2)) = x_1 + x_2 POL(U42(x_1)) = 1 + x_1 POL(U51(x_1, x_2)) = x_1 + x_2 POL(U52(x_1)) = x_1 POL(U61(x_1)) = x_1 POL(U71(x_1, x_2)) = 2*x_1 + 2*x_2 POL(U72(x_1)) = x_1 POL(U81(x_1)) = 2 + 2*x_1 POL(__(x_1, x_2)) = 2*x_1 + x_2 POL(a) = 2 POL(activate(x_1)) = x_1 POL(e) = 2 POL(i) = 2 POL(isList(x_1)) = 1 + x_1 POL(isNeList(x_1)) = 1 + x_1 POL(isNePal(x_1)) = x_1 POL(isPal(x_1)) = 2 + 2*x_1 POL(isQid(x_1)) = x_1 POL(n____(x_1, x_2)) = 2*x_1 + x_2 POL(n__a) = 2 POL(n__e) = 2 POL(n__i) = 2 POL(n__nil) = 1 POL(n__o) = 2 POL(n__u) = 2 POL(nil) = 1 POL(o) = 2 POL(tt) = 2 POL(u) = 2 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: __(X, nil) -> X __(nil, X) -> X U22(tt) -> tt U31(tt) -> tt U42(tt) -> tt U51(tt, V2) -> U52(isList(activate(V2))) U71(tt, P) -> U72(isPal(activate(P))) U81(tt) -> tt isPal(n__nil) -> tt ---------------------------------------- (2) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: __(__(X, Y), Z) -> __(X, __(Y, Z)) U11(tt) -> tt U21(tt, V2) -> U22(isList(activate(V2))) U41(tt, V2) -> U42(isNeList(activate(V2))) U52(tt) -> tt U61(tt) -> tt U72(tt) -> tt isList(V) -> U11(isNeList(activate(V))) isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) isPal(V) -> U81(isNePal(activate(V))) 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)) -> __(X1, 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: Polynomial interpretation [POLO]: POL(U11(x_1)) = 2*x_1 POL(U21(x_1, x_2)) = 1 + 2*x_1 + 2*x_2 POL(U22(x_1)) = x_1 POL(U31(x_1)) = x_1 POL(U41(x_1, x_2)) = x_1 + x_2 POL(U42(x_1)) = x_1 POL(U51(x_1, x_2)) = 2*x_1 + x_2 POL(U52(x_1)) = 1 + 2*x_1 POL(U61(x_1)) = x_1 POL(U71(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 POL(U72(x_1)) = 1 + x_1 POL(U81(x_1)) = x_1 POL(__(x_1, x_2)) = 1 + 2*x_1 + x_2 POL(a) = 2 POL(activate(x_1)) = x_1 POL(e) = 1 POL(i) = 1 POL(isList(x_1)) = 2*x_1 POL(isNeList(x_1)) = x_1 POL(isNePal(x_1)) = 2*x_1 POL(isPal(x_1)) = 1 + 2*x_1 POL(isQid(x_1)) = x_1 POL(n____(x_1, x_2)) = 1 + 2*x_1 + x_2 POL(n__a) = 2 POL(n__e) = 1 POL(n__i) = 1 POL(n__nil) = 2 POL(n__o) = 2 POL(n__u) = 2 POL(nil) = 2 POL(o) = 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: __(__(X, Y), Z) -> __(X, __(Y, Z)) U21(tt, V2) -> U22(isList(activate(V2))) U52(tt) -> tt U72(tt) -> tt isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) isPal(V) -> U81(isNePal(activate(V))) isQid(n__a) -> tt isQid(n__e) -> tt isQid(n__i) -> tt isQid(n__o) -> tt isQid(n__u) -> tt ---------------------------------------- (4) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: U11(tt) -> tt U41(tt, V2) -> U42(isNeList(activate(V2))) U61(tt) -> tt isList(V) -> U11(isNeList(activate(V))) isNeList(V) -> U31(isQid(activate(V))) isNePal(V) -> U61(isQid(activate(V))) 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)) -> __(X1, 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. ---------------------------------------- (5) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1)) = x_1 POL(U31(x_1)) = x_1 POL(U41(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 POL(U42(x_1)) = x_1 POL(U61(x_1)) = 2 + x_1 POL(__(x_1, x_2)) = 2 + x_1 + 2*x_2 POL(a) = 1 POL(activate(x_1)) = x_1 POL(e) = 1 POL(i) = 0 POL(isList(x_1)) = 2 + 2*x_1 POL(isNeList(x_1)) = 2 + 2*x_1 POL(isNePal(x_1)) = 2 + 2*x_1 POL(isQid(x_1)) = 2*x_1 POL(n____(x_1, x_2)) = 2 + x_1 + 2*x_2 POL(n__a) = 1 POL(n__e) = 1 POL(n__i) = 0 POL(n__nil) = 2 POL(n__o) = 1 POL(n__u) = 1 POL(nil) = 2 POL(o) = 1 POL(tt) = 1 POL(u) = 1 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: U41(tt, V2) -> U42(isNeList(activate(V2))) U61(tt) -> tt isNeList(V) -> U31(isQid(activate(V))) ---------------------------------------- (6) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: U11(tt) -> tt isList(V) -> U11(isNeList(activate(V))) isNePal(V) -> U61(isQid(activate(V))) 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)) -> __(X1, 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. ---------------------------------------- (7) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1)) = 2*x_1 POL(U61(x_1)) = x_1 POL(__(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(a) = 1 POL(activate(x_1)) = 1 + x_1 POL(e) = 2 POL(i) = 2 POL(isList(x_1)) = 2 + 2*x_1 POL(isNeList(x_1)) = x_1 POL(isNePal(x_1)) = 2 + x_1 POL(isQid(x_1)) = x_1 POL(n____(x_1, x_2)) = 1 + x_1 + 2*x_2 POL(n__a) = 1 POL(n__e) = 2 POL(n__i) = 1 POL(n__nil) = 2 POL(n__o) = 1 POL(n__u) = 1 POL(nil) = 2 POL(o) = 2 POL(tt) = 1 POL(u) = 1 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: U11(tt) -> tt isNePal(V) -> U61(isQid(activate(V))) i -> n__i o -> n__o activate(n__nil) -> nil activate(n____(X1, X2)) -> __(X1, X2) activate(n__a) -> a activate(n__e) -> e activate(n__u) -> u activate(X) -> X ---------------------------------------- (8) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: isList(V) -> U11(isNeList(activate(V))) nil -> n__nil __(X1, X2) -> n____(X1, X2) a -> n__a e -> n__e u -> n__u activate(n__i) -> i activate(n__o) -> o Q is empty. ---------------------------------------- (9) QTRSRRRProof (EQUIVALENT) Used ordering: Knuth-Bendix order [KBO] with precedence:activate_1 > isList_1 > U11_1 > o > n__o > i > n__i > u > n__u > e > n__e > a > n__a > ___2 > n_____2 > isNeList_1 > nil > n__nil and weight map: nil=1 n__nil=1 a=1 n__a=1 e=1 n__e=1 u=1 n__u=1 n__i=1 i=2 n__o=1 o=2 isList_1=3 U11_1=1 isNeList_1=1 activate_1=1 ___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: isList(V) -> U11(isNeList(activate(V))) nil -> n__nil __(X1, X2) -> n____(X1, X2) a -> n__a e -> n__e u -> n__u activate(n__i) -> i activate(n__o) -> o ---------------------------------------- (10) Obligation: Q restricted rewrite system: R is empty. Q is empty. ---------------------------------------- (11) RisEmptyProof (EQUIVALENT) The TRS R is empty. Hence, termination is trivially proven. ---------------------------------------- (12) YES