NO proof of Transformed_CSR_04_PALINDROME_nokinds-noand_L.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished Termination w.r.t. Q of the given QTRS could be disproven: (0) QTRS (1) QTRSRRRProof [EQUIVALENT, 69 ms] (2) QTRS (3) QTRSRRRProof [EQUIVALENT, 0 ms] (4) QTRS (5) DependencyPairsProof [EQUIVALENT, 0 ms] (6) QDP (7) DependencyGraphProof [EQUIVALENT, 0 ms] (8) AND (9) QDP (10) UsableRulesProof [EQUIVALENT, 0 ms] (11) QDP (12) MNOCProof [EQUIVALENT, 0 ms] (13) QDP (14) TransformationProof [EQUIVALENT, 0 ms] (15) QDP (16) UsableRulesProof [EQUIVALENT, 0 ms] (17) QDP (18) QReductionProof [EQUIVALENT, 0 ms] (19) QDP (20) NonTerminationLoopProof [COMPLETE, 0 ms] (21) NO (22) QDP (23) UsableRulesProof [EQUIVALENT, 0 ms] (24) QDP (25) TransformationProof [EQUIVALENT, 0 ms] (26) QDP (27) TransformationProof [EQUIVALENT, 0 ms] (28) QDP (29) TransformationProof [EQUIVALENT, 0 ms] (30) QDP (31) TransformationProof [EQUIVALENT, 0 ms] (32) QDP (33) TransformationProof [EQUIVALENT, 0 ms] (34) QDP (35) NonTerminationLoopProof [COMPLETE, 0 ms] (36) NO ---------------------------------------- (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) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U61(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U61(isQid) isNePal -> U71(isQid) isPal -> U81(isNePal) isPal -> tt isQid -> tt Q is empty. ---------------------------------------- (1) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1)) = x_1 POL(U21(x_1)) = 2*x_1 POL(U22(x_1)) = x_1 POL(U31(x_1)) = 2*x_1 POL(U41(x_1)) = x_1 POL(U42(x_1)) = x_1 POL(U51(x_1)) = 2*x_1 POL(U52(x_1)) = 2*x_1 POL(U61(x_1)) = x_1 POL(U71(x_1)) = 2 + x_1 POL(U72(x_1)) = x_1 POL(U81(x_1)) = x_1 POL(__(x_1, x_2)) = 2 + 2*x_1 + x_2 POL(isList) = 0 POL(isNeList) = 0 POL(isNePal) = 2 POL(isPal) = 2 POL(isQid) = 0 POL(nil) = 2 POL(tt) = 0 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 isNePal -> U61(isQid) isPal -> tt ---------------------------------------- (2) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: U11(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U61(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U71(isQid) isPal -> U81(isNePal) isQid -> tt Q is empty. ---------------------------------------- (3) QTRSRRRProof (EQUIVALENT) Used ordering: Polynomial interpretation [POLO]: POL(U11(x_1)) = 2*x_1 POL(U21(x_1)) = 2*x_1 POL(U22(x_1)) = x_1 POL(U31(x_1)) = 2*x_1 POL(U41(x_1)) = x_1 POL(U42(x_1)) = x_1 POL(U51(x_1)) = x_1 POL(U52(x_1)) = 2*x_1 POL(U61(x_1)) = 1 + x_1 POL(U71(x_1)) = x_1 POL(U72(x_1)) = x_1 POL(U81(x_1)) = 2*x_1 POL(isList) = 0 POL(isNeList) = 0 POL(isNePal) = 0 POL(isPal) = 0 POL(isQid) = 0 POL(tt) = 0 With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: U61(tt) -> tt ---------------------------------------- (4) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: U11(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U71(isQid) isPal -> U81(isNePal) isQid -> tt Q is empty. ---------------------------------------- (5) DependencyPairsProof (EQUIVALENT) Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem. ---------------------------------------- (6) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> U22^1(isList) U21^1(tt) -> ISLIST U41^1(tt) -> U42^1(isNeList) U41^1(tt) -> ISNELIST U51^1(tt) -> U52^1(isList) U51^1(tt) -> ISLIST U71^1(tt) -> U72^1(isPal) U71^1(tt) -> ISPAL ISLIST -> U11^1(isNeList) ISLIST -> ISNELIST ISLIST -> U21^1(isList) ISLIST -> ISLIST ISNELIST -> U31^1(isQid) ISNELIST -> ISQID ISNELIST -> U41^1(isList) ISNELIST -> ISLIST ISNELIST -> U51^1(isNeList) ISNELIST -> ISNELIST ISNEPAL -> U71^1(isQid) ISNEPAL -> ISQID ISPAL -> U81^1(isNePal) ISPAL -> ISNEPAL The TRS R consists of the following rules: U11(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U71(isQid) isPal -> U81(isNePal) isQid -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (7) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 9 less nodes. ---------------------------------------- (8) Complex Obligation (AND) ---------------------------------------- (9) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(isQid) The TRS R consists of the following rules: U11(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U71(isQid) isPal -> U81(isNePal) isQid -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (10) UsableRulesProof (EQUIVALENT) We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R. ---------------------------------------- (11) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(isQid) The TRS R consists of the following rules: isQid -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (12) MNOCProof (EQUIVALENT) We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R. ---------------------------------------- (13) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(isQid) The TRS R consists of the following rules: isQid -> tt The set Q consists of the following terms: isQid We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (14) TransformationProof (EQUIVALENT) By rewriting [LPAR04] the rule ISNEPAL -> U71^1(isQid) at position [0] we obtained the following new rules [LPAR04]: (ISNEPAL -> U71^1(tt),ISNEPAL -> U71^1(tt)) ---------------------------------------- (15) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(tt) The TRS R consists of the following rules: isQid -> tt The set Q consists of the following terms: isQid We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (16) UsableRulesProof (EQUIVALENT) As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R. ---------------------------------------- (17) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(tt) R is empty. The set Q consists of the following terms: isQid We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (18) QReductionProof (EQUIVALENT) We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN]. isQid ---------------------------------------- (19) Obligation: Q DP problem: The TRS P consists of the following rules: U71^1(tt) -> ISPAL ISPAL -> ISNEPAL ISNEPAL -> U71^1(tt) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (20) NonTerminationLoopProof (COMPLETE) We used the non-termination processor [FROCOS05] to show that the DP problem is infinite. Found a loop by narrowing to the left: s = ISPAL evaluates to t =ISPAL Thus s starts an infinite chain as s semiunifies with t with the following substitutions: * Matcher: [ ] * Semiunifier: [ ] -------------------------------------------------------------------------------- Rewriting sequence ISPAL -> ISNEPAL with rule ISPAL -> ISNEPAL at position [] and matcher [ ] ISNEPAL -> U71^1(tt) with rule ISNEPAL -> U71^1(tt) at position [] and matcher [ ] U71^1(tt) -> ISPAL with rule U71^1(tt) -> ISPAL Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence All these steps are and every following step will be a correct step w.r.t to Q. ---------------------------------------- (21) NO ---------------------------------------- (22) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST ISNELIST -> U41^1(isList) U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> U21^1(isList) ISLIST -> ISLIST ISNELIST -> U51^1(isNeList) U51^1(tt) -> ISLIST ISNELIST -> ISNELIST The TRS R consists of the following rules: U11(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U31(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt U51(tt) -> U52(isList) U52(tt) -> tt U71(tt) -> U72(isPal) U72(tt) -> tt U81(tt) -> tt isList -> U11(isNeList) isList -> tt isList -> U21(isList) isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) isNePal -> U71(isQid) isPal -> U81(isNePal) isQid -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (23) UsableRulesProof (EQUIVALENT) We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R. ---------------------------------------- (24) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST ISNELIST -> U41^1(isList) U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> U21^1(isList) ISLIST -> ISLIST ISNELIST -> U51^1(isNeList) U51^1(tt) -> ISLIST ISNELIST -> ISNELIST The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (25) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule ISNELIST -> U41^1(isList) at position [0] we obtained the following new rules [LPAR04]: (ISNELIST -> U41^1(U11(isNeList)),ISNELIST -> U41^1(U11(isNeList))) (ISNELIST -> U41^1(tt),ISNELIST -> U41^1(tt)) (ISNELIST -> U41^1(U21(isList)),ISNELIST -> U41^1(U21(isList))) ---------------------------------------- (26) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> U21^1(isList) ISLIST -> ISLIST ISNELIST -> U51^1(isNeList) U51^1(tt) -> ISLIST ISNELIST -> ISNELIST ISNELIST -> U41^1(U11(isNeList)) ISNELIST -> U41^1(tt) ISNELIST -> U41^1(U21(isList)) The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (27) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule ISLIST -> U21^1(isList) at position [0] we obtained the following new rules [LPAR04]: (ISLIST -> U21^1(U11(isNeList)),ISLIST -> U21^1(U11(isNeList))) (ISLIST -> U21^1(tt),ISLIST -> U21^1(tt)) (ISLIST -> U21^1(U21(isList)),ISLIST -> U21^1(U21(isList))) ---------------------------------------- (28) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> ISLIST ISNELIST -> U51^1(isNeList) U51^1(tt) -> ISLIST ISNELIST -> ISNELIST ISNELIST -> U41^1(U11(isNeList)) ISNELIST -> U41^1(tt) ISNELIST -> U41^1(U21(isList)) ISLIST -> U21^1(U11(isNeList)) ISLIST -> U21^1(tt) ISLIST -> U21^1(U21(isList)) The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (29) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule ISNELIST -> U51^1(isNeList) at position [0] we obtained the following new rules [LPAR04]: (ISNELIST -> U51^1(U31(isQid)),ISNELIST -> U51^1(U31(isQid))) (ISNELIST -> U51^1(U41(isList)),ISNELIST -> U51^1(U41(isList))) (ISNELIST -> U51^1(U51(isNeList)),ISNELIST -> U51^1(U51(isNeList))) ---------------------------------------- (30) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> ISLIST U51^1(tt) -> ISLIST ISNELIST -> ISNELIST ISNELIST -> U41^1(U11(isNeList)) ISNELIST -> U41^1(tt) ISNELIST -> U41^1(U21(isList)) ISLIST -> U21^1(U11(isNeList)) ISLIST -> U21^1(tt) ISLIST -> U21^1(U21(isList)) ISNELIST -> U51^1(U31(isQid)) ISNELIST -> U51^1(U41(isList)) ISNELIST -> U51^1(U51(isNeList)) The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (31) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule ISNELIST -> U51^1(U31(isQid)) at position [0] we obtained the following new rules [LPAR04]: (ISNELIST -> U51^1(U31(tt)),ISNELIST -> U51^1(U31(tt))) ---------------------------------------- (32) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> ISLIST U51^1(tt) -> ISLIST ISNELIST -> ISNELIST ISNELIST -> U41^1(U11(isNeList)) ISNELIST -> U41^1(tt) ISNELIST -> U41^1(U21(isList)) ISLIST -> U21^1(U11(isNeList)) ISLIST -> U21^1(tt) ISLIST -> U21^1(U21(isList)) ISNELIST -> U51^1(U41(isList)) ISNELIST -> U51^1(U51(isNeList)) ISNELIST -> U51^1(U31(tt)) The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (33) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule ISNELIST -> U51^1(U31(tt)) at position [0] we obtained the following new rules [LPAR04]: (ISNELIST -> U51^1(tt),ISNELIST -> U51^1(tt)) ---------------------------------------- (34) Obligation: Q DP problem: The TRS P consists of the following rules: U21^1(tt) -> ISLIST ISLIST -> ISNELIST U41^1(tt) -> ISNELIST ISNELIST -> ISLIST ISLIST -> ISLIST U51^1(tt) -> ISLIST ISNELIST -> ISNELIST ISNELIST -> U41^1(U11(isNeList)) ISNELIST -> U41^1(tt) ISNELIST -> U41^1(U21(isList)) ISLIST -> U21^1(U11(isNeList)) ISLIST -> U21^1(tt) ISLIST -> U21^1(U21(isList)) ISNELIST -> U51^1(U41(isList)) ISNELIST -> U51^1(U51(isNeList)) ISNELIST -> U51^1(tt) The TRS R consists of the following rules: isNeList -> U31(isQid) isNeList -> U41(isList) isNeList -> U51(isNeList) U51(tt) -> U52(isList) isList -> U11(isNeList) isList -> tt isList -> U21(isList) U52(tt) -> tt U21(tt) -> U22(isList) U22(tt) -> tt U11(tt) -> tt U41(tt) -> U42(isNeList) U42(tt) -> tt isQid -> tt U31(tt) -> tt Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (35) NonTerminationLoopProof (COMPLETE) We used the non-termination processor [FROCOS05] to show that the DP problem is infinite. Found a loop by semiunifying a rule from P directly. s = ISLIST evaluates to t =ISLIST Thus s starts an infinite chain as s semiunifies with t with the following substitutions: * Matcher: [ ] * Semiunifier: [ ] -------------------------------------------------------------------------------- Rewriting sequence The DP semiunifies directly so there is only one rewrite step from ISLIST to ISLIST. ---------------------------------------- (36) NO