WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 132 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 8 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 66 ms] (12) CdtProblem (13) CdtKnowledgeProof [FINISHED, 0 ms] (14) BOUNDS(1, 1) (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 4 ms] (16) TRS for Loop Detection (17) DecreasingLoopProof [LOWER BOUND(ID), 156 ms] (18) BEST (19) proven lower bound (20) LowerBoundPropagationProof [FINISHED, 0 ms] (21) BOUNDS(n^1, INF) (22) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 Tuples: U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0)) PLUS'(z0, 0) -> c9 PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) ACTIVATE'(z0) -> c11 U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z0)) PLUS''(z0, 0) -> c16 PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) ACTIVATE''(z0) -> c18 S tuples: U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z0)) PLUS''(z0, 0) -> c16 PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) ACTIVATE''(z0) -> c18 K tuples:none Defined Rule Symbols: U11'_3, U12'_3, PLUS_2, ACTIVATE_1, U11_3, U12_3, plus_2, activate_1 Defined Pair Symbols: U11''_3, U12''_3, PLUS'_2, ACTIVATE'_1, U11'''_3, U12'''_3, PLUS''_2, ACTIVATE''_1 Compound Symbols: c7_3, c8_3, c9, c10_1, c11, c12_4, c13_4, c14_4, c15_4, c16, c17_1, c18 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: PLUS''(z0, 0) -> c16 ACTIVATE''(z0) -> c18 ACTIVATE'(z0) -> c11 PLUS'(z0, 0) -> c9 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 Tuples: U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1)) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0)) PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) S tuples: U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z0)) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1)), ACTIVATE'(z0), ACTIVATE'(z1), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z1)) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0)), ACTIVATE'(z1), ACTIVATE'(z0), ACTIVATE''(z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) K tuples:none Defined Rule Symbols: U11'_3, U12'_3, PLUS_2, ACTIVATE_1, U11_3, U12_3, plus_2, activate_1 Defined Pair Symbols: U11''_3, U12''_3, PLUS'_2, U11'''_3, U12'''_3, PLUS''_2 Compound Symbols: c7_3, c8_3, c10_1, c12_4, c13_4, c14_4, c15_4, c17_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 16 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 Tuples: PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0))) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) S tuples: PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) K tuples:none Defined Rule Symbols: U11'_3, U12'_3, PLUS_2, ACTIVATE_1, U11_3, U12_3, plus_2, activate_1 Defined Pair Symbols: PLUS'_2, PLUS''_2, U11''_3, U12''_3, U11'''_3, U12'''_3 Compound Symbols: c10_1, c17_1, c7_1, c8_1, c12_1, c13_1, c14_1, c15_1 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: activate(z0) -> z0 Tuples: PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0))) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) S tuples: PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) K tuples:none Defined Rule Symbols: activate_1 Defined Pair Symbols: PLUS'_2, PLUS''_2, U11''_3, U12''_3, U11'''_3, U12'''_3 Compound Symbols: c10_1, c17_1, c7_1, c8_1, c12_1, c13_1, c14_1, c15_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) We considered the (Usable) Rules: activate(z0) -> z0 And the Tuples: PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0))) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(PLUS'(x_1, x_2)) = x_1 POL(PLUS''(x_1, x_2)) = x_1 + x_2 POL(U11''(x_1, x_2, x_3)) = x_3 POL(U11'''(x_1, x_2, x_3)) = x_2 + x_3 POL(U12''(x_1, x_2, x_3)) = x_3 POL(U12'''(x_1, x_2, x_3)) = x_2 + x_3 POL(activate(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 POL(tt) = [1] ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: activate(z0) -> z0 Tuples: PLUS'(z0, s(z1)) -> c10(U11''(tt, z1, z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) U11''(tt, z0, z1) -> c7(U12''(tt, activate(z0), activate(z1))) U12''(tt, z0, z1) -> c8(PLUS'(activate(z1), activate(z0))) U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) S tuples: U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) K tuples: PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) Defined Rule Symbols: activate_1 Defined Pair Symbols: PLUS'_2, PLUS''_2, U11''_3, U12''_3, U11'''_3, U12'''_3 Compound Symbols: c10_1, c17_1, c7_1, c8_1, c12_1, c13_1, c14_1, c15_1 ---------------------------------------- (13) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: U11'''(tt, z0, z1) -> c12(U12'''(tt, activate(z0), activate(z1))) U11'''(tt, z0, z1) -> c13(U12'''(tt, activate(z0), activate(z1))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c14(PLUS''(activate(z1), activate(z0))) U12'''(tt, z0, z1) -> c15(PLUS''(activate(z1), activate(z0))) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) PLUS''(z0, s(z1)) -> c17(U11'''(tt, z1, z0)) Now S is empty ---------------------------------------- (14) BOUNDS(1, 1) ---------------------------------------- (15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (16) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (17) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence PLUS(z0, s(z1)) ->^+ c5(c1(c2(PLUS(activate(z0), z1), ACTIVATE(z0)), ACTIVATE(z0))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0]. The pumping substitution is [z1 / s(z1)]. The result substitution is [z0 / activate(z0)]. ---------------------------------------- (18) Complex Obligation (BEST) ---------------------------------------- (19) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (20) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (21) BOUNDS(n^1, INF) ---------------------------------------- (22) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: U11'(tt, z0, z1) -> c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0)) U11'(tt, z0, z1) -> c1(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c2(PLUS(activate(z1), activate(z0)), ACTIVATE(z1)) U12'(tt, z0, z1) -> c3(PLUS(activate(z1), activate(z0)), ACTIVATE(z0)) PLUS(z0, 0) -> c4 PLUS(z0, s(z1)) -> c5(U11'(tt, z1, z0)) ACTIVATE(z0) -> c6 The (relative) TRS S consists of the following rules: U11(tt, z0, z1) -> U12(tt, activate(z0), activate(z1)) U12(tt, z0, z1) -> s(plus(activate(z1), activate(z0))) plus(z0, 0) -> z0 plus(z0, s(z1)) -> U11(tt, z1, z0) activate(z0) -> z0 Rewrite Strategy: INNERMOST