WORST_CASE(NON_POLY,?) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(INF, INF). (0) CpxTRS (1) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (2) TRS for Loop Detection (3) InfiniteLowerBoundProof [FINISHED, 0 ms] (4) BOUNDS(INF, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(INF, INF). The TRS R consists of the following rules: 2nd(cons(X, cons(Y, Z))) -> Y from(X) -> cons(X, from(s(X))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (2) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(INF, INF). The TRS R consists of the following rules: 2nd(cons(X, cons(Y, Z))) -> Y from(X) -> cons(X, from(s(X))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (3) InfiniteLowerBoundProof (FINISHED) The following loop proves infinite runtime complexity: The rewrite sequence from(X) ->^+ cons(X, from(s(X))) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [ ]. The result substitution is [X / s(X)]. ---------------------------------------- (4) BOUNDS(INF, INF)