WORST_CASE(?,O(n^1)) proof of input_8ezI11cnGS.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), 202 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), 428 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 80 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 3052 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 1025 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 1 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 148 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 53 ms] (36) CpxRNTS (37) FinalProof [FINISHED, 0 ms] (38) 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: merge(Cons(x, xs), Nil) -> Cons(x, xs) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Nil, ys) -> ys goal(xs, ys) -> merge(xs, ys) The (relative) TRS S consists of the following rules: <=(S(x), S(y)) -> <=(x, y) <=(0, y) -> True <=(S(x), 0) -> False merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) 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: merge(Cons(x, xs), Nil) -> Cons(x, xs) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Nil, ys) -> ys goal(xs, ys) -> merge(xs, ys) The (relative) TRS S consists of the following rules: <=(S(x), S(y)) -> <=(x, y) <=(0, y) -> True <=(S(x), 0) -> False merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) 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: merge(Cons(x, xs), Nil) -> Cons(x, xs) [1] merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) [1] merge(Nil, ys) -> ys [1] goal(xs, ys) -> merge(xs, ys) [1] <=(S(x), S(y)) -> <=(x, y) [0] <=(0, y) -> True [0] <=(S(x), 0) -> False [0] merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) [0] merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: <= => lteq ---------------------------------------- (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: merge(Cons(x, xs), Nil) -> Cons(x, xs) [1] merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](lteq(x', x), Cons(x', xs'), Cons(x, xs)) [1] merge(Nil, ys) -> ys [1] goal(xs, ys) -> merge(xs, ys) [1] lteq(S(x), S(y)) -> lteq(x, y) [0] lteq(0, y) -> True [0] lteq(S(x), 0) -> False [0] merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) [0] merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) [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: merge(Cons(x, xs), Nil) -> Cons(x, xs) [1] merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](lteq(x', x), Cons(x', xs'), Cons(x, xs)) [1] merge(Nil, ys) -> ys [1] goal(xs, ys) -> merge(xs, ys) [1] lteq(S(x), S(y)) -> lteq(x, y) [0] lteq(0, y) -> True [0] lteq(S(x), 0) -> False [0] merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) [0] merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) [0] The TRS has the following type information: merge :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: S:0 -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil lteq :: S:0 -> S:0 -> True:False goal :: Cons:Nil -> Cons:Nil -> Cons:Nil S :: S:0 -> S:0 0 :: S:0 True :: True:False False :: True:False 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: merge_2 goal_2 (c) The following functions are completely defined: lteq_2 merge[Ite]_3 Due to the following rules being added: lteq(v0, v1) -> null_lteq [0] merge[Ite](v0, v1, v2) -> Nil [0] And the following fresh constants: null_lteq ---------------------------------------- (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: merge(Cons(x, xs), Nil) -> Cons(x, xs) [1] merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](lteq(x', x), Cons(x', xs'), Cons(x, xs)) [1] merge(Nil, ys) -> ys [1] goal(xs, ys) -> merge(xs, ys) [1] lteq(S(x), S(y)) -> lteq(x, y) [0] lteq(0, y) -> True [0] lteq(S(x), 0) -> False [0] merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) [0] merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) [0] lteq(v0, v1) -> null_lteq [0] merge[Ite](v0, v1, v2) -> Nil [0] The TRS has the following type information: merge :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: S:0 -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge[Ite] :: True:False:null_lteq -> Cons:Nil -> Cons:Nil -> Cons:Nil lteq :: S:0 -> S:0 -> True:False:null_lteq goal :: Cons:Nil -> Cons:Nil -> Cons:Nil S :: S:0 -> S:0 0 :: S:0 True :: True:False:null_lteq False :: True:False:null_lteq null_lteq :: True:False:null_lteq 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: merge(Cons(x, xs), Nil) -> Cons(x, xs) [1] merge(Cons(S(x''), xs'), Cons(S(y'), xs)) -> merge[Ite](lteq(x'', y'), Cons(S(x''), xs'), Cons(S(y'), xs)) [1] merge(Cons(0, xs'), Cons(x, xs)) -> merge[Ite](True, Cons(0, xs'), Cons(x, xs)) [1] merge(Cons(S(x1), xs'), Cons(0, xs)) -> merge[Ite](False, Cons(S(x1), xs'), Cons(0, xs)) [1] merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](null_lteq, Cons(x', xs'), Cons(x, xs)) [1] merge(Nil, ys) -> ys [1] goal(xs, ys) -> merge(xs, ys) [1] lteq(S(x), S(y)) -> lteq(x, y) [0] lteq(0, y) -> True [0] lteq(S(x), 0) -> False [0] merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs)) [0] merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys)) [0] lteq(v0, v1) -> null_lteq [0] merge[Ite](v0, v1, v2) -> Nil [0] The TRS has the following type information: merge :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: S:0 -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge[Ite] :: True:False:null_lteq -> Cons:Nil -> Cons:Nil -> Cons:Nil lteq :: S:0 -> S:0 -> True:False:null_lteq goal :: Cons:Nil -> Cons:Nil -> Cons:Nil S :: S:0 -> S:0 0 :: S:0 True :: True:False:null_lteq False :: True:False:null_lteq null_lteq :: True:False:null_lteq 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 True => 2 False => 1 null_lteq => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 1 }-> merge(xs, ys) :|: xs >= 0, z = xs, z' = ys, ys >= 0 lteq(z, z') -{ 0 }-> lteq(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x lteq(z, z') -{ 0 }-> 2 :|: y >= 0, z = 0, z' = y lteq(z, z') -{ 0 }-> 1 :|: x >= 0, z = 1 + x, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 merge(z, z') -{ 1 }-> ys :|: z' = ys, ys >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z = 1 + 0 + xs', xs' >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + xs) :|: xs >= 0, x1 >= 0, z' = 1 + 0 + xs, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, ys) :|: z = 2, xs >= 0, z' = 1 + x + xs, ys >= 0, x >= 0, z'' = ys merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs', xs) :|: xs >= 0, z = 1, xs' >= 0, x >= 0, z' = xs', z'' = 1 + x + xs ---------------------------------------- (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: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { lteq } { merge[Ite], merge } { goal } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {lteq}, {merge[Ite],merge}, {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: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {lteq}, {merge[Ite],merge}, {goal} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: lteq after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 2 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {lteq}, {merge[Ite],merge}, {goal} Previous analysis results are: lteq: runtime: ?, size: O(1) [2] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: lteq 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: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](lteq(x'', y'), 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {merge[Ite],merge}, {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (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: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](s, 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {merge[Ite],merge}, {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: merge[Ite] after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' + z'' Computed SIZE bound using CoFloCo for: merge 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: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](s, 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {merge[Ite],merge}, {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] merge[Ite]: runtime: ?, size: O(n^1) [z' + z''] merge: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: merge[Ite] after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 8 + z' + z'' Computed RUNTIME bound using CoFloCo for: merge after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 9 + z + z' ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 1 }-> merge(z, z') :|: z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> merge[Ite](s, 1 + (1 + x'') + xs', 1 + (1 + y') + xs) :|: s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 1 }-> merge[Ite](2, 1 + 0 + (z - 1), 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 1 }-> merge[Ite](1, 1 + (1 + x1) + xs', 1 + 0 + (z' - 1)) :|: z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 1 }-> merge[Ite](0, 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(xs, z'') :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 merge[Ite](z, z', z'') -{ 0 }-> 1 + x + merge(z', xs) :|: xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs Function symbols to be analyzed: {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] merge[Ite]: runtime: O(n^1) [8 + z' + z''], size: O(n^1) [z' + z''] merge: runtime: O(n^1) [9 + z + 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: goal(z, z') -{ 10 + z + z' }-> s4 :|: s4 >= 0, s4 <= z + z', z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 13 + x'' + xs + xs' + y' }-> s'' :|: s'' >= 0, s'' <= 1 + (1 + x'') + xs' + (1 + (1 + y') + xs), s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 10 + x + xs + z }-> s1 :|: s1 >= 0, s1 <= 1 + 0 + (z - 1) + (1 + x + xs), xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 11 + x1 + xs' + z' }-> s2 :|: s2 >= 0, s2 <= 1 + (1 + x1) + xs' + (1 + 0 + (z' - 1)), z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 11 + x + x' + xs + xs' }-> s3 :|: s3 >= 0, s3 <= 1 + x' + xs' + (1 + x + xs), xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 9 + xs + z' }-> 1 + x + s5 :|: s5 >= 0, s5 <= z' + xs, xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs merge[Ite](z, z', z'') -{ 9 + xs + z'' }-> 1 + x + s6 :|: s6 >= 0, s6 <= xs + z'', z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 Function symbols to be analyzed: {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] merge[Ite]: runtime: O(n^1) [8 + z' + z''], size: O(n^1) [z' + z''] merge: runtime: O(n^1) [9 + z + z'], size: O(n^1) [z + z'] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: goal after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z + z' ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 10 + z + z' }-> s4 :|: s4 >= 0, s4 <= z + z', z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 13 + x'' + xs + xs' + y' }-> s'' :|: s'' >= 0, s'' <= 1 + (1 + x'') + xs' + (1 + (1 + y') + xs), s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 10 + x + xs + z }-> s1 :|: s1 >= 0, s1 <= 1 + 0 + (z - 1) + (1 + x + xs), xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 11 + x1 + xs' + z' }-> s2 :|: s2 >= 0, s2 <= 1 + (1 + x1) + xs' + (1 + 0 + (z' - 1)), z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 11 + x + x' + xs + xs' }-> s3 :|: s3 >= 0, s3 <= 1 + x' + xs' + (1 + x + xs), xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 9 + xs + z' }-> 1 + x + s5 :|: s5 >= 0, s5 <= z' + xs, xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs merge[Ite](z, z', z'') -{ 9 + xs + z'' }-> 1 + x + s6 :|: s6 >= 0, s6 <= xs + z'', z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 Function symbols to be analyzed: {goal} Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] merge[Ite]: runtime: O(n^1) [8 + z' + z''], size: O(n^1) [z' + z''] merge: runtime: O(n^1) [9 + z + z'], size: O(n^1) [z + z'] goal: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (35) 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: 10 + z + z' ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: goal(z, z') -{ 10 + z + z' }-> s4 :|: s4 >= 0, s4 <= z + z', z >= 0, z' >= 0 lteq(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 2, z - 1 >= 0, z' - 1 >= 0 lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0 lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0 lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 merge(z, z') -{ 13 + x'' + xs + xs' + y' }-> s'' :|: s'' >= 0, s'' <= 1 + (1 + x'') + xs' + (1 + (1 + y') + xs), s >= 0, s <= 2, z = 1 + (1 + x'') + xs', xs >= 0, z' = 1 + (1 + y') + xs, xs' >= 0, y' >= 0, x'' >= 0 merge(z, z') -{ 10 + x + xs + z }-> s1 :|: s1 >= 0, s1 <= 1 + 0 + (z - 1) + (1 + x + xs), xs >= 0, z' = 1 + x + xs, z - 1 >= 0, x >= 0 merge(z, z') -{ 11 + x1 + xs' + z' }-> s2 :|: s2 >= 0, s2 <= 1 + (1 + x1) + xs' + (1 + 0 + (z' - 1)), z' - 1 >= 0, x1 >= 0, z = 1 + (1 + x1) + xs', xs' >= 0 merge(z, z') -{ 11 + x + x' + xs + xs' }-> s3 :|: s3 >= 0, s3 <= 1 + x' + xs' + (1 + x + xs), xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs' merge(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 merge(z, z') -{ 1 }-> 1 + x + xs :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0 merge[Ite](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 merge[Ite](z, z', z'') -{ 9 + xs + z' }-> 1 + x + s5 :|: s5 >= 0, s5 <= z' + xs, xs >= 0, z = 1, z' >= 0, x >= 0, z'' = 1 + x + xs merge[Ite](z, z', z'') -{ 9 + xs + z'' }-> 1 + x + s6 :|: s6 >= 0, s6 <= xs + z'', z = 2, xs >= 0, z' = 1 + x + xs, z'' >= 0, x >= 0 Function symbols to be analyzed: Previous analysis results are: lteq: runtime: O(1) [0], size: O(1) [2] merge[Ite]: runtime: O(n^1) [8 + z' + z''], size: O(n^1) [z' + z''] merge: runtime: O(n^1) [9 + z + z'], size: O(n^1) [z + z'] goal: runtime: O(n^1) [10 + z + z'], size: O(n^1) [z + z'] ---------------------------------------- (37) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (38) BOUNDS(1, n^1)