WORST_CASE(?,O(n^1)) proof of input_MOfsysFWEw.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) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 47 ms] (10) CdtProblem (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (12) 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: f(0) -> true f(1) -> false f(s(x)) -> f(x) if(true, s(x), s(y)) -> s(x) if(false, s(x), s(y)) -> s(y) g(x, c(y)) -> c(g(x, y)) g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 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: f(0) -> true f(1) -> false f(s(z0)) -> f(z0) if(true, s(z0), s(z1)) -> s(z0) if(false, s(z0), s(z1)) -> s(z1) g(z0, c(z1)) -> c(g(z0, z1)) g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1))) Tuples: F(0) -> c1 F(1) -> c2 F(s(z0)) -> c3(F(z0)) IF(true, s(z0), s(z1)) -> c4 IF(false, s(z0), s(z1)) -> c5 G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0)) G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1)) S tuples: F(0) -> c1 F(1) -> c2 F(s(z0)) -> c3(F(z0)) IF(true, s(z0), s(z1)) -> c4 IF(false, s(z0), s(z1)) -> c5 G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0)) G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1)) K tuples:none Defined Rule Symbols: f_1, if_3, g_2 Defined Pair Symbols: F_1, IF_3, G_2 Compound Symbols: c1, c2, c3_1, c4, c5, c6_1, c7_3, c8_3 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: F(1) -> c2 IF(false, s(z0), s(z1)) -> c5 F(0) -> c1 IF(true, s(z0), s(z1)) -> c4 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(0) -> true f(1) -> false f(s(z0)) -> f(z0) if(true, s(z0), s(z1)) -> s(z0) if(false, s(z0), s(z1)) -> s(z1) g(z0, c(z1)) -> c(g(z0, z1)) g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1))) Tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0)) G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1)) S tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0)) G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1)) K tuples:none Defined Rule Symbols: f_1, if_3, g_2 Defined Pair Symbols: F_1, G_2 Compound Symbols: c3_1, c6_1, c7_3, c8_3 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing tuple parts ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(0) -> true f(1) -> false f(s(z0)) -> f(z0) if(true, s(z0), s(z1)) -> s(z0) if(false, s(z0), s(z1)) -> s(z1) g(z0, c(z1)) -> c(g(z0, z1)) g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1))) Tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) S tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) K tuples:none Defined Rule Symbols: f_1, if_3, g_2 Defined Pair Symbols: F_1, G_2 Compound Symbols: c3_1, c6_1, c7_1, c8_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f(0) -> true f(1) -> false f(s(z0)) -> f(z0) if(true, s(z0), s(z1)) -> s(z0) if(false, s(z0), s(z1)) -> s(z1) g(z0, c(z1)) -> c(g(z0, z1)) g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1))) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) S tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_1, G_2 Compound Symbols: c3_1, c6_1, c7_1, c8_1 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) We considered the (Usable) Rules:none And the Tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1)) = [2] + [2]x_1 POL(G(x_1, x_2)) = [1] + [2]x_1 + [3]x_2 POL(c(x_1)) = [3] + x_1 POL(c3(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) S tuples:none K tuples: F(s(z0)) -> c3(F(z0)) G(z0, c(z1)) -> c6(G(z0, z1)) G(z0, c(z1)) -> c7(F(z0)) G(z0, c(z1)) -> c8(G(s(z0), z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1, G_2 Compound Symbols: c3_1, c6_1, c7_1, c8_1 ---------------------------------------- (11) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (12) BOUNDS(1, 1)