WORST_CASE(?,O(n^1)) proof of input_3evJRlrxji.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 218 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxWeightedTrs (5) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (14) CpxRNTS (15) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 617 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 69 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 293 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 106 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 411 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 43 ms] (36) CpxRNTS (37) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 591 ms] (40) CpxRNTS (41) IntTrsBoundProof [UPPER BOUND(ID), 74 ms] (42) CpxRNTS (43) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 428 ms] (46) CpxRNTS (47) IntTrsBoundProof [UPPER BOUND(ID), 53 ms] (48) CpxRNTS (49) FinalProof [FINISHED, 0 ms] (50) BOUNDS(1, n^1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(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: PARALLEL_INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(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: PARALLEL_INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: map(Cons(x, xs)) -> Cons(f(x), map(xs)) [1] map(Nil) -> Nil [1] goal(xs) -> map(xs) [1] f(x) -> *(x, x) [1] +Full(S(x), y) -> +Full(x, S(y)) [1] +Full(0, y) -> y [1] *(x, S(S(y))) -> +(x, *(x, S(y))) [0] *(x, S(0)) -> x [0] *(x, 0) -> 0 [0] *(0, y) -> 0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: * => times ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: map(Cons(x, xs)) -> Cons(f(x), map(xs)) [1] map(Nil) -> Nil [1] goal(xs) -> map(xs) [1] f(x) -> times(x, x) [1] +Full(S(x), y) -> +Full(x, S(y)) [1] +Full(0, y) -> y [1] times(x, S(S(y))) -> +(x, times(x, S(y))) [0] times(x, S(0)) -> x [0] times(x, 0) -> 0 [0] times(0, y) -> 0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: map(Cons(x, xs)) -> Cons(f(x), map(xs)) [1] map(Nil) -> Nil [1] goal(xs) -> map(xs) [1] f(x) -> times(x, x) [1] +Full(S(x), y) -> +Full(x, S(y)) [1] +Full(0, y) -> y [1] times(x, S(S(y))) -> +(x, times(x, S(y))) [0] times(x, S(0)) -> x [0] times(x, 0) -> 0 [0] times(0, y) -> 0 [0] The TRS has the following type information: map :: Cons:Nil -> Cons:Nil Cons :: S:0:+ -> Cons:Nil -> Cons:Nil f :: S:0:+ -> S:0:+ Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil times :: S:0:+ -> S:0:+ -> S:0:+ +Full :: S:0:+ -> S:0:+ -> S:0:+ S :: S:0:+ -> S:0:+ 0 :: S:0:+ + :: S:0:+ -> S:0:+ -> S:0:+ Rewrite Strategy: INNERMOST ---------------------------------------- (9) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: map_1 goal_1 f_1 +Full_2 (c) The following functions are completely defined: times_2 Due to the following rules being added: times(v0, v1) -> 0 [0] And the following fresh constants: none ---------------------------------------- (10) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: map(Cons(x, xs)) -> Cons(f(x), map(xs)) [1] map(Nil) -> Nil [1] goal(xs) -> map(xs) [1] f(x) -> times(x, x) [1] +Full(S(x), y) -> +Full(x, S(y)) [1] +Full(0, y) -> y [1] times(x, S(S(y))) -> +(x, times(x, S(y))) [0] times(x, S(0)) -> x [0] times(x, 0) -> 0 [0] times(0, y) -> 0 [0] times(v0, v1) -> 0 [0] The TRS has the following type information: map :: Cons:Nil -> Cons:Nil Cons :: S:0:+ -> Cons:Nil -> Cons:Nil f :: S:0:+ -> S:0:+ Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil times :: S:0:+ -> S:0:+ -> S:0:+ +Full :: S:0:+ -> S:0:+ -> S:0:+ S :: S:0:+ -> S:0:+ 0 :: S:0:+ + :: S:0:+ -> S:0:+ -> S:0:+ Rewrite Strategy: INNERMOST ---------------------------------------- (11) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: map(Cons(x, xs)) -> Cons(f(x), map(xs)) [1] map(Nil) -> Nil [1] goal(xs) -> map(xs) [1] f(x) -> times(x, x) [1] +Full(S(x), y) -> +Full(x, S(y)) [1] +Full(0, y) -> y [1] times(x, S(S(y))) -> +(x, times(x, S(y))) [0] times(x, S(0)) -> x [0] times(x, 0) -> 0 [0] times(0, y) -> 0 [0] times(v0, v1) -> 0 [0] The TRS has the following type information: map :: Cons:Nil -> Cons:Nil Cons :: S:0:+ -> Cons:Nil -> Cons:Nil f :: S:0:+ -> S:0:+ Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil times :: S:0:+ -> S:0:+ -> S:0:+ +Full :: S:0:+ -> S:0:+ -> S:0:+ S :: S:0:+ -> S:0:+ 0 :: S:0:+ + :: S:0:+ -> S:0:+ -> S:0:+ Rewrite Strategy: INNERMOST ---------------------------------------- (13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: Nil => 0 0 => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> y :|: y >= 0, z = 0, z' = y +Full(z, z') -{ 1 }-> +Full(x, 1 + y) :|: x >= 0, y >= 0, z = 1 + x, z' = y f(z) -{ 1 }-> times(x, x) :|: x >= 0, z = x goal(z) -{ 1 }-> map(xs) :|: xs >= 0, z = xs map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> x :|: x >= 0, z' = 1 + 0, z = x times(z, z') -{ 0 }-> 0 :|: x >= 0, z = x, z' = 0 times(z, z') -{ 0 }-> 0 :|: y >= 0, z = 0, z' = y times(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 times(z, z') -{ 0 }-> 1 + x + times(x, 1 + y) :|: z' = 1 + (1 + y), x >= 0, y >= 0, z = x ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> times(z, z) :|: z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + times(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { times } { +Full } { f } { map } { goal } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> times(z, z) :|: z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + times(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {times}, {+Full}, {f}, {map}, {goal} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> times(z, z) :|: z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + times(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {times}, {+Full}, {f}, {map}, {goal} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: times after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: z + z*z' + z' ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> times(z, z) :|: z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + times(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {times}, {+Full}, {f}, {map}, {goal} Previous analysis results are: times: runtime: ?, size: O(n^2) [z + z*z' + z'] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: times after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> times(z, z) :|: z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + times(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {+Full}, {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {+Full}, {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: +Full after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z + z' ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {+Full}, {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: +Full after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 +Full(z, z') -{ 1 }-> +Full(z - 1, 1 + z') :|: z - 1 >= 0, z' >= 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (31) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: f after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 2*z + z^2 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {f}, {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: ?, size: O(n^2) [2*z + z^2] ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: f after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 1 }-> 1 + f(x) + map(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] ---------------------------------------- (37) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 2 }-> 1 + s1 + map(xs) :|: s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] ---------------------------------------- (39) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: map after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 2 }-> 1 + s1 + map(xs) :|: s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {map}, {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] map: runtime: ?, size: INF ---------------------------------------- (41) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: map after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + 2*z ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 1 }-> map(z) :|: z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 2 }-> 1 + s1 + map(xs) :|: s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] map: runtime: O(n^1) [1 + 2*z], size: INF ---------------------------------------- (43) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 2 + 2*z }-> s3 :|: s3 >= 0, s3 <= inf', z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 3 + 2*xs }-> 1 + s1 + s2 :|: s2 >= 0, s2 <= inf, s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] map: runtime: O(n^1) [1 + 2*z], size: INF ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: goal after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 2 + 2*z }-> s3 :|: s3 >= 0, s3 <= inf', z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 3 + 2*xs }-> 1 + s1 + s2 :|: s2 >= 0, s2 <= inf, s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: {goal} Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] map: runtime: O(n^1) [1 + 2*z], size: INF goal: runtime: ?, size: INF ---------------------------------------- (47) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: goal after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2 + 2*z ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: +Full(z, z') -{ 1 + z }-> s'' :|: s'' >= 0, s'' <= z - 1 + (1 + z'), z - 1 >= 0, z' >= 0 +Full(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 f(z) -{ 1 }-> s :|: s >= 0, s <= z * z + z + z, z >= 0 goal(z) -{ 2 + 2*z }-> s3 :|: s3 >= 0, s3 <= inf', z >= 0 map(z) -{ 1 }-> 0 :|: z = 0 map(z) -{ 3 + 2*xs }-> 1 + s1 + s2 :|: s2 >= 0, s2 <= inf, s1 >= 0, s1 <= 2 * x + x * x, z = 1 + x + xs, xs >= 0, x >= 0 times(z, z') -{ 0 }-> z :|: z >= 0, z' = 1 + 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0 times(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0 times(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 times(z, z') -{ 0 }-> 1 + z + s' :|: s' >= 0, s' <= (1 + (z' - 2)) * z + (1 + (z' - 2)) + z, z >= 0, z' - 2 >= 0 Function symbols to be analyzed: Previous analysis results are: times: runtime: O(1) [0], size: O(n^2) [z + z*z' + z'] +Full: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] f: runtime: O(1) [1], size: O(n^2) [2*z + z^2] map: runtime: O(n^1) [1 + 2*z], size: INF goal: runtime: O(n^1) [2 + 2*z], size: INF ---------------------------------------- (49) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (50) BOUNDS(1, n^1)