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), 241 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 37 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 7 ms] (14) CdtProblem (15) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (16) BOUNDS(1, 1) (17) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (18) TRS for Loop Detection (19) DecreasingLoopProof [LOWER BOUND(ID), 7 ms] (20) BEST (21) proven lower bound (22) LowerBoundPropagationProof [FINISHED, 0 ms] (23) BOUNDS(n^1, INF) (24) 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: map(Cons(x, xs)) -> Cons(f(x), map(xs)) map(Nil) -> Nil goal(xs) -> map(xs) f(x) -> *(x, x) +Full(S(x), y) -> +Full(x, S(y)) +Full(0, y) -> y The (relative) TRS S consists of the following rules: *(x, S(S(y))) -> +(x, *(x, S(y))) *(x, S(0)) -> x *(x, 0) -> 0 *(0, y) -> 0 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: map(Cons(x, xs)) -> Cons(f(x), map(xs)) map(Nil) -> Nil goal(xs) -> map(xs) f(x) -> *(x, x) +Full(S(x), y) -> +Full(x, S(y)) +Full(0, y) -> y The (relative) TRS S consists of the following rules: *(x, S(S(y))) -> +(x, *(x, S(y))) *(x, S(0)) -> x *(x, 0) -> 0 *(0, y) -> 0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, S(S(z1))) -> +(z0, *(z0, S(z1))) *(z0, S(0)) -> z0 *(z0, 0) -> 0 *(0, z0) -> 0 map(Cons(z0, z1)) -> Cons(f(z0), map(z1)) map(Nil) -> Nil goal(z0) -> map(z0) f(z0) -> *(z0, z0) +Full(S(z0), z1) -> +Full(z0, S(z1)) +Full(0, z0) -> z0 Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) *'(z0, S(0)) -> c1 *'(z0, 0) -> c2 *'(0, z0) -> c3 MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) MAP(Nil) -> c5 GOAL(z0) -> c6(MAP(z0)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) +FULL(0, z0) -> c9 S tuples: MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) MAP(Nil) -> c5 GOAL(z0) -> c6(MAP(z0)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) +FULL(0, z0) -> c9 K tuples:none Defined Rule Symbols: map_1, goal_1, f_1, +Full_2, *_2 Defined Pair Symbols: *'_2, MAP_1, GOAL_1, F_1, +FULL_2 Compound Symbols: c_1, c1, c2, c3, c4_2, c5, c6_1, c7_1, c8_1, c9 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: GOAL(z0) -> c6(MAP(z0)) Removed 5 trailing nodes: *'(z0, S(0)) -> c1 +FULL(0, z0) -> c9 MAP(Nil) -> c5 *'(0, z0) -> c3 *'(z0, 0) -> c2 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, S(S(z1))) -> +(z0, *(z0, S(z1))) *(z0, S(0)) -> z0 *(z0, 0) -> 0 *(0, z0) -> 0 map(Cons(z0, z1)) -> Cons(f(z0), map(z1)) map(Nil) -> Nil goal(z0) -> map(z0) f(z0) -> *(z0, z0) +Full(S(z0), z1) -> +Full(z0, S(z1)) +Full(0, z0) -> z0 Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) S tuples: MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) K tuples:none Defined Rule Symbols: map_1, goal_1, f_1, +Full_2, *_2 Defined Pair Symbols: *'_2, MAP_1, F_1, +FULL_2 Compound Symbols: c_1, c4_2, c7_1, c8_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: *(z0, S(S(z1))) -> +(z0, *(z0, S(z1))) *(z0, S(0)) -> z0 *(z0, 0) -> 0 *(0, z0) -> 0 map(Cons(z0, z1)) -> Cons(f(z0), map(z1)) map(Nil) -> Nil goal(z0) -> map(z0) f(z0) -> *(z0, z0) +Full(S(z0), z1) -> +Full(z0, S(z1)) +Full(0, z0) -> z0 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) S tuples: MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: *'_2, MAP_1, F_1, +FULL_2 Compound Symbols: c_1, c4_2, 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. +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) We considered the (Usable) Rules:none And the Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*'(x_1, x_2)) = [1] + x_2 POL(+FULL(x_1, x_2)) = x_1 POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(F(x_1)) = [1] + x_1 POL(MAP(x_1)) = x_1 POL(S(x_1)) = [1] + x_1 POL(c(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) S tuples: MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) K tuples: +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) Defined Rule Symbols:none Defined Pair Symbols: *'_2, MAP_1, F_1, +FULL_2 Compound Symbols: c_1, c4_2, c7_1, c8_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. F(z0) -> c7(*'(z0, z0)) We considered the (Usable) Rules:none And the Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*'(x_1, x_2)) = x_1 POL(+FULL(x_1, x_2)) = x_2 POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(F(x_1)) = [1] + x_1 POL(MAP(x_1)) = x_1 POL(S(x_1)) = 0 POL(c(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) S tuples: MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) K tuples: +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) F(z0) -> c7(*'(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: *'_2, MAP_1, F_1, +FULL_2 Compound Symbols: c_1, c4_2, c7_1, c8_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. MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) We considered the (Usable) Rules:none And the Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*'(x_1, x_2)) = x_2 POL(+FULL(x_1, x_2)) = 0 POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(F(x_1)) = x_1 POL(MAP(x_1)) = x_1 POL(S(x_1)) = [1] + x_1 POL(c(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, S(S(z1))) -> c(*'(z0, S(z1))) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) F(z0) -> c7(*'(z0, z0)) +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) S tuples:none K tuples: +FULL(S(z0), z1) -> c8(+FULL(z0, S(z1))) F(z0) -> c7(*'(z0, z0)) MAP(Cons(z0, z1)) -> c4(F(z0), MAP(z1)) Defined Rule Symbols:none Defined Pair Symbols: *'_2, MAP_1, F_1, +FULL_2 Compound Symbols: c_1, c4_2, c7_1, c8_1 ---------------------------------------- (15) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (16) BOUNDS(1, 1) ---------------------------------------- (17) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (18) 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: map(Cons(x, xs)) -> Cons(f(x), map(xs)) map(Nil) -> Nil goal(xs) -> map(xs) f(x) -> *(x, x) +Full(S(x), y) -> +Full(x, S(y)) +Full(0, y) -> y The (relative) TRS S consists of the following rules: *(x, S(S(y))) -> +(x, *(x, S(y))) *(x, S(0)) -> x *(x, 0) -> 0 *(0, y) -> 0 Rewrite Strategy: INNERMOST ---------------------------------------- (19) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence map(Cons(x, xs)) ->^+ Cons(f(x), map(xs)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [xs / Cons(x, xs)]. The result substitution is [ ]. ---------------------------------------- (20) Complex Obligation (BEST) ---------------------------------------- (21) 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: map(Cons(x, xs)) -> Cons(f(x), map(xs)) map(Nil) -> Nil goal(xs) -> map(xs) f(x) -> *(x, x) +Full(S(x), y) -> +Full(x, S(y)) +Full(0, y) -> y The (relative) TRS S consists of the following rules: *(x, S(S(y))) -> +(x, *(x, S(y))) *(x, S(0)) -> x *(x, 0) -> 0 *(0, y) -> 0 Rewrite Strategy: INNERMOST ---------------------------------------- (22) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (23) BOUNDS(n^1, INF) ---------------------------------------- (24) 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: map(Cons(x, xs)) -> Cons(f(x), map(xs)) map(Nil) -> Nil goal(xs) -> map(xs) f(x) -> *(x, x) +Full(S(x), y) -> +Full(x, S(y)) +Full(0, y) -> y The (relative) TRS S consists of the following rules: *(x, S(S(y))) -> +(x, *(x, S(y))) *(x, S(0)) -> x *(x, 0) -> 0 *(0, y) -> 0 Rewrite Strategy: INNERMOST