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), 329 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 50 ms] (14) CdtProblem (15) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CdtProblem (21) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 8 ms] (28) CdtProblem (29) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (30) BOUNDS(1, 1) (31) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (32) TRS for Loop Detection (33) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (34) BEST (35) proven lower bound (36) LowerBoundPropagationProof [FINISHED, 0 ms] (37) BOUNDS(n^1, INF) (38) 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: P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 The (relative) TRS S consists of the following rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 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: P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 The (relative) TRS S consists of the following rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 Tuples: P'(0) -> c10 P'(s(z0)) -> c11 LE'(0, z0) -> c12 LE'(s(z0), 0) -> c13 LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) MINUS'(z0, 0) -> c15 MINUS'(z0, s(z1)) -> c16(IF'(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1))) IF'(true, z0, z1) -> c17 IF'(false, z0, z1) -> c18 P''(0) -> c19 P''(s(z0)) -> c20 LE''(0, z0) -> c21 LE''(s(z0), 0) -> c22 LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, 0) -> c24 MINUS''(z0, s(z1)) -> c25(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), P''(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), MINUS''(z0, p(s(z1))), P'(s(z1)), P''(s(z1))) IF''(true, z0, z1) -> c27 IF''(false, z0, z1) -> c28 S tuples: P''(0) -> c19 P''(s(z0)) -> c20 LE''(0, z0) -> c21 LE''(s(z0), 0) -> c22 LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, 0) -> c24 MINUS''(z0, s(z1)) -> c25(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), P''(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), MINUS''(z0, p(s(z1))), P'(s(z1)), P''(s(z1))) IF''(true, z0, z1) -> c27 IF''(false, z0, z1) -> c28 K tuples:none Defined Rule Symbols: P_1, LE_2, MINUS_2, IF_3, p_1, le_2, minus_2, if_3 Defined Pair Symbols: P'_1, LE'_2, MINUS'_2, IF'_3, P''_1, LE''_2, MINUS''_2, IF''_3 Compound Symbols: c10, c11, c12, c13, c14_1, c15, c16_5, c17, c18, c19, c20, c21, c22, c23_1, c24, c25_6, c26_11, c27, c28 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 14 trailing nodes: P''(0) -> c19 P''(s(z0)) -> c20 IF'(false, z0, z1) -> c18 P'(s(z0)) -> c11 IF''(false, z0, z1) -> c28 LE''(0, z0) -> c21 LE''(s(z0), 0) -> c22 IF'(true, z0, z1) -> c17 MINUS'(z0, 0) -> c15 IF''(true, z0, z1) -> c27 LE'(s(z0), 0) -> c13 LE'(0, z0) -> c12 P'(0) -> c10 MINUS''(z0, 0) -> c24 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) MINUS'(z0, s(z1)) -> c16(IF'(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1))) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c25(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), P''(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), MINUS''(z0, p(s(z1))), P'(s(z1)), P''(s(z1))) S tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c25(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(IF''(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE'(z0, s(z1)), P'(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), P''(minus(z0, p(s(z1)))), MINUS'(z0, p(s(z1))), P'(s(z1)), MINUS''(z0, p(s(z1))), P'(s(z1)), P''(s(z1))) K tuples:none Defined Rule Symbols: P_1, LE_2, MINUS_2, IF_3, p_1, le_2, minus_2, if_3 Defined Pair Symbols: LE'_2, MINUS'_2, LE''_2, MINUS''_2 Compound Symbols: c14_1, c16_5, c23_1, c25_6, c26_11 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 13 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c25(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) S tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c25(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) K tuples:none Defined Rule Symbols: P_1, LE_2, MINUS_2, IF_3, p_1, le_2, minus_2, if_3 Defined Pair Symbols: LE'_2, LE''_2, MINUS'_2, MINUS''_2 Compound Symbols: c14_1, c23_1, c16_2, c25_3, c26_4 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) S tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) K tuples:none Defined Rule Symbols: P_1, LE_2, MINUS_2, IF_3, p_1, le_2, minus_2, if_3 Defined Pair Symbols: LE'_2, LE''_2, MINUS'_2, MINUS''_2 Compound Symbols: c14_1, c23_1, c16_2, c26_4, c10_1 ---------------------------------------- (11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: p(0) -> 0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) S tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) K tuples:none Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS'_2, MINUS''_2 Compound Symbols: c14_1, c23_1, c16_2, c26_4, c10_1 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) We considered the (Usable) Rules: p(s(z0)) -> z0 And the Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(LE'(x_1, x_2)) = 0 POL(LE''(x_1, x_2)) = x_1 + x_2 POL(MINUS'(x_1, x_2)) = 0 POL(MINUS''(x_1, x_2)) = [1] + x_1 + x_2 POL(c10(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c16(x_1, x_2)) = x_1 + x_2 POL(c23(x_1)) = x_1 POL(c26(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(p(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) S tuples: MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS'_2, MINUS''_2 Compound Symbols: c14_1, c23_1, c16_2, c26_4, c10_1 ---------------------------------------- (15) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MINUS'(z0, s(z1)) -> c16(LE'(z0, s(z1)), MINUS'(z0, p(s(z1)))) by MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) S tuples: MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c26_4, c10_1, c16_2 ---------------------------------------- (17) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, p(s(z1))), MINUS'(z0, p(s(z1))), MINUS''(z0, p(s(z1)))) by MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) S tuples: MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (19) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) by MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) S tuples: MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (21) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, p(s(z0))), MINUS''(x0, p(s(z0)))) by MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, z0), MINUS''(x0, p(s(z0)))) ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, z0), MINUS''(x0, p(s(z0)))) S tuples: MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, z0), MINUS''(x0, p(s(z0)))) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (23) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MINUS''(x0, s(z0)) -> c26(LE'(x0, s(z0)), MINUS'(x0, z0), MINUS'(x0, z0), MINUS''(x0, p(s(z0)))) by MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) S tuples: MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols: p_1 Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (25) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: p(s(z0)) -> z0 ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) S tuples: MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) Defined Rule Symbols:none Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(LE'(x_1, x_2)) = 0 POL(LE''(x_1, x_2)) = [1] + x_1 POL(MINUS'(x_1, x_2)) = 0 POL(MINUS''(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c16(x_1, x_2)) = x_1 + x_2 POL(c23(x_1)) = x_1 POL(c26(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: LE'(s(z0), s(z1)) -> c14(LE'(z0, z1)) LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS'(x0, s(z0)) -> c16(LE'(x0, s(z0)), MINUS'(x0, z0)) MINUS''(x0, s(z0)) -> c10(MINUS'(x0, z0)) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) S tuples:none K tuples: LE''(s(z0), s(z1)) -> c23(LE''(z0, z1)) MINUS''(z0, s(z1)) -> c10(LE'(z0, s(z1))) MINUS''(z0, s(z1)) -> c10(MINUS'(z0, p(s(z1)))) MINUS''(z0, s(z1)) -> c10(LE''(z0, s(z1))) MINUS''(z0, s(z1)) -> c26(LE'(z0, s(z1)), MINUS'(z0, z1), MINUS'(z0, z1), MINUS''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: LE'_2, LE''_2, MINUS''_2, MINUS'_2 Compound Symbols: c14_1, c23_1, c10_1, c16_2, c26_4 ---------------------------------------- (29) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (30) BOUNDS(1, 1) ---------------------------------------- (31) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (32) 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: P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 The (relative) TRS S consists of the following rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 Rewrite Strategy: INNERMOST ---------------------------------------- (33) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence LE(s(z0), s(z1)) ->^+ c4(LE(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (34) Complex Obligation (BEST) ---------------------------------------- (35) 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: P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 The (relative) TRS S consists of the following rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 Rewrite Strategy: INNERMOST ---------------------------------------- (36) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (37) BOUNDS(n^1, INF) ---------------------------------------- (38) 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: P(0) -> c P(s(z0)) -> c1 LE(0, z0) -> c2 LE(s(z0), 0) -> c3 LE(s(z0), s(z1)) -> c4(LE(z0, z1)) MINUS(z0, 0) -> c5 MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1))) MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1))) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9 The (relative) TRS S consists of the following rules: p(0) -> 0 p(s(z0)) -> z0 le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) minus(z0, 0) -> z0 minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 Rewrite Strategy: INNERMOST