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 CpxTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxTRS (1) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxWeightedTrs (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxTypedWeightedTrs (5) CompletionProof [UPPER BOUND(ID), 0 ms] (6) CpxTypedWeightedCompleteTrs (7) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (8) CpxRNTS (9) CompleteCoflocoProof [FINISHED, 157 ms] (10) BOUNDS(1, n^1) (11) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (12) TRS for Loop Detection (13) DecreasingLoopProof [LOWER BOUND(ID), 32 ms] (14) BEST (15) proven lower bound (16) LowerBoundPropagationProof [FINISHED, 0 ms] (17) BOUNDS(n^1, INF) (18) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: first(0, X) -> nil first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) from(X) -> cons(X, n__from(s(X))) first(X1, X2) -> n__first(X1, X2) from(X) -> n__from(X) activate(n__first(X1, X2)) -> first(X1, X2) activate(n__from(X)) -> from(X) activate(X) -> X S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (2) 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: first(0, X) -> nil [1] first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) [1] from(X) -> cons(X, n__from(s(X))) [1] first(X1, X2) -> n__first(X1, X2) [1] from(X) -> n__from(X) [1] activate(n__first(X1, X2)) -> first(X1, X2) [1] activate(n__from(X)) -> from(X) [1] activate(X) -> X [1] Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: first(0, X) -> nil [1] first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) [1] from(X) -> cons(X, n__from(s(X))) [1] first(X1, X2) -> n__first(X1, X2) [1] from(X) -> n__from(X) [1] activate(n__first(X1, X2)) -> first(X1, X2) [1] activate(n__from(X)) -> from(X) [1] activate(X) -> X [1] The TRS has the following type information: first :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from 0 :: 0:s nil :: nil:cons:n__first:n__from s :: 0:s -> 0:s cons :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from n__first :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from activate :: nil:cons:n__first:n__from -> nil:cons:n__first:n__from from :: 0:s -> nil:cons:n__first:n__from n__from :: 0:s -> nil:cons:n__first:n__from Rewrite Strategy: INNERMOST ---------------------------------------- (5) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: none And the following fresh constants: none ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: first(0, X) -> nil [1] first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) [1] from(X) -> cons(X, n__from(s(X))) [1] first(X1, X2) -> n__first(X1, X2) [1] from(X) -> n__from(X) [1] activate(n__first(X1, X2)) -> first(X1, X2) [1] activate(n__from(X)) -> from(X) [1] activate(X) -> X [1] The TRS has the following type information: first :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from 0 :: 0:s nil :: nil:cons:n__first:n__from s :: 0:s -> 0:s cons :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from n__first :: 0:s -> nil:cons:n__first:n__from -> nil:cons:n__first:n__from activate :: nil:cons:n__first:n__from -> nil:cons:n__first:n__from from :: 0:s -> nil:cons:n__first:n__from n__from :: 0:s -> nil:cons:n__first:n__from Rewrite Strategy: INNERMOST ---------------------------------------- (7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 nil => 0 ---------------------------------------- (8) Obligation: Complexity RNTS consisting of the following rules: activate(z) -{ 1 }-> X :|: X >= 0, z = X activate(z) -{ 1 }-> from(X) :|: z = 1 + X, X >= 0 activate(z) -{ 1 }-> first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 first(z, z') -{ 1 }-> 0 :|: z' = X, X >= 0, z = 0 first(z, z') -{ 1 }-> 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2 first(z, z') -{ 1 }-> 1 + Y + (1 + X + activate(Z)) :|: Z >= 0, z = 1 + X, Y >= 0, X >= 0, z' = 1 + Y + Z from(z) -{ 1 }-> 1 + X :|: X >= 0, z = X from(z) -{ 1 }-> 1 + X + (1 + (1 + X)) :|: X >= 0, z = X Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (9) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V),0,[first(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[from(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[activate(V1, Out)],[V1 >= 0]). eq(first(V1, V, Out),1,[],[Out = 0,V = X3,X3 >= 0,V1 = 0]). eq(first(V1, V, Out),1,[activate(Z1, Ret11)],[Out = 2 + Ret11 + X4 + Y1,Z1 >= 0,V1 = 1 + X4,Y1 >= 0,X4 >= 0,V = 1 + Y1 + Z1]). eq(from(V1, Out),1,[],[Out = 3 + 2*X5,X5 >= 0,V1 = X5]). eq(first(V1, V, Out),1,[],[Out = 1 + X11 + X21,X11 >= 0,X21 >= 0,V1 = X11,V = X21]). eq(from(V1, Out),1,[],[Out = 1 + X6,X6 >= 0,V1 = X6]). eq(activate(V1, Out),1,[first(X12, X22, Ret)],[Out = Ret,X12 >= 0,X22 >= 0,V1 = 1 + X12 + X22]). eq(activate(V1, Out),1,[from(X7, Ret1)],[Out = Ret1,V1 = 1 + X7,X7 >= 0]). eq(activate(V1, Out),1,[],[Out = X8,X8 >= 0,V1 = X8]). input_output_vars(first(V1,V,Out),[V1,V],[Out]). input_output_vars(from(V1,Out),[V1],[Out]). input_output_vars(activate(V1,Out),[V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [from/2] 1. recursive : [activate/2,first/3] 2. non_recursive : [start/2] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into from/2 1. SCC is partially evaluated into activate/2 2. SCC is partially evaluated into start/2 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations from/2 * CE 10 is refined into CE [12] * CE 11 is refined into CE [13] ### Cost equations --> "Loop" of from/2 * CEs [12] --> Loop 7 * CEs [13] --> Loop 8 ### Ranking functions of CR from(V1,Out) #### Partial ranking functions of CR from(V1,Out) ### Specialization of cost equations activate/2 * CE 5 is refined into CE [14] * CE 9 is refined into CE [15] * CE 7 is refined into CE [16] * CE 8 is refined into CE [17,18] * CE 6 is refined into CE [19] ### Cost equations --> "Loop" of activate/2 * CEs [19] --> Loop 9 * CEs [18] --> Loop 10 * CEs [14,15,17] --> Loop 11 * CEs [16] --> Loop 12 ### Ranking functions of CR activate(V1,Out) * RF of phase [9]: [V1-2] #### Partial ranking functions of CR activate(V1,Out) * Partial RF of phase [9]: - RF of loop [9:1]: V1-2 ### Specialization of cost equations start/2 * CE 1 is refined into CE [20] * CE 2 is refined into CE [21,22,23,24,25,26] * CE 3 is refined into CE [27,28] * CE 4 is refined into CE [29,30,31,32,33,34] ### Cost equations --> "Loop" of start/2 * CEs [20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] --> Loop 13 ### Ranking functions of CR start(V1,V) #### Partial ranking functions of CR start(V1,V) Computing Bounds ===================================== #### Cost of chains of from(V1,Out): * Chain [8]: 1 with precondition: [V1+1=Out,V1>=0] * Chain [7]: 1 with precondition: [2*V1+3=Out,V1>=0] #### Cost of chains of activate(V1,Out): * Chain [[9],12]: 2*it(9)+2 Such that:it(9) =< V1 with precondition: [Out>=2,V1>=Out+2] * Chain [[9],11]: 2*it(9)+2 Such that:it(9) =< V1 with precondition: [3*Out>=2*V1,V1>=Out+1] * Chain [[9],10]: 2*it(9)+2 Such that:it(9) =< V1 with precondition: [3*Out>=2*V1+7,2*V1>=Out+3] * Chain [12]: 2 with precondition: [Out=0,V1>=1] * Chain [11]: 2 with precondition: [V1=Out,V1>=0] * Chain [10]: 2 with precondition: [2*V1+1=Out,V1>=1] #### Cost of chains of start(V1,V): * Chain [13]: 6*s(1)+6*s(4)+3 Such that:aux(1) =< V1 aux(2) =< V s(4) =< aux(1) s(1) =< aux(2) with precondition: [V1>=0] Closed-form bounds of start(V1,V): ------------------------------------- * Chain [13] with precondition: [V1>=0] - Upper bound: 6*V1+3+nat(V)*6 - Complexity: n ### Maximum cost of start(V1,V): 6*V1+3+nat(V)*6 Asymptotic class: n * Total analysis performed in 94 ms. ---------------------------------------- (10) BOUNDS(1, n^1) ---------------------------------------- (11) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (12) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: first(0, X) -> nil first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) from(X) -> cons(X, n__from(s(X))) first(X1, X2) -> n__first(X1, X2) from(X) -> n__from(X) activate(n__first(X1, X2)) -> first(X1, X2) activate(n__from(X)) -> from(X) activate(X) -> X S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (13) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence activate(n__first(s(X1_0), cons(Y2_0, Z3_0))) ->^+ cons(Y2_0, n__first(X1_0, activate(Z3_0))) gives rise to a decreasing loop by considering the right hand sides subterm at position [1,1]. The pumping substitution is [Z3_0 / n__first(s(X1_0), cons(Y2_0, Z3_0))]. The result substitution is [ ]. ---------------------------------------- (14) Complex Obligation (BEST) ---------------------------------------- (15) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: first(0, X) -> nil first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) from(X) -> cons(X, n__from(s(X))) first(X1, X2) -> n__first(X1, X2) from(X) -> n__from(X) activate(n__first(X1, X2)) -> first(X1, X2) activate(n__from(X)) -> from(X) activate(X) -> X S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (16) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (17) BOUNDS(n^1, INF) ---------------------------------------- (18) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: first(0, X) -> nil first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) from(X) -> cons(X, n__from(s(X))) first(X1, X2) -> n__first(X1, X2) from(X) -> n__from(X) activate(n__first(X1, X2)) -> first(X1, X2) activate(n__from(X)) -> from(X) activate(X) -> X S is empty. Rewrite Strategy: INNERMOST