WORST_CASE(Omega(n^1),O(n^2)) proof of input_4BVyBIUxB3.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxTRS (1) RelTrsToWeightedTrsProof [UPPER BOUND(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, 2358 ms] (10) BOUNDS(1, n^2) (11) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 38 ms] (12) CdtProblem (13) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRelTRS (15) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRelTRS (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (18) typed CpxTrs (19) OrderProof [LOWER BOUND(ID), 0 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 388 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 15 ms] (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 117 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 72 ms] (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 61 ms] (34) typed CpxTrs (35) RewriteLemmaProof [LOWER BOUND(ID), 26 ms] (36) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: le(0, y) -> true le(s(x), 0) -> false le(s(x), s(y)) -> le(x, y) inc(0) -> 0 inc(s(x)) -> s(inc(x)) minus(0, y) -> 0 minus(x, 0) -> x minus(s(x), s(y)) -> minus(x, y) quot(0, s(y)) -> 0 quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) log(x) -> log2(x, 0) log2(x, y) -> if(le(x, 0), le(x, s(0)), x, inc(y)) if(true, b, x, y) -> log_undefined if(false, b, x, y) -> if2(b, x, y) if2(true, x, s(y)) -> y if2(false, x, y) -> log2(quot(x, s(s(0))), y) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToWeightedTrsProof (UPPER BOUND(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^2). The TRS R consists of the following rules: le(0, y) -> true [1] le(s(x), 0) -> false [1] le(s(x), s(y)) -> le(x, y) [1] inc(0) -> 0 [1] inc(s(x)) -> s(inc(x)) [1] minus(0, y) -> 0 [1] minus(x, 0) -> x [1] minus(s(x), s(y)) -> minus(x, y) [1] quot(0, s(y)) -> 0 [1] quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) [1] log(x) -> log2(x, 0) [1] log2(x, y) -> if(le(x, 0), le(x, s(0)), x, inc(y)) [1] if(true, b, x, y) -> log_undefined [1] if(false, b, x, y) -> if2(b, x, y) [1] if2(true, x, s(y)) -> y [1] if2(false, x, y) -> log2(quot(x, s(s(0))), y) [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: le(0, y) -> true [1] le(s(x), 0) -> false [1] le(s(x), s(y)) -> le(x, y) [1] inc(0) -> 0 [1] inc(s(x)) -> s(inc(x)) [1] minus(0, y) -> 0 [1] minus(x, 0) -> x [1] minus(s(x), s(y)) -> minus(x, y) [1] quot(0, s(y)) -> 0 [1] quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) [1] log(x) -> log2(x, 0) [1] log2(x, y) -> if(le(x, 0), le(x, s(0)), x, inc(y)) [1] if(true, b, x, y) -> log_undefined [1] if(false, b, x, y) -> if2(b, x, y) [1] if2(true, x, s(y)) -> y [1] if2(false, x, y) -> log2(quot(x, s(s(0))), y) [1] The TRS has the following type information: le :: 0:s:log_undefined -> 0:s:log_undefined -> true:false 0 :: 0:s:log_undefined true :: true:false s :: 0:s:log_undefined -> 0:s:log_undefined false :: true:false inc :: 0:s:log_undefined -> 0:s:log_undefined minus :: 0:s:log_undefined -> 0:s:log_undefined -> 0:s:log_undefined quot :: 0:s:log_undefined -> 0:s:log_undefined -> 0:s:log_undefined log :: 0:s:log_undefined -> 0:s:log_undefined log2 :: 0:s:log_undefined -> 0:s:log_undefined -> 0:s:log_undefined if :: true:false -> true:false -> 0:s:log_undefined -> 0:s:log_undefined -> 0:s:log_undefined log_undefined :: 0:s:log_undefined if2 :: true:false -> 0:s:log_undefined -> 0:s:log_undefined -> 0:s:log_undefined 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: le(v0, v1) -> null_le [0] inc(v0) -> null_inc [0] minus(v0, v1) -> null_minus [0] quot(v0, v1) -> null_quot [0] if2(v0, v1, v2) -> null_if2 [0] if(v0, v1, v2, v3) -> null_if [0] And the following fresh constants: null_le, null_inc, null_minus, null_quot, null_if2, null_if ---------------------------------------- (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: le(0, y) -> true [1] le(s(x), 0) -> false [1] le(s(x), s(y)) -> le(x, y) [1] inc(0) -> 0 [1] inc(s(x)) -> s(inc(x)) [1] minus(0, y) -> 0 [1] minus(x, 0) -> x [1] minus(s(x), s(y)) -> minus(x, y) [1] quot(0, s(y)) -> 0 [1] quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) [1] log(x) -> log2(x, 0) [1] log2(x, y) -> if(le(x, 0), le(x, s(0)), x, inc(y)) [1] if(true, b, x, y) -> log_undefined [1] if(false, b, x, y) -> if2(b, x, y) [1] if2(true, x, s(y)) -> y [1] if2(false, x, y) -> log2(quot(x, s(s(0))), y) [1] le(v0, v1) -> null_le [0] inc(v0) -> null_inc [0] minus(v0, v1) -> null_minus [0] quot(v0, v1) -> null_quot [0] if2(v0, v1, v2) -> null_if2 [0] if(v0, v1, v2, v3) -> null_if [0] The TRS has the following type information: le :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> true:false:null_le 0 :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if true :: true:false:null_le s :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if false :: true:false:null_le inc :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if minus :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if quot :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if log :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if log2 :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if if :: true:false:null_le -> true:false:null_le -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if log_undefined :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if if2 :: true:false:null_le -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if -> 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if null_le :: true:false:null_le null_inc :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if null_minus :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if null_quot :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if null_if2 :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if null_if :: 0:s:log_undefined:null_inc:null_minus:null_quot:null_if2:null_if 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 true => 2 false => 1 log_undefined => 1 null_le => 0 null_inc => 0 null_minus => 0 null_quot => 0 null_if2 => 0 null_if => 0 ---------------------------------------- (8) Obligation: Complexity RNTS consisting of the following rules: if(z, z', z'', z1) -{ 1 }-> if2(b, x, y) :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x if(z, z', z'', z1) -{ 1 }-> 1 :|: z = 2, b >= 0, z1 = y, x >= 0, y >= 0, z' = b, z'' = x if(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 if2(z, z', z'') -{ 1 }-> y :|: z = 2, z' = x, x >= 0, y >= 0, z'' = 1 + y if2(z, z', z'') -{ 1 }-> log2(quot(x, 1 + (1 + 0)), y) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0 if2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 inc(z) -{ 1 }-> 0 :|: z = 0 inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 inc(z) -{ 1 }-> 1 + inc(x) :|: x >= 0, z = 1 + x le(z, z') -{ 1 }-> le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x le(z, z') -{ 1 }-> 2 :|: y >= 0, z = 0, z' = y le(z, z') -{ 1 }-> 1 :|: x >= 0, z = 1 + x, z' = 0 le(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 log(z) -{ 1 }-> log2(x, 0) :|: x >= 0, z = x log2(z, z') -{ 1 }-> if(le(x, 0), le(x, 1 + 0), x, inc(y)) :|: x >= 0, y >= 0, z = x, z' = y minus(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0 minus(z, z') -{ 1 }-> minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x minus(z, z') -{ 1 }-> 0 :|: y >= 0, z = 0, z' = y minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 1 }-> 0 :|: z' = 1 + y, y >= 0, z = 0 quot(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 1 }-> 1 + quot(minus(x, y), 1 + y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + 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, V17, V21),0,[le(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V17, V21),0,[inc(V1, Out)],[V1 >= 0]). eq(start(V1, V, V17, V21),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V17, V21),0,[quot(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V17, V21),0,[log(V1, Out)],[V1 >= 0]). eq(start(V1, V, V17, V21),0,[log2(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V17, V21),0,[if(V1, V, V17, V21, Out)],[V1 >= 0,V >= 0,V17 >= 0,V21 >= 0]). eq(start(V1, V, V17, V21),0,[if2(V1, V, V17, Out)],[V1 >= 0,V >= 0,V17 >= 0]). eq(le(V1, V, Out),1,[],[Out = 2,V2 >= 0,V1 = 0,V = V2]). eq(le(V1, V, Out),1,[],[Out = 1,V3 >= 0,V1 = 1 + V3,V = 0]). eq(le(V1, V, Out),1,[le(V4, V5, Ret)],[Out = Ret,V = 1 + V5,V4 >= 0,V5 >= 0,V1 = 1 + V4]). eq(inc(V1, Out),1,[],[Out = 0,V1 = 0]). eq(inc(V1, Out),1,[inc(V6, Ret1)],[Out = 1 + Ret1,V6 >= 0,V1 = 1 + V6]). eq(minus(V1, V, Out),1,[],[Out = 0,V7 >= 0,V1 = 0,V = V7]). eq(minus(V1, V, Out),1,[],[Out = V8,V8 >= 0,V1 = V8,V = 0]). eq(minus(V1, V, Out),1,[minus(V9, V10, Ret2)],[Out = Ret2,V = 1 + V10,V9 >= 0,V10 >= 0,V1 = 1 + V9]). eq(quot(V1, V, Out),1,[],[Out = 0,V = 1 + V11,V11 >= 0,V1 = 0]). eq(quot(V1, V, Out),1,[minus(V13, V12, Ret10),quot(Ret10, 1 + V12, Ret11)],[Out = 1 + Ret11,V = 1 + V12,V13 >= 0,V12 >= 0,V1 = 1 + V13]). eq(log(V1, Out),1,[log2(V14, 0, Ret3)],[Out = Ret3,V14 >= 0,V1 = V14]). eq(log2(V1, V, Out),1,[le(V15, 0, Ret0),le(V15, 1 + 0, Ret12),inc(V16, Ret31),if(Ret0, Ret12, V15, Ret31, Ret4)],[Out = Ret4,V15 >= 0,V16 >= 0,V1 = V15,V = V16]). eq(if(V1, V, V17, V21, Out),1,[],[Out = 1,V1 = 2,V19 >= 0,V21 = V20,V18 >= 0,V20 >= 0,V = V19,V17 = V18]). eq(if(V1, V, V17, V21, Out),1,[if2(V22, V24, V23, Ret5)],[Out = Ret5,V22 >= 0,V21 = V23,V1 = 1,V24 >= 0,V23 >= 0,V = V22,V17 = V24]). eq(if2(V1, V, V17, Out),1,[],[Out = V25,V1 = 2,V = V26,V26 >= 0,V25 >= 0,V17 = 1 + V25]). eq(if2(V1, V, V17, Out),1,[quot(V27, 1 + (1 + 0), Ret01),log2(Ret01, V28, Ret6)],[Out = Ret6,V = V27,V17 = V28,V1 = 1,V27 >= 0,V28 >= 0]). eq(le(V1, V, Out),0,[],[Out = 0,V30 >= 0,V29 >= 0,V1 = V30,V = V29]). eq(inc(V1, Out),0,[],[Out = 0,V31 >= 0,V1 = V31]). eq(minus(V1, V, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V1 = V33,V = V32]). eq(quot(V1, V, Out),0,[],[Out = 0,V34 >= 0,V35 >= 0,V1 = V34,V = V35]). eq(if2(V1, V, V17, Out),0,[],[Out = 0,V36 >= 0,V17 = V38,V37 >= 0,V1 = V36,V = V37,V38 >= 0]). eq(if(V1, V, V17, V21, Out),0,[],[Out = 0,V21 = V42,V40 >= 0,V17 = V41,V39 >= 0,V1 = V40,V = V39,V41 >= 0,V42 >= 0]). input_output_vars(le(V1,V,Out),[V1,V],[Out]). input_output_vars(inc(V1,Out),[V1],[Out]). input_output_vars(minus(V1,V,Out),[V1,V],[Out]). input_output_vars(quot(V1,V,Out),[V1,V],[Out]). input_output_vars(log(V1,Out),[V1],[Out]). input_output_vars(log2(V1,V,Out),[V1,V],[Out]). input_output_vars(if(V1,V,V17,V21,Out),[V1,V,V17,V21],[Out]). input_output_vars(if2(V1,V,V17,Out),[V1,V,V17],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [inc/2] 1. recursive : [le/3] 2. recursive : [minus/3] 3. recursive : [quot/3] 4. recursive : [if/5,if2/4,log2/3] 5. non_recursive : [log/2] 6. non_recursive : [start/4] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into inc/2 1. SCC is partially evaluated into le/3 2. SCC is partially evaluated into minus/3 3. SCC is partially evaluated into quot/3 4. SCC is partially evaluated into log2/3 5. SCC is completely evaluated into other SCCs 6. SCC is partially evaluated into start/4 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations inc/2 * CE 26 is refined into CE [33] * CE 28 is refined into CE [34] * CE 27 is refined into CE [35] ### Cost equations --> "Loop" of inc/2 * CEs [35] --> Loop 19 * CEs [33,34] --> Loop 20 ### Ranking functions of CR inc(V1,Out) * RF of phase [19]: [V1] #### Partial ranking functions of CR inc(V1,Out) * Partial RF of phase [19]: - RF of loop [19:1]: V1 ### Specialization of cost equations le/3 * CE 25 is refined into CE [36] * CE 23 is refined into CE [37] * CE 22 is refined into CE [38] * CE 24 is refined into CE [39] ### Cost equations --> "Loop" of le/3 * CEs [39] --> Loop 21 * CEs [36] --> Loop 22 * CEs [37] --> Loop 23 * CEs [38] --> Loop 24 ### Ranking functions of CR le(V1,V,Out) * RF of phase [21]: [V,V1] #### Partial ranking functions of CR le(V1,V,Out) * Partial RF of phase [21]: - RF of loop [21:1]: V V1 ### Specialization of cost equations minus/3 * CE 30 is refined into CE [40] * CE 29 is refined into CE [41] * CE 32 is refined into CE [42] * CE 31 is refined into CE [43] ### Cost equations --> "Loop" of minus/3 * CEs [43] --> Loop 25 * CEs [40] --> Loop 26 * CEs [41,42] --> Loop 27 ### Ranking functions of CR minus(V1,V,Out) * RF of phase [25]: [V,V1] #### Partial ranking functions of CR minus(V1,V,Out) * Partial RF of phase [25]: - RF of loop [25:1]: V V1 ### Specialization of cost equations quot/3 * CE 14 is refined into CE [44] * CE 16 is refined into CE [45] * CE 15 is refined into CE [46,47,48] ### Cost equations --> "Loop" of quot/3 * CEs [48] --> Loop 28 * CEs [47] --> Loop 29 * CEs [46] --> Loop 30 * CEs [44,45] --> Loop 31 ### Ranking functions of CR quot(V1,V,Out) * RF of phase [28]: [V1-1,V1-V+1] * RF of phase [30]: [V1] #### Partial ranking functions of CR quot(V1,V,Out) * Partial RF of phase [28]: - RF of loop [28:1]: V1-1 V1-V+1 * Partial RF of phase [30]: - RF of loop [30:1]: V1 ### Specialization of cost equations log2/3 * CE 21 is refined into CE [49,50,51,52] * CE 17 is refined into CE [53,54,55,56,57,58] * CE 19 is refined into CE [59] * CE 20 is refined into CE [60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77] * CE 18 is refined into CE [78,79,80,81,82,83,84,85] ### Cost equations --> "Loop" of log2/3 * CEs [85] --> Loop 32 * CEs [81] --> Loop 33 * CEs [83,84] --> Loop 34 * CEs [79,80] --> Loop 35 * CEs [82] --> Loop 36 * CEs [78] --> Loop 37 * CEs [59] --> Loop 38 * CEs [57,58,68,69,76,77] --> Loop 39 * CEs [49,50,51,52] --> Loop 40 * CEs [53,54,55,56,60,61,62,63,64,65,66,67,70,71,72,73,74,75] --> Loop 41 ### Ranking functions of CR log2(V1,V,Out) * RF of phase [32,34]: [V1-1] * RF of phase [33,35]: [V1-1] #### Partial ranking functions of CR log2(V1,V,Out) * Partial RF of phase [32,34]: - RF of loop [32:1]: V1-2 - RF of loop [34:1]: V1-1 * Partial RF of phase [33,35]: - RF of loop [33:1]: V1-2 - RF of loop [35:1]: V1-1 ### Specialization of cost equations start/4 * CE 6 is refined into CE [86] * CE 7 is refined into CE [87] * CE 5 is refined into CE [88] * CE 1 is refined into CE [89] * CE 2 is refined into CE [90] * CE 3 is refined into CE [91,92,93,94,95,96,97,98,99,100,101] * CE 4 is refined into CE [102,103,104,105,106,107,108,109,110,111,112] * CE 8 is refined into CE [113,114,115,116,117] * CE 9 is refined into CE [118,119] * CE 10 is refined into CE [120,121,122] * CE 11 is refined into CE [123,124,125,126,127] * CE 12 is refined into CE [128,129,130] * CE 13 is refined into CE [131,132,133,134,135] ### Cost equations --> "Loop" of start/4 * CEs [123] --> Loop 42 * CEs [114,120] --> Loop 43 * CEs [86] --> Loop 44 * CEs [87] --> Loop 45 * CEs [88,133] --> Loop 46 * CEs [89,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112] --> Loop 47 * CEs [90,113,115,116,117,118,119,121,122,124,125,126,127,128,129,130,131,132,134,135] --> Loop 48 ### Ranking functions of CR start(V1,V,V17,V21) #### Partial ranking functions of CR start(V1,V,V17,V21) Computing Bounds ===================================== #### Cost of chains of inc(V1,Out): * Chain [[19],20]: 1*it(19)+1 Such that:it(19) =< Out with precondition: [Out>=1,V1>=Out] * Chain [20]: 1 with precondition: [Out=0,V1>=0] #### Cost of chains of le(V1,V,Out): * Chain [[21],24]: 1*it(21)+1 Such that:it(21) =< V1 with precondition: [Out=2,V1>=1,V>=V1] * Chain [[21],23]: 1*it(21)+1 Such that:it(21) =< V with precondition: [Out=1,V>=1,V1>=V+1] * Chain [[21],22]: 1*it(21)+0 Such that:it(21) =< V with precondition: [Out=0,V1>=1,V>=1] * Chain [24]: 1 with precondition: [V1=0,Out=2,V>=0] * Chain [23]: 1 with precondition: [V=0,Out=1,V1>=1] * Chain [22]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of minus(V1,V,Out): * Chain [[25],27]: 1*it(25)+1 Such that:it(25) =< V with precondition: [Out=0,V1>=1,V>=1] * Chain [[25],26]: 1*it(25)+1 Such that:it(25) =< V with precondition: [V1=Out+V,V>=1,V1>=V] * Chain [27]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [26]: 1 with precondition: [V=0,V1=Out,V1>=0] #### Cost of chains of quot(V1,V,Out): * Chain [[30],31]: 2*it(30)+1 Such that:it(30) =< Out with precondition: [V=1,Out>=1,V1>=Out] * Chain [[30],29,31]: 2*it(30)+1*s(3)+3 Such that:s(3) =< 1 it(30) =< Out with precondition: [V=1,Out>=2,V1>=Out] * Chain [[28],31]: 2*it(28)+1*s(6)+1 Such that:it(28) =< V1-V+1 aux(3) =< V1 it(28) =< aux(3) s(6) =< aux(3) with precondition: [V>=2,Out>=1,V1+2>=2*Out+V] * Chain [[28],29,31]: 2*it(28)+1*s(3)+1*s(6)+3 Such that:it(28) =< V1-V+1 s(3) =< V aux(4) =< V1 it(28) =< aux(4) s(6) =< aux(4) with precondition: [V>=2,Out>=2,V1+3>=2*Out+V] * Chain [31]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [29,31]: 1*s(3)+3 Such that:s(3) =< V with precondition: [Out=1,V1>=1,V>=1] #### Cost of chains of log2(V1,V,Out): * Chain [[33,35],41]: 12*it(33)+9*it(35)+14*s(10)+3*s(60)+2*s(61)+3*s(65)+5 Such that:aux(6) =< 1 s(66) =< 2*V1 aux(18) =< V1 aux(19) =< 3*V1 s(10) =< aux(6) it(33) =< aux(18) it(35) =< aux(18) it(35) =< aux(19) s(61) =< aux(18)*2 s(65) =< s(66) s(60) =< aux(19) with precondition: [Out=0,V1>=2,V>=0] * Chain [[33,35],39]: 12*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(65)+6*s(68)+5 Such that:aux(20) =< 1 s(66) =< 2*V1 aux(22) =< V1 aux(23) =< 3*V1 s(68) =< aux(20) it(33) =< aux(22) it(35) =< aux(22) it(35) =< aux(23) s(61) =< aux(22)*2 s(65) =< s(66) s(60) =< aux(23) with precondition: [Out=0,V1>=2,V>=0] * Chain [[33,35],37,41]: 12*it(33)+9*it(35)+15*s(10)+3*s(60)+2*s(61)+3*s(65)+12 Such that:aux(24) =< 1 s(66) =< 2*V1 aux(25) =< V1 aux(26) =< 3*V1 s(10) =< aux(24) it(33) =< aux(25) it(35) =< aux(25) it(35) =< aux(26) s(61) =< aux(25)*2 s(65) =< s(66) s(60) =< aux(26) with precondition: [Out=0,V1>=3,V>=0] * Chain [[33,35],37,40]: 12*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(65)+3*s(79)+12 Such that:aux(29) =< 1 s(66) =< 2*V1 aux(30) =< V1 aux(31) =< 3*V1 s(79) =< aux(29) it(33) =< aux(30) it(35) =< aux(30) it(35) =< aux(31) s(61) =< aux(30)*2 s(65) =< s(66) s(60) =< aux(31) with precondition: [Out=1,V1>=3,V>=0] * Chain [[32,34],[33,35],41]: 18*it(32)+18*it(33)+9*it(35)+14*s(10)+3*s(60)+2*s(61)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5 Such that:aux(6) =< 1 aux(42) =< V1 aux(19) =< 6*V1+12*V aux(38) =< V aux(45) =< 2*V1+4*V aux(46) =< 3*V1 s(10) =< aux(6) it(33) =< aux(45) it(35) =< aux(45) it(35) =< aux(19) s(61) =< aux(45)*2 s(60) =< aux(19) aux(36) =< aux(42) it(32) =< aux(42) aux(36) =< aux(46) it(32) =< aux(46) aux(41) =< aux(38) s(113) =< aux(36)*2 s(111) =< it(32)*aux(38) s(110) =< aux(36) s(120) =< it(32)*aux(41) s(116) =< s(120) s(112) =< aux(46) with precondition: [Out=0,V1>=3,V>=1] * Chain [[32,34],[33,35],39]: 18*it(32)+18*it(33)+9*it(35)+3*s(60)+2*s(61)+6*s(68)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5 Such that:aux(20) =< 1 aux(42) =< V1 aux(23) =< 6*V1+12*V aux(38) =< V aux(47) =< 2*V1+4*V aux(48) =< 3*V1 s(68) =< aux(20) it(33) =< aux(47) it(35) =< aux(47) it(35) =< aux(23) s(61) =< aux(47)*2 s(60) =< aux(23) aux(36) =< aux(42) it(32) =< aux(42) aux(36) =< aux(48) it(32) =< aux(48) aux(41) =< aux(38) s(113) =< aux(36)*2 s(111) =< it(32)*aux(38) s(110) =< aux(36) s(120) =< it(32)*aux(41) s(116) =< s(120) s(112) =< aux(48) with precondition: [Out=0,V1>=3,V>=1] * Chain [[32,34],[33,35],37,41]: 18*it(32)+18*it(33)+9*it(35)+15*s(10)+3*s(60)+2*s(61)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12 Such that:aux(24) =< 1 aux(42) =< V1 aux(26) =< 6*V1+12*V aux(38) =< V aux(49) =< 2*V1+4*V aux(50) =< 3*V1 s(10) =< aux(24) it(33) =< aux(49) it(35) =< aux(49) it(35) =< aux(26) s(61) =< aux(49)*2 s(60) =< aux(26) aux(36) =< aux(42) it(32) =< aux(42) aux(36) =< aux(50) it(32) =< aux(50) aux(41) =< aux(38) s(113) =< aux(36)*2 s(111) =< it(32)*aux(38) s(110) =< aux(36) s(120) =< it(32)*aux(41) s(116) =< s(120) s(112) =< aux(50) with precondition: [Out=0,V1>=5,V>=1] * Chain [[32,34],[33,35],37,40]: 18*it(32)+18*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(79)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12 Such that:aux(29) =< 1 aux(42) =< V1 aux(31) =< 6*V1+12*V aux(38) =< V aux(51) =< 2*V1+4*V aux(52) =< 3*V1 s(79) =< aux(29) it(33) =< aux(51) it(35) =< aux(51) it(35) =< aux(31) s(61) =< aux(51)*2 s(60) =< aux(31) aux(36) =< aux(42) it(32) =< aux(42) aux(36) =< aux(52) it(32) =< aux(52) aux(41) =< aux(38) s(113) =< aux(36)*2 s(111) =< it(32)*aux(38) s(110) =< aux(36) s(120) =< it(32)*aux(41) s(116) =< s(120) s(112) =< aux(52) with precondition: [Out=1,V1>=5,V>=1] * Chain [[32,34],41]: 12*it(32)+9*it(34)+14*s(10)+12*s(12)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5 Such that:aux(6) =< 1 aux(38) =< V aux(53) =< V1 aux(54) =< 2*V1+4*V aux(55) =< 3*V1 s(10) =< aux(6) s(12) =< aux(54) it(32) =< aux(53) it(34) =< aux(53) it(34) =< aux(55) aux(41) =< aux(38) s(113) =< aux(53)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(112) =< aux(55) with precondition: [Out=0,V1>=2,V>=1] * Chain [[32,34],39]: 12*it(32)+9*it(34)+6*s(68)+6*s(70)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5 Such that:aux(20) =< 1 aux(38) =< V aux(56) =< V1 aux(57) =< 2*V1+4*V aux(58) =< 3*V1 s(68) =< aux(20) s(70) =< aux(57) it(32) =< aux(56) it(34) =< aux(56) it(34) =< aux(58) aux(41) =< aux(38) s(113) =< aux(56)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(112) =< aux(58) with precondition: [Out=0,V1>=2,V>=1] * Chain [[32,34],38]: 12*it(32)+9*it(34)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+4*s(118)+1*s(122)+6 Such that:s(122) =< 1 aux(38) =< V aux(59) =< V1 aux(60) =< 2*V1+4*V aux(61) =< 3*V1 s(118) =< aux(60) it(32) =< aux(59) it(34) =< aux(59) it(34) =< aux(61) aux(41) =< aux(38) s(113) =< aux(59)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(112) =< aux(61) with precondition: [V1>=2,Out>=0,V>=Out+1] * Chain [[32,34],37,41]: 12*it(32)+9*it(34)+15*s(10)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+3*s(118)+12 Such that:aux(24) =< 1 s(119) =< 2*V1+4*V aux(38) =< V aux(62) =< V1 aux(63) =< 3*V1 s(10) =< aux(24) it(32) =< aux(62) it(34) =< aux(62) it(34) =< aux(63) aux(41) =< aux(38) s(113) =< aux(62)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(118) =< s(119) s(112) =< aux(63) with precondition: [Out=0,V1>=3,V>=1] * Chain [[32,34],37,40]: 12*it(32)+9*it(34)+3*s(79)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+3*s(118)+12 Such that:aux(29) =< 1 s(119) =< 2*V1+4*V aux(38) =< V aux(64) =< V1 aux(65) =< 3*V1 s(79) =< aux(29) it(32) =< aux(64) it(34) =< aux(64) it(34) =< aux(65) aux(41) =< aux(38) s(113) =< aux(64)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(118) =< s(119) s(112) =< aux(65) with precondition: [Out=1,V1>=3,V>=1] * Chain [[32,34],36,41]: 12*it(32)+9*it(34)+15*s(10)+13*s(12)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12 Such that:aux(66) =< 1 aux(38) =< V aux(68) =< V1 aux(69) =< 2*V1+4*V aux(70) =< 3*V1 s(10) =< aux(66) s(12) =< aux(69) it(32) =< aux(68) it(34) =< aux(68) it(34) =< aux(70) aux(41) =< aux(38) s(113) =< aux(68)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(112) =< aux(70) with precondition: [Out=0,V1>=3,V>=1] * Chain [[32,34],36,40]: 12*it(32)+9*it(34)+6*s(80)+3*s(81)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12 Such that:aux(71) =< 1 aux(38) =< V aux(73) =< V1 aux(74) =< 2*V1+4*V aux(75) =< 3*V1 s(81) =< aux(71) s(80) =< aux(74) it(32) =< aux(73) it(34) =< aux(73) it(34) =< aux(75) aux(41) =< aux(38) s(113) =< aux(73)*2 s(111) =< it(32)*aux(38) s(120) =< it(34)*aux(41) s(116) =< s(120) s(112) =< aux(75) with precondition: [Out=1,V1>=3,V>=1] * Chain [41]: 14*s(10)+9*s(12)+5 Such that:aux(6) =< 1 aux(7) =< V s(10) =< aux(6) s(12) =< aux(7) with precondition: [Out=0,V1>=0,V>=0] * Chain [40]: 2*s(80)+2*s(81)+5 Such that:aux(27) =< 1 aux(28) =< V s(81) =< aux(27) s(80) =< aux(28) with precondition: [V1=0,Out=1,V>=0] * Chain [39]: 6*s(68)+3*s(70)+5 Such that:aux(20) =< 1 aux(21) =< V s(68) =< aux(20) s(70) =< aux(21) with precondition: [V1=1,Out=0,V>=0] * Chain [38]: 1*s(122)+1*s(123)+6 Such that:s(122) =< 1 s(123) =< V with precondition: [V1=1,Out>=0,V>=Out+1] * Chain [37,41]: 15*s(10)+12 Such that:aux(24) =< 1 s(10) =< aux(24) with precondition: [Out=0,V1>=2,V>=0] * Chain [37,40]: 3*s(79)+12 Such that:aux(29) =< 1 s(79) =< aux(29) with precondition: [Out=1,V1>=2,V>=0] * Chain [36,41]: 15*s(10)+10*s(12)+12 Such that:aux(66) =< 1 aux(67) =< V s(10) =< aux(66) s(12) =< aux(67) with precondition: [Out=0,V1>=2,V>=1] * Chain [36,40]: 3*s(80)+3*s(81)+12 Such that:aux(71) =< 1 aux(72) =< V s(81) =< aux(71) s(80) =< aux(72) with precondition: [Out=1,V1>=2,V>=1] #### Cost of chains of start(V1,V,V17,V21): * Chain [48]: 33*s(356)+256*s(358)+4*s(363)+381*s(372)+139*s(383)+333*s(385)+42*s(387)+87*s(391)+36*s(392)+8*s(393)+12*s(394)+16*s(396)+24*s(398)+119*s(439)+7*s(444)+22*s(446)+36*s(448)+8*s(449)+12*s(450)+4*s(453)+13 Such that:aux(90) =< 1 aux(91) =< V1 aux(92) =< V1-V+1 aux(93) =< 2*V1 aux(94) =< 2*V1+4*V aux(95) =< 3*V1 aux(96) =< 6*V1 aux(97) =< 6*V1+12*V aux(98) =< V s(372) =< aux(90) s(358) =< aux(91) s(363) =< aux(92) s(356) =< aux(98) s(383) =< aux(93) s(385) =< aux(91) s(385) =< aux(95) s(387) =< aux(91)*2 s(391) =< aux(95) s(392) =< aux(93) s(392) =< aux(96) s(393) =< aux(93)*2 s(394) =< aux(96) s(395) =< aux(91) s(395) =< aux(95) s(396) =< s(395)*2 s(398) =< s(395) s(439) =< aux(94) s(442) =< aux(98) s(444) =< s(358)*aux(98) s(445) =< s(385)*s(442) s(446) =< s(445) s(448) =< aux(94) s(448) =< aux(97) s(449) =< aux(94)*2 s(450) =< aux(97) s(453) =< s(385)*aux(98) s(363) =< aux(91) with precondition: [V1>=0] * Chain [47]: 1612*s(498)+98*s(499)+88*s(509)+27*s(518)+6*s(519)+9*s(520)+28*s(526)+88*s(536)+234*s(538)+28*s(540)+4*s(541)+14*s(543)+60*s(544)+27*s(545)+6*s(546)+9*s(547)+12*s(549)+3*s(550)+18*s(551)+131*s(556)+119*s(568)+132*s(569)+171*s(570)+22*s(572)+7*s(573)+22*s(575)+45*s(576)+36*s(577)+8*s(578)+12*s(579)+8*s(581)+4*s(582)+12*s(583)+119*s(649)+132*s(650)+171*s(651)+22*s(653)+7*s(654)+22*s(656)+45*s(657)+36*s(658)+8*s(659)+12*s(660)+8*s(662)+4*s(663)+12*s(664)+12*s(665)+88*s(727)+27*s(736)+6*s(737)+9*s(738)+88*s(754)+4*s(759)+14*s(761)+27*s(763)+6*s(764)+9*s(765)+3*s(768)+33*s(774)+119*s(786)+132*s(787)+171*s(788)+22*s(790)+7*s(791)+22*s(793)+45*s(794)+36*s(795)+8*s(796)+12*s(797)+8*s(799)+4*s(800)+12*s(801)+119*s(867)+132*s(868)+171*s(869)+22*s(871)+7*s(872)+22*s(874)+45*s(875)+36*s(876)+8*s(877)+12*s(878)+8*s(880)+4*s(881)+12*s(882)+12*s(883)+17 Such that:s(721) =< 4*V17 s(748) =< 4*V17+2 s(723) =< 12*V17 s(750) =< 12*V17+6 s(503) =< 4*V21 s(530) =< 4*V21+2 s(505) =< 12*V21 s(532) =< 12*V21+6 aux(119) =< 1 aux(120) =< 2 aux(121) =< 3 aux(122) =< V aux(123) =< V+1 aux(124) =< V+4*V17 aux(125) =< V+4*V17+1 aux(126) =< 3*V+12*V17 aux(127) =< 3*V+12*V17+3 aux(128) =< V/2 aux(129) =< V/2+1/2 aux(130) =< 3/2*V aux(131) =< 3/2*V+3/2 aux(132) =< V17 aux(133) =< V17+1 aux(134) =< V17+4*V21 aux(135) =< V17+4*V21+1 aux(136) =< 3*V17+12*V21 aux(137) =< 3*V17+12*V21+3 aux(138) =< V17/2 aux(139) =< V17/2+1/2 aux(140) =< 3/2*V17 aux(141) =< 3/2*V17+3/2 aux(142) =< V21 s(498) =< aux(119) s(526) =< aux(120) s(556) =< aux(132) s(499) =< aux(142) s(509) =< s(503) s(518) =< s(503) s(518) =< s(505) s(519) =< s(503)*2 s(520) =< s(505) s(568) =< aux(134) s(569) =< aux(138) s(570) =< aux(138) s(570) =< aux(140) s(539) =< aux(142) s(572) =< aux(138)*2 s(573) =< s(569)*aux(142) s(574) =< s(570)*s(539) s(575) =< s(574) s(576) =< aux(140) s(577) =< aux(134) s(577) =< aux(136) s(578) =< aux(134)*2 s(579) =< aux(136) s(580) =< aux(138) s(580) =< aux(140) s(581) =< s(580)*2 s(582) =< s(570)*aux(142) s(583) =< s(580) s(649) =< aux(135) s(650) =< aux(139) s(651) =< aux(139) s(651) =< aux(141) s(653) =< aux(139)*2 s(654) =< s(650)*aux(142) s(655) =< s(651)*s(539) s(656) =< s(655) s(657) =< aux(141) s(658) =< aux(135) s(658) =< aux(137) s(659) =< aux(135)*2 s(660) =< aux(137) s(661) =< aux(139) s(661) =< aux(141) s(662) =< s(661)*2 s(663) =< s(651)*aux(142) s(664) =< s(661) s(665) =< aux(133) s(727) =< s(721) s(736) =< s(721) s(736) =< s(723) s(737) =< s(721)*2 s(738) =< s(723) s(774) =< aux(122) s(786) =< aux(124) s(787) =< aux(128) s(788) =< aux(128) s(788) =< aux(130) s(757) =< aux(132) s(790) =< aux(128)*2 s(791) =< s(787)*aux(132) s(792) =< s(788)*s(757) s(793) =< s(792) s(794) =< aux(130) s(795) =< aux(124) s(795) =< aux(126) s(796) =< aux(124)*2 s(797) =< aux(126) s(798) =< aux(128) s(798) =< aux(130) s(799) =< s(798)*2 s(800) =< s(788)*aux(132) s(801) =< s(798) s(867) =< aux(125) s(868) =< aux(129) s(869) =< aux(129) s(869) =< aux(131) s(871) =< aux(129)*2 s(872) =< s(868)*aux(132) s(873) =< s(869)*s(757) s(874) =< s(873) s(875) =< aux(131) s(876) =< aux(125) s(876) =< aux(127) s(877) =< aux(125)*2 s(878) =< aux(127) s(879) =< aux(129) s(879) =< aux(131) s(880) =< s(879)*2 s(881) =< s(869)*aux(132) s(882) =< s(879) s(883) =< aux(123) s(536) =< s(530) s(538) =< aux(119) s(538) =< aux(121) s(540) =< aux(119)*2 s(541) =< s(498)*aux(142) s(542) =< s(538)*s(539) s(543) =< s(542) s(544) =< aux(121) s(545) =< s(530) s(545) =< s(532) s(546) =< s(530)*2 s(547) =< s(532) s(548) =< aux(119) s(548) =< aux(121) s(549) =< s(548)*2 s(550) =< s(538)*aux(142) s(551) =< s(548) s(754) =< s(748) s(759) =< s(498)*aux(132) s(760) =< s(538)*s(757) s(761) =< s(760) s(763) =< s(748) s(763) =< s(750) s(764) =< s(748)*2 s(765) =< s(750) s(768) =< s(538)*aux(132) with precondition: [V1=1,V>=0,V17>=0] * Chain [46]: 1*s(932)+1*s(933)+6 Such that:s(932) =< 1 s(933) =< V with precondition: [V1=1,V>=1] * Chain [45]: 1 with precondition: [V1=2,V>=0,V17>=0,V21>=0] * Chain [44]: 1 with precondition: [V1=2,V>=0,V17>=1] * Chain [43]: 1 with precondition: [V=0,V1>=0] * Chain [42]: 1*s(934)+4*s(936)+3 Such that:s(934) =< 1 s(935) =< V1 s(936) =< s(935) with precondition: [V=1,V1>=1] Closed-form bounds of start(V1,V,V17,V21): ------------------------------------- * Chain [48] with precondition: [V1>=0] - Upper bound: 729*V1+394+33*V1*nat(V)+nat(V)*33+382*V1+261*V1+72*V1+nat(2*V1+4*V)*171+nat(6*V1+12*V)*12+nat(V1-V+1)*4 - Complexity: n^2 * Chain [47] with precondition: [V1=1,V>=0,V17>=0] - Upper bound: 33*V+152*V17+2197+(V/2+1/2)*(33*V17)+V/2*(33*V17)+nat(V21)*119+(V17/2+1/2)*(nat(V21)*33)+V17/2*(nat(V21)*33)+508*V17+nat(4*V21)*127+108*V17+nat(12*V21)*9+135/2*V+135/2*V17+(12*V+12)+(171*V+684*V17)+(12*V17+12)+nat(V17+4*V21)*171+(36*V+144*V17)+nat(3*V17+12*V21)*12+(508*V17+254)+nat(4*V21+2)*127+(108*V17+54)+nat(12*V21+6)*9+(135/2*V+135/2)+(135/2*V17+135/2)+(171*V+684*V17+171)+nat(V17+4*V21+1)*171+(36*V+144*V17+36)+nat(3*V17+12*V21+3)*12+(375/2*V+375/2)+(375/2*V17+375/2)+375/2*V+375/2*V17 - Complexity: n^2 * Chain [46] with precondition: [V1=1,V>=1] - Upper bound: V+7 - Complexity: n * Chain [45] with precondition: [V1=2,V>=0,V17>=0,V21>=0] - Upper bound: 1 - Complexity: constant * Chain [44] with precondition: [V1=2,V>=0,V17>=1] - Upper bound: 1 - Complexity: constant * Chain [43] with precondition: [V=0,V1>=0] - Upper bound: 1 - Complexity: constant * Chain [42] with precondition: [V=1,V1>=1] - Upper bound: 4*V1+4 - Complexity: n ### Maximum cost of start(V1,V,V17,V21): max([4*V1+3,nat(V)*32+387+max([33*V1*nat(V)+729*V1+382*V1+261*V1+72*V1+nat(2*V1+4*V)*171+nat(6*V1+12*V)*12+nat(V1-V+1)*4,nat(V17)*152+1803+nat(V17)*33*nat(V/2+1/2)+nat(V17)*33*nat(V/2)+nat(V21)*119+nat(V21)*33*nat(V17/2+1/2)+nat(V21)*33*nat(V17/2)+nat(4*V17)*127+nat(4*V21)*127+nat(12*V17)*9+nat(12*V21)*9+nat(3/2*V)*45+nat(3/2*V17)*45+nat(V+1)*12+nat(V+4*V17)*171+nat(V17+1)*12+nat(V17+4*V21)*171+nat(3*V+12*V17)*12+nat(3*V17+12*V21)*12+nat(4*V17+2)*127+nat(4*V21+2)*127+nat(12*V17+6)*9+nat(12*V21+6)*9+nat(3/2*V+3/2)*45+nat(3/2*V17+3/2)*45+nat(V+4*V17+1)*171+nat(V17+4*V21+1)*171+nat(3*V+12*V17+3)*12+nat(3*V17+12*V21+3)*12+nat(V/2+1/2)*375+nat(V17/2+1/2)*375+nat(V/2)*375+nat(V17/2)*375])+(nat(V)+6)])+1 Asymptotic class: n^2 * Total analysis performed in 1998 ms. ---------------------------------------- (10) BOUNDS(1, n^2) ---------------------------------------- (11) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0) -> 0 inc(s(z0)) -> s(inc(z0)) minus(0, z0) -> 0 minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0, s(z0)) -> 0 quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0) log2(z0, z1) -> if(le(z0, 0), le(z0, s(0)), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0))), z1) Tuples: LE(0, z0) -> c LE(s(z0), 0) -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0) -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0, z0) -> c5 MINUS(z0, 0) -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0, s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0)) LOG2(z0, z1) -> c11(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, 0)) LOG2(z0, z1) -> c12(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, s(0))) LOG2(z0, z1) -> c13(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0))), z1), QUOT(z0, s(s(0)))) S tuples: LE(0, z0) -> c LE(s(z0), 0) -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0) -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0, z0) -> c5 MINUS(z0, 0) -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0, s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0)) LOG2(z0, z1) -> c11(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, 0)) LOG2(z0, z1) -> c12(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, s(0))) LOG2(z0, z1) -> c13(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0))), z1), QUOT(z0, s(s(0)))) K tuples:none Defined Rule Symbols: le_2, inc_1, minus_2, quot_2, log_1, log2_2, if_4, if2_3 Defined Pair Symbols: LE_2, INC_1, MINUS_2, QUOT_2, LOG_1, LOG2_2, IF_4, IF2_3 Compound Symbols: c, c1, c2_1, c3, c4_1, c5, c6, c7_1, c8, c9_2, c10_1, c11_2, c12_2, c13_2, c14, c15_1, c16, c17_2 ---------------------------------------- (13) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (14) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: LE(0, z0) -> c LE(s(z0), 0) -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0) -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0, z0) -> c5 MINUS(z0, 0) -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0, s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0)) LOG2(z0, z1) -> c11(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, 0)) LOG2(z0, z1) -> c12(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), LE(z0, s(0))) LOG2(z0, z1) -> c13(IF(le(z0, 0), le(z0, s(0)), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0))), z1), QUOT(z0, s(s(0)))) The (relative) TRS S consists of the following rules: le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0) -> 0 inc(s(z0)) -> s(inc(z0)) minus(0, z0) -> 0 minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0, s(z0)) -> 0 quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0) log2(z0, z1) -> if(le(z0, 0), le(z0, s(0)), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0))), z1) Rewrite Strategy: INNERMOST ---------------------------------------- (15) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (16) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) The (relative) TRS S consists of the following rules: le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Rewrite Strategy: INNERMOST ---------------------------------------- (17) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (18) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 ---------------------------------------- (19) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: LE, INC, MINUS, QUOT, minus, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: LE < LOG2 INC < LOG2 MINUS < QUOT minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (20) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: LE, INC, MINUS, QUOT, minus, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: LE < LOG2 INC < LOG2 MINUS < QUOT minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) Induction Base: LE(gen_0':s:log_undefined12_18(0), gen_0':s:log_undefined12_18(0)) ->_R^Omega(1) c Induction Step: LE(gen_0':s:log_undefined12_18(+(n17_18, 1)), gen_0':s:log_undefined12_18(+(n17_18, 1))) ->_R^Omega(1) c2(LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18))) ->_IH c2(gen_c:c1:c211_18(c18_18)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (22) Complex Obligation (BEST) ---------------------------------------- (23) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: LE, INC, MINUS, QUOT, minus, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: LE < LOG2 INC < LOG2 MINUS < QUOT minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: INC, MINUS, QUOT, minus, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: INC < LOG2 MINUS < QUOT minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) Induction Base: INC(gen_0':s:log_undefined12_18(0)) ->_R^Omega(1) c3 Induction Step: INC(gen_0':s:log_undefined12_18(+(n749_18, 1))) ->_R^Omega(1) c4(INC(gen_0':s:log_undefined12_18(n749_18))) ->_IH c4(gen_c3:c413_18(c750_18)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (28) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: MINUS, QUOT, minus, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: MINUS < QUOT minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18)) -> gen_c5:c6:c714_18(n1176_18), rt in Omega(1 + n1176_18) Induction Base: MINUS(gen_0':s:log_undefined12_18(0), gen_0':s:log_undefined12_18(0)) ->_R^Omega(1) c5 Induction Step: MINUS(gen_0':s:log_undefined12_18(+(n1176_18, 1)), gen_0':s:log_undefined12_18(+(n1176_18, 1))) ->_R^Omega(1) c7(MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18))) ->_IH c7(gen_c5:c6:c714_18(c1177_18)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18)) -> gen_c5:c6:c714_18(n1176_18), rt in Omega(1 + n1176_18) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: minus, QUOT, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: minus < QUOT QUOT < LOG2 minus < quot le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: minus(gen_0':s:log_undefined12_18(n1870_18), gen_0':s:log_undefined12_18(n1870_18)) -> gen_0':s:log_undefined12_18(0), rt in Omega(0) Induction Base: minus(gen_0':s:log_undefined12_18(0), gen_0':s:log_undefined12_18(0)) ->_R^Omega(0) 0' Induction Step: minus(gen_0':s:log_undefined12_18(+(n1870_18, 1)), gen_0':s:log_undefined12_18(+(n1870_18, 1))) ->_R^Omega(0) minus(gen_0':s:log_undefined12_18(n1870_18), gen_0':s:log_undefined12_18(n1870_18)) ->_IH gen_0':s:log_undefined12_18(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (32) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18)) -> gen_c5:c6:c714_18(n1176_18), rt in Omega(1 + n1176_18) minus(gen_0':s:log_undefined12_18(n1870_18), gen_0':s:log_undefined12_18(n1870_18)) -> gen_0':s:log_undefined12_18(0), rt in Omega(0) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: QUOT, LOG2, le, inc, quot, log2 They will be analysed ascendingly in the following order: QUOT < LOG2 le < LOG2 inc < LOG2 quot < LOG2 le < log2 inc < log2 quot < log2 ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: le(gen_0':s:log_undefined12_18(n3336_18), gen_0':s:log_undefined12_18(n3336_18)) -> true, rt in Omega(0) Induction Base: le(gen_0':s:log_undefined12_18(0), gen_0':s:log_undefined12_18(0)) ->_R^Omega(0) true Induction Step: le(gen_0':s:log_undefined12_18(+(n3336_18, 1)), gen_0':s:log_undefined12_18(+(n3336_18, 1))) ->_R^Omega(0) le(gen_0':s:log_undefined12_18(n3336_18), gen_0':s:log_undefined12_18(n3336_18)) ->_IH true We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (34) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18)) -> gen_c5:c6:c714_18(n1176_18), rt in Omega(1 + n1176_18) minus(gen_0':s:log_undefined12_18(n1870_18), gen_0':s:log_undefined12_18(n1870_18)) -> gen_0':s:log_undefined12_18(0), rt in Omega(0) le(gen_0':s:log_undefined12_18(n3336_18), gen_0':s:log_undefined12_18(n3336_18)) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: inc, LOG2, quot, log2 They will be analysed ascendingly in the following order: inc < LOG2 quot < LOG2 inc < log2 quot < log2 ---------------------------------------- (35) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: inc(gen_0':s:log_undefined12_18(n3845_18)) -> gen_0':s:log_undefined12_18(n3845_18), rt in Omega(0) Induction Base: inc(gen_0':s:log_undefined12_18(0)) ->_R^Omega(0) 0' Induction Step: inc(gen_0':s:log_undefined12_18(+(n3845_18, 1))) ->_R^Omega(0) s(inc(gen_0':s:log_undefined12_18(n3845_18))) ->_IH s(gen_0':s:log_undefined12_18(c3846_18)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (36) Obligation: Innermost TRS: Rules: LE(0', z0) -> c LE(s(z0), 0') -> c1 LE(s(z0), s(z1)) -> c2(LE(z0, z1)) INC(0') -> c3 INC(s(z0)) -> c4(INC(z0)) MINUS(0', z0) -> c5 MINUS(z0, 0') -> c6 MINUS(s(z0), s(z1)) -> c7(MINUS(z0, z1)) QUOT(0', s(z0)) -> c8 QUOT(s(z0), s(z1)) -> c9(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) LOG(z0) -> c10(LOG2(z0, 0')) LOG2(z0, z1) -> c11(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, 0')) LOG2(z0, z1) -> c12(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), LE(z0, s(0'))) LOG2(z0, z1) -> c13(IF(le(z0, 0'), le(z0, s(0')), z0, inc(z1)), INC(z1)) IF(true, z0, z1, z2) -> c14 IF(false, z0, z1, z2) -> c15(IF2(z0, z1, z2)) IF2(true, z0, s(z1)) -> c16 IF2(false, z0, z1) -> c17(LOG2(quot(z0, s(s(0'))), z1), QUOT(z0, s(s(0')))) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) inc(0') -> 0' inc(s(z0)) -> s(inc(z0)) minus(0', z0) -> 0' minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) quot(0', s(z0)) -> 0' quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1))) log(z0) -> log2(z0, 0') log2(z0, z1) -> if(le(z0, 0'), le(z0, s(0')), z0, inc(z1)) if(true, z0, z1, z2) -> log_undefined if(false, z0, z1, z2) -> if2(z0, z1, z2) if2(true, z0, s(z1)) -> z1 if2(false, z0, z1) -> log2(quot(z0, s(s(0'))), z1) Types: LE :: 0':s:log_undefined -> 0':s:log_undefined -> c:c1:c2 0' :: 0':s:log_undefined c :: c:c1:c2 s :: 0':s:log_undefined -> 0':s:log_undefined c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 INC :: 0':s:log_undefined -> c3:c4 c3 :: c3:c4 c4 :: c3:c4 -> c3:c4 MINUS :: 0':s:log_undefined -> 0':s:log_undefined -> c5:c6:c7 c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 QUOT :: 0':s:log_undefined -> 0':s:log_undefined -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c5:c6:c7 -> c8:c9 minus :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined LOG :: 0':s:log_undefined -> c10 c10 :: c11:c12:c13 -> c10 LOG2 :: 0':s:log_undefined -> 0':s:log_undefined -> c11:c12:c13 c11 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 IF :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c14:c15 le :: 0':s:log_undefined -> 0':s:log_undefined -> true:false inc :: 0':s:log_undefined -> 0':s:log_undefined c12 :: c14:c15 -> c:c1:c2 -> c11:c12:c13 c13 :: c14:c15 -> c3:c4 -> c11:c12:c13 true :: true:false c14 :: c14:c15 false :: true:false c15 :: c16:c17 -> c14:c15 IF2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> c16:c17 c16 :: c16:c17 c17 :: c11:c12:c13 -> c8:c9 -> c16:c17 quot :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log :: 0':s:log_undefined -> 0':s:log_undefined log2 :: 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined if :: true:false -> true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined log_undefined :: 0':s:log_undefined if2 :: true:false -> 0':s:log_undefined -> 0':s:log_undefined -> 0':s:log_undefined hole_c:c1:c21_18 :: c:c1:c2 hole_0':s:log_undefined2_18 :: 0':s:log_undefined hole_c3:c43_18 :: c3:c4 hole_c5:c6:c74_18 :: c5:c6:c7 hole_c8:c95_18 :: c8:c9 hole_c106_18 :: c10 hole_c11:c12:c137_18 :: c11:c12:c13 hole_c14:c158_18 :: c14:c15 hole_true:false9_18 :: true:false hole_c16:c1710_18 :: c16:c17 gen_c:c1:c211_18 :: Nat -> c:c1:c2 gen_0':s:log_undefined12_18 :: Nat -> 0':s:log_undefined gen_c3:c413_18 :: Nat -> c3:c4 gen_c5:c6:c714_18 :: Nat -> c5:c6:c7 gen_c8:c915_18 :: Nat -> c8:c9 Lemmas: LE(gen_0':s:log_undefined12_18(n17_18), gen_0':s:log_undefined12_18(n17_18)) -> gen_c:c1:c211_18(n17_18), rt in Omega(1 + n17_18) INC(gen_0':s:log_undefined12_18(n749_18)) -> gen_c3:c413_18(n749_18), rt in Omega(1 + n749_18) MINUS(gen_0':s:log_undefined12_18(n1176_18), gen_0':s:log_undefined12_18(n1176_18)) -> gen_c5:c6:c714_18(n1176_18), rt in Omega(1 + n1176_18) minus(gen_0':s:log_undefined12_18(n1870_18), gen_0':s:log_undefined12_18(n1870_18)) -> gen_0':s:log_undefined12_18(0), rt in Omega(0) le(gen_0':s:log_undefined12_18(n3336_18), gen_0':s:log_undefined12_18(n3336_18)) -> true, rt in Omega(0) inc(gen_0':s:log_undefined12_18(n3845_18)) -> gen_0':s:log_undefined12_18(n3845_18), rt in Omega(0) Generator Equations: gen_c:c1:c211_18(0) <=> c gen_c:c1:c211_18(+(x, 1)) <=> c2(gen_c:c1:c211_18(x)) gen_0':s:log_undefined12_18(0) <=> 0' gen_0':s:log_undefined12_18(+(x, 1)) <=> s(gen_0':s:log_undefined12_18(x)) gen_c3:c413_18(0) <=> c3 gen_c3:c413_18(+(x, 1)) <=> c4(gen_c3:c413_18(x)) gen_c5:c6:c714_18(0) <=> c5 gen_c5:c6:c714_18(+(x, 1)) <=> c7(gen_c5:c6:c714_18(x)) gen_c8:c915_18(0) <=> c8 gen_c8:c915_18(+(x, 1)) <=> c9(gen_c8:c915_18(x), c5) The following defined symbols remain to be analysed: quot, LOG2, log2 They will be analysed ascendingly in the following order: quot < LOG2 quot < log2