WORST_CASE(?,O(n^1)) proof of input_lVxxkHQmOG.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 43 ms] (8) CdtProblem (9) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (10) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: fib(0) -> 0 fib(s(0)) -> s(0) fib(s(s(x))) -> +(fib(s(x)), fib(x)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: fib(0) -> 0 fib(s(0)) -> s(0) fib(s(s(z0))) -> +(fib(s(z0)), fib(z0)) Tuples: FIB(0) -> c FIB(s(0)) -> c1 FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) S tuples: FIB(0) -> c FIB(s(0)) -> c1 FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) K tuples:none Defined Rule Symbols: fib_1 Defined Pair Symbols: FIB_1 Compound Symbols: c, c1, c2_1, c3_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: FIB(s(0)) -> c1 FIB(0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: fib(0) -> 0 fib(s(0)) -> s(0) fib(s(s(z0))) -> +(fib(s(z0)), fib(z0)) Tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) S tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) K tuples:none Defined Rule Symbols: fib_1 Defined Pair Symbols: FIB_1 Compound Symbols: c2_1, c3_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: fib(0) -> 0 fib(s(0)) -> s(0) fib(s(s(z0))) -> +(fib(s(z0)), fib(z0)) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) S tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: FIB_1 Compound Symbols: c2_1, c3_1 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) We considered the (Usable) Rules:none And the Tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(FIB(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(s(x_1)) = [3] + x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) S tuples:none K tuples: FIB(s(s(z0))) -> c2(FIB(s(z0))) FIB(s(s(z0))) -> c3(FIB(z0)) Defined Rule Symbols:none Defined Pair Symbols: FIB_1 Compound Symbols: c2_1, c3_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)