WORST_CASE(?,O(n^3)) proof of input_JddcGaEp47.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxWeightedTrs (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedTrs (13) CompletionProof [UPPER BOUND(ID), 0 ms] (14) CpxTypedWeightedCompleteTrs (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (16) CpxRNTS (17) CompleteCoflocoProof [FINISHED, 31.6 s] (18) BOUNDS(1, n^3) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3). The TRS R consists of the following rules: lessElements(l, t) -> lessE(l, t, 0) lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) if(true, b, l, t, n) -> l if(false, true, l, t, n) -> t if(false, false, l, t, n) -> lessE(l, t, s(n)) length(nil) -> 0 length(cons(n, l)) -> s(length(l)) toList(leaf) -> nil toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) append(nil, l2) -> l2 append(cons(n, l1), l2) -> cons(n, append(l1, l2)) le(s(n), 0) -> false le(0, m) -> true le(s(n), s(m)) -> le(n, m) a -> c a -> d S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: lessElements(z0, z1) -> lessE(z0, z1, 0) lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2) if(true, z0, z1, z2, z3) -> z1 if(false, true, z0, z1, z2) -> z1 if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) toList(leaf) -> nil toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) append(nil, z0) -> z0 append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) a -> c a -> d Tuples: LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0)) LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(true, z0, z1, z2, z3) -> c4 IF(false, true, z0, z1, z2) -> c5 IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(nil) -> c7 LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(leaf) -> c9 TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(nil, z0) -> c12 APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), 0) -> c14 LE(0, z0) -> c15 LE(s(z0), s(z1)) -> c16(LE(z0, z1)) A -> c17 A -> c18 S tuples: LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0)) LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(true, z0, z1, z2, z3) -> c4 IF(false, true, z0, z1, z2) -> c5 IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(nil) -> c7 LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(leaf) -> c9 TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(nil, z0) -> c12 APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), 0) -> c14 LE(0, z0) -> c15 LE(s(z0), s(z1)) -> c16(LE(z0, z1)) A -> c17 A -> c18 K tuples:none Defined Rule Symbols: lessElements_2, lessE_3, if_5, length_1, toList_1, append_2, le_2, a Defined Pair Symbols: LESSELEMENTS_2, LESSE_3, IF_5, LENGTH_1, TOLIST_1, APPEND_2, LE_2, A Compound Symbols: c1_1, c2_3, c3_4, c4, c5, c6_1, c7, c8_1, c9, c10_2, c11_2, c12, c13_1, c14, c15, c16_1, c17, c18 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: LESSELEMENTS(z0, z1) -> c1(LESSE(z0, z1, 0)) Removed 9 trailing nodes: TOLIST(leaf) -> c9 IF(false, true, z0, z1, z2) -> c5 LE(0, z0) -> c15 LE(s(z0), 0) -> c14 A -> c17 A -> c18 APPEND(nil, z0) -> c12 IF(true, z0, z1, z2, z3) -> c4 LENGTH(nil) -> c7 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: lessElements(z0, z1) -> lessE(z0, z1, 0) lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2) if(true, z0, z1, z2, z3) -> z1 if(false, true, z0, z1, z2) -> z1 if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) toList(leaf) -> nil toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) append(nil, z0) -> z0 append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) a -> c a -> d Tuples: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), s(z1)) -> c16(LE(z0, z1)) S tuples: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), s(z1)) -> c16(LE(z0, z1)) K tuples:none Defined Rule Symbols: lessElements_2, lessE_3, if_5, length_1, toList_1, append_2, le_2, a Defined Pair Symbols: LESSE_3, IF_5, LENGTH_1, TOLIST_1, APPEND_2, LE_2 Compound Symbols: c2_3, c3_4, c6_1, c8_1, c10_2, c11_2, c13_1, c16_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: lessElements(z0, z1) -> lessE(z0, z1, 0) lessE(z0, z1, z2) -> if(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2) if(true, z0, z1, z2, z3) -> z1 if(false, true, z0, z1, z2) -> z1 if(false, false, z0, z1, z2) -> lessE(z0, z1, s(z2)) a -> c a -> d ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) toList(leaf) -> nil toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) append(nil, z0) -> z0 append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) Tuples: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), s(z1)) -> c16(LE(z0, z1)) S tuples: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), s(z1)) -> c16(LE(z0, z1)) K tuples:none Defined Rule Symbols: le_2, length_1, toList_1, append_2 Defined Pair Symbols: LESSE_3, IF_5, LENGTH_1, TOLIST_1, APPEND_2, LE_2 Compound Symbols: c2_3, c3_4, c6_1, c8_1, c10_2, c11_2, c13_1, c16_1 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^3). The TRS R consists of the following rules: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) LE(s(z0), s(z1)) -> c16(LE(z0, z1)) The (relative) TRS S consists of the following rules: le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) toList(leaf) -> nil toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) append(nil, z0) -> z0 append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (9) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3). The TRS R consists of the following rules: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) [1] LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) [1] IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) [1] LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) [1] TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) [1] TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) [1] APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) [1] LE(s(z0), s(z1)) -> c16(LE(z0, z1)) [1] le(s(z0), 0) -> false [0] le(0, z0) -> true [0] le(s(z0), s(z1)) -> le(z0, z1) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] toList(leaf) -> nil [0] toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) [0] append(nil, z0) -> z0 [0] append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) [1] LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) [1] IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) [1] LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) [1] TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) [1] TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) [1] APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) [1] LE(s(z0), s(z1)) -> c16(LE(z0, z1)) [1] le(s(z0), 0) -> false [0] le(0, z0) -> true [0] le(s(z0), s(z1)) -> le(z0, z1) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] toList(leaf) -> nil [0] toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) [0] append(nil, z0) -> z0 [0] append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) [0] The TRS has the following type information: LESSE :: cons:nil -> node:leaf -> s:0 -> c2:c3 c2 :: c6 -> c16 -> c8 -> c2:c3 IF :: false:true -> false:true -> cons:nil -> node:leaf -> s:0 -> c6 le :: s:0 -> s:0 -> false:true length :: cons:nil -> s:0 toList :: node:leaf -> cons:nil LE :: s:0 -> s:0 -> c16 LENGTH :: cons:nil -> c8 c3 :: c6 -> c16 -> c8 -> c10:c11 -> c2:c3 TOLIST :: node:leaf -> c10:c11 false :: false:true c6 :: c2:c3 -> c6 s :: s:0 -> s:0 cons :: a -> cons:nil -> cons:nil c8 :: c8 -> c8 node :: node:leaf -> a -> node:leaf -> node:leaf c10 :: c13 -> c10:c11 -> c10:c11 APPEND :: cons:nil -> cons:nil -> c13 c11 :: c13 -> c10:c11 -> c10:c11 c13 :: c13 -> c13 c16 :: c16 -> c16 0 :: s:0 true :: false:true nil :: cons:nil leaf :: node:leaf append :: cons:nil -> cons:nil -> cons:nil Rewrite Strategy: INNERMOST ---------------------------------------- (13) 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] length(v0) -> null_length [0] toList(v0) -> null_toList [0] append(v0, v1) -> null_append [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] LENGTH(v0) -> null_LENGTH [0] TOLIST(v0) -> null_TOLIST [0] APPEND(v0, v1) -> null_APPEND [0] LE(v0, v1) -> null_LE [0] And the following fresh constants: null_le, null_length, null_toList, null_append, null_IF, null_LENGTH, null_TOLIST, null_APPEND, null_LE, const, const1 ---------------------------------------- (14) 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: LESSE(z0, z1, z2) -> c2(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(z0), z2), LENGTH(z0)) [1] LESSE(z0, z1, z2) -> c3(IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2), LE(length(toList(z1)), z2), LENGTH(toList(z1)), TOLIST(z1)) [1] IF(false, false, z0, z1, z2) -> c6(LESSE(z0, z1, s(z2))) [1] LENGTH(cons(z0, z1)) -> c8(LENGTH(z1)) [1] TOLIST(node(z0, z1, z2)) -> c10(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z0)) [1] TOLIST(node(z0, z1, z2)) -> c11(APPEND(toList(z0), cons(z1, toList(z2))), TOLIST(z2)) [1] APPEND(cons(z0, z1), z2) -> c13(APPEND(z1, z2)) [1] LE(s(z0), s(z1)) -> c16(LE(z0, z1)) [1] le(s(z0), 0) -> false [0] le(0, z0) -> true [0] le(s(z0), s(z1)) -> le(z0, z1) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] toList(leaf) -> nil [0] toList(node(z0, z1, z2)) -> append(toList(z0), cons(z1, toList(z2))) [0] append(nil, z0) -> z0 [0] append(cons(z0, z1), z2) -> cons(z0, append(z1, z2)) [0] le(v0, v1) -> null_le [0] length(v0) -> null_length [0] toList(v0) -> null_toList [0] append(v0, v1) -> null_append [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] LENGTH(v0) -> null_LENGTH [0] TOLIST(v0) -> null_TOLIST [0] APPEND(v0, v1) -> null_APPEND [0] LE(v0, v1) -> null_LE [0] The TRS has the following type information: LESSE :: cons:nil:null_toList:null_append -> node:leaf -> s:0:null_length -> c2:c3 c2 :: c6:null_IF -> c16:null_LE -> c8:null_LENGTH -> c2:c3 IF :: false:true:null_le -> false:true:null_le -> cons:nil:null_toList:null_append -> node:leaf -> s:0:null_length -> c6:null_IF le :: s:0:null_length -> s:0:null_length -> false:true:null_le length :: cons:nil:null_toList:null_append -> s:0:null_length toList :: node:leaf -> cons:nil:null_toList:null_append LE :: s:0:null_length -> s:0:null_length -> c16:null_LE LENGTH :: cons:nil:null_toList:null_append -> c8:null_LENGTH c3 :: c6:null_IF -> c16:null_LE -> c8:null_LENGTH -> c10:c11:null_TOLIST -> c2:c3 TOLIST :: node:leaf -> c10:c11:null_TOLIST false :: false:true:null_le c6 :: c2:c3 -> c6:null_IF s :: s:0:null_length -> s:0:null_length cons :: a -> cons:nil:null_toList:null_append -> cons:nil:null_toList:null_append c8 :: c8:null_LENGTH -> c8:null_LENGTH node :: node:leaf -> a -> node:leaf -> node:leaf c10 :: c13:null_APPEND -> c10:c11:null_TOLIST -> c10:c11:null_TOLIST APPEND :: cons:nil:null_toList:null_append -> cons:nil:null_toList:null_append -> c13:null_APPEND c11 :: c13:null_APPEND -> c10:c11:null_TOLIST -> c10:c11:null_TOLIST c13 :: c13:null_APPEND -> c13:null_APPEND c16 :: c16:null_LE -> c16:null_LE 0 :: s:0:null_length true :: false:true:null_le nil :: cons:nil:null_toList:null_append leaf :: node:leaf append :: cons:nil:null_toList:null_append -> cons:nil:null_toList:null_append -> cons:nil:null_toList:null_append null_le :: false:true:null_le null_length :: s:0:null_length null_toList :: cons:nil:null_toList:null_append null_append :: cons:nil:null_toList:null_append null_IF :: c6:null_IF null_LENGTH :: c8:null_LENGTH null_TOLIST :: c10:c11:null_TOLIST null_APPEND :: c13:null_APPEND null_LE :: c16:null_LE const :: c2:c3 const1 :: a Rewrite Strategy: INNERMOST ---------------------------------------- (15) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: false => 1 0 => 0 true => 2 nil => 0 leaf => 0 null_le => 0 null_length => 0 null_toList => 0 null_append => 0 null_IF => 0 null_LENGTH => 0 null_TOLIST => 0 null_APPEND => 0 null_LE => 0 const => 0 const1 => 0 ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: APPEND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 APPEND(z, z') -{ 1 }-> 1 + APPEND(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0 IF(z, z', z'', z3, z4) -{ 0 }-> 0 :|: z4 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0 IF(z, z', z'', z3, z4) -{ 1 }-> 1 + LESSE(z0, z1, 1 + z2) :|: z1 >= 0, z = 1, z'' = z0, z3 = z1, z0 >= 0, z' = 1, z2 >= 0, z4 = z2 LE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 LE(z, z') -{ 1 }-> 1 + LE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 LENGTH(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 LENGTH(z) -{ 1 }-> 1 + LENGTH(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 LESSE(z, z', z'') -{ 1 }-> 1 + IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2) + LE(length(z0), z2) + LENGTH(z0) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 LESSE(z, z', z'') -{ 1 }-> 1 + IF(le(length(z0), z2), le(length(toList(z1)), z2), z0, z1, z2) + LE(length(toList(z1)), z2) + LENGTH(toList(z1)) + TOLIST(z1) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 TOLIST(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 TOLIST(z) -{ 1 }-> 1 + APPEND(toList(z0), 1 + z1 + toList(z2)) + TOLIST(z0) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0 TOLIST(z) -{ 1 }-> 1 + APPEND(toList(z0), 1 + z1 + toList(z2)) + TOLIST(z2) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0 append(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0 append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 append(z, z') -{ 0 }-> 1 + z0 + append(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0 le(z, z') -{ 0 }-> le(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 le(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0 le(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0 le(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 length(z) -{ 0 }-> 0 :|: z = 0 length(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 length(z) -{ 0 }-> 1 + length(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 toList(z) -{ 0 }-> append(toList(z0), 1 + z1 + toList(z2)) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0 toList(z) -{ 0 }-> 0 :|: z = 0 toList(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (17) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V2, V13, V9),0,[fun(V1, V, V2, Out)],[V1 >= 0,V >= 0,V2 >= 0]). eq(start(V1, V, V2, V13, V9),0,[fun1(V1, V, V2, V13, V9, Out)],[V1 >= 0,V >= 0,V2 >= 0,V13 >= 0,V9 >= 0]). eq(start(V1, V, V2, V13, V9),0,[fun3(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2, V13, V9),0,[fun4(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2, V13, V9),0,[fun5(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2, V13, V9),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2, V13, V9),0,[le(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2, V13, V9),0,[length(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2, V13, V9),0,[toList(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2, V13, V9),0,[append(V1, V, Out)],[V1 >= 0,V >= 0]). eq(fun(V1, V, V2, Out),1,[length(V4, Ret00100),le(Ret00100, V5, Ret0010),toList(V3, Ret001100),length(Ret001100, Ret00110),le(Ret00110, V5, Ret0011),fun1(Ret0010, Ret0011, V4, V3, V5, Ret001),length(V4, Ret010),fun2(Ret010, V5, Ret01),fun3(V4, Ret1)],[Out = 1 + Ret001 + Ret01 + Ret1,V2 = V5,V1 = V4,V3 >= 0,V = V3,V4 >= 0,V5 >= 0]). eq(fun(V1, V, V2, Out),1,[length(V8, Ret000100),le(Ret000100, V6, Ret00010),toList(V7, Ret0001100),length(Ret0001100, Ret000110),le(Ret000110, V6, Ret00011),fun1(Ret00010, Ret00011, V8, V7, V6, Ret0001),toList(V7, Ret001001),length(Ret001001, Ret00101),fun2(Ret00101, V6, Ret0012),toList(V7, Ret0101),fun3(Ret0101, Ret011),fun4(V7, Ret11)],[Out = 1 + Ret0001 + Ret0012 + Ret011 + Ret11,V2 = V6,V1 = V8,V7 >= 0,V = V7,V8 >= 0,V6 >= 0]). eq(fun1(V1, V, V2, V13, V9, Out),1,[fun(V12, V11, 1 + V10, Ret12)],[Out = 1 + Ret12,V11 >= 0,V1 = 1,V2 = V12,V13 = V11,V12 >= 0,V = 1,V10 >= 0,V9 = V10]). eq(fun3(V1, Out),1,[fun3(V15, Ret13)],[Out = 1 + Ret13,V15 >= 0,V14 >= 0,V1 = 1 + V14 + V15]). eq(fun4(V1, Out),1,[toList(V17, Ret0102),toList(V18, Ret0111),fun5(Ret0102, 1 + V16 + Ret0111, Ret012),fun4(V17, Ret14)],[Out = 1 + Ret012 + Ret14,V16 >= 0,V1 = 1 + V16 + V17 + V18,V17 >= 0,V18 >= 0]). eq(fun4(V1, Out),1,[toList(V20, Ret0103),toList(V21, Ret01111),fun5(Ret0103, 1 + V19 + Ret01111, Ret013),fun4(V21, Ret15)],[Out = 1 + Ret013 + Ret15,V19 >= 0,V1 = 1 + V19 + V20 + V21,V20 >= 0,V21 >= 0]). eq(fun5(V1, V, Out),1,[fun5(V23, V22, Ret16)],[Out = 1 + Ret16,V23 >= 0,V = V22,V24 >= 0,V1 = 1 + V23 + V24,V22 >= 0]). eq(fun2(V1, V, Out),1,[fun2(V26, V25, Ret17)],[Out = 1 + Ret17,V25 >= 0,V1 = 1 + V26,V26 >= 0,V = 1 + V25]). eq(le(V1, V, Out),0,[],[Out = 1,V1 = 1 + V27,V27 >= 0,V = 0]). eq(le(V1, V, Out),0,[],[Out = 2,V28 >= 0,V1 = 0,V = V28]). eq(le(V1, V, Out),0,[le(V29, V30, Ret)],[Out = Ret,V30 >= 0,V1 = 1 + V29,V29 >= 0,V = 1 + V30]). eq(length(V1, Out),0,[],[Out = 0,V1 = 0]). eq(length(V1, Out),0,[length(V31, Ret18)],[Out = 1 + Ret18,V31 >= 0,V32 >= 0,V1 = 1 + V31 + V32]). eq(toList(V1, Out),0,[],[Out = 0,V1 = 0]). eq(toList(V1, Out),0,[toList(V34, Ret0),toList(V33, Ret111),append(Ret0, 1 + V35 + Ret111, Ret2)],[Out = Ret2,V35 >= 0,V1 = 1 + V33 + V34 + V35,V34 >= 0,V33 >= 0]). eq(append(V1, V, Out),0,[],[Out = V36,V36 >= 0,V1 = 0,V = V36]). eq(append(V1, V, Out),0,[append(V38, V37, Ret19)],[Out = 1 + Ret19 + V39,V38 >= 0,V = V37,V39 >= 0,V1 = 1 + V38 + V39,V37 >= 0]). eq(le(V1, V, Out),0,[],[Out = 0,V41 >= 0,V40 >= 0,V1 = V41,V = V40]). eq(length(V1, Out),0,[],[Out = 0,V42 >= 0,V1 = V42]). eq(toList(V1, Out),0,[],[Out = 0,V43 >= 0,V1 = V43]). eq(append(V1, V, Out),0,[],[Out = 0,V44 >= 0,V45 >= 0,V1 = V44,V = V45]). eq(fun1(V1, V, V2, V13, V9, Out),0,[],[Out = 0,V9 = V48,V46 >= 0,V48 >= 0,V2 = V50,V47 >= 0,V1 = V46,V = V47,V13 = V49,V50 >= 0,V49 >= 0]). eq(fun3(V1, Out),0,[],[Out = 0,V51 >= 0,V1 = V51]). eq(fun4(V1, Out),0,[],[Out = 0,V52 >= 0,V1 = V52]). eq(fun5(V1, V, Out),0,[],[Out = 0,V53 >= 0,V54 >= 0,V1 = V53,V = V54]). eq(fun2(V1, V, Out),0,[],[Out = 0,V55 >= 0,V56 >= 0,V1 = V55,V = V56]). input_output_vars(fun(V1,V,V2,Out),[V1,V,V2],[Out]). input_output_vars(fun1(V1,V,V2,V13,V9,Out),[V1,V,V2,V13,V9],[Out]). input_output_vars(fun3(V1,Out),[V1],[Out]). input_output_vars(fun4(V1,Out),[V1],[Out]). input_output_vars(fun5(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,V,Out),[V1,V],[Out]). input_output_vars(le(V1,V,Out),[V1,V],[Out]). input_output_vars(length(V1,Out),[V1],[Out]). input_output_vars(toList(V1,Out),[V1],[Out]). input_output_vars(append(V1,V,Out),[V1,V],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [append/3] 1. recursive : [fun2/3] 2. recursive : [fun3/2] 3. recursive : [fun5/3] 4. recursive [non_tail,multiple] : [toList/2] 5. recursive : [fun4/2] 6. recursive : [le/3] 7. recursive : [length/2] 8. recursive [non_tail] : [fun/4,fun1/6] 9. non_recursive : [start/5] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into append/3 1. SCC is partially evaluated into fun2/3 2. SCC is partially evaluated into fun3/2 3. SCC is partially evaluated into fun5/3 4. SCC is partially evaluated into toList/2 5. SCC is partially evaluated into fun4/2 6. SCC is partially evaluated into le/3 7. SCC is partially evaluated into length/2 8. SCC is partially evaluated into fun/4 9. SCC is partially evaluated into start/5 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations append/3 * CE 35 is refined into CE [36] * CE 33 is refined into CE [37] * CE 34 is refined into CE [38] ### Cost equations --> "Loop" of append/3 * CEs [38] --> Loop 23 * CEs [36] --> Loop 24 * CEs [37] --> Loop 25 ### Ranking functions of CR append(V1,V,Out) * RF of phase [23]: [V1] #### Partial ranking functions of CR append(V1,V,Out) * Partial RF of phase [23]: - RF of loop [23:1]: V1 ### Specialization of cost equations fun2/3 * CE 24 is refined into CE [39] * CE 23 is refined into CE [40] ### Cost equations --> "Loop" of fun2/3 * CEs [40] --> Loop 26 * CEs [39] --> Loop 27 ### Ranking functions of CR fun2(V1,V,Out) * RF of phase [26]: [V,V1] #### Partial ranking functions of CR fun2(V1,V,Out) * Partial RF of phase [26]: - RF of loop [26:1]: V V1 ### Specialization of cost equations fun3/2 * CE 17 is refined into CE [41] * CE 16 is refined into CE [42] ### Cost equations --> "Loop" of fun3/2 * CEs [42] --> Loop 28 * CEs [41] --> Loop 29 ### Ranking functions of CR fun3(V1,Out) * RF of phase [28]: [V1] #### Partial ranking functions of CR fun3(V1,Out) * Partial RF of phase [28]: - RF of loop [28:1]: V1 ### Specialization of cost equations fun5/3 * CE 22 is refined into CE [43] * CE 21 is refined into CE [44] ### Cost equations --> "Loop" of fun5/3 * CEs [44] --> Loop 30 * CEs [43] --> Loop 31 ### Ranking functions of CR fun5(V1,V,Out) * RF of phase [30]: [V1] #### Partial ranking functions of CR fun5(V1,V,Out) * Partial RF of phase [30]: - RF of loop [30:1]: V1 ### Specialization of cost equations toList/2 * CE 31 is refined into CE [45] * CE 32 is refined into CE [46,47,48,49] ### Cost equations --> "Loop" of toList/2 * CEs [49] --> Loop 32 * CEs [48] --> Loop 33 * CEs [46] --> Loop 34 * CEs [47] --> Loop 35 * CEs [45] --> Loop 36 ### Ranking functions of CR toList(V1,Out) * RF of phase [32,33,34,35]: [V1] #### Partial ranking functions of CR toList(V1,Out) * Partial RF of phase [32,33,34,35]: - RF of loop [32:1,32:2,33:1,33:2,34:1,34:2,35:1,35:2]: V1 ### Specialization of cost equations fun4/2 * CE 20 is refined into CE [50] * CE 18 is refined into CE [51,52,53,54,55,56] * CE 19 is refined into CE [57,58,59,60,61,62] ### Cost equations --> "Loop" of fun4/2 * CEs [54,56] --> Loop 37 * CEs [60,62] --> Loop 38 * CEs [51,52,53,55,57,58,59,61] --> Loop 39 * CEs [50] --> Loop 40 ### Ranking functions of CR fun4(V1,Out) * RF of phase [37,38,39]: [V1] #### Partial ranking functions of CR fun4(V1,Out) * Partial RF of phase [37,38,39]: - RF of loop [37:1,38:1]: V1-1 - RF of loop [39:1]: V1 ### Specialization of cost equations le/3 * CE 28 is refined into CE [63] * CE 25 is refined into CE [64] * CE 26 is refined into CE [65] * CE 27 is refined into CE [66] ### Cost equations --> "Loop" of le/3 * CEs [66] --> Loop 41 * CEs [63] --> Loop 42 * CEs [64] --> Loop 43 * CEs [65] --> Loop 44 ### Ranking functions of CR le(V1,V,Out) * RF of phase [41]: [V,V1] #### Partial ranking functions of CR le(V1,V,Out) * Partial RF of phase [41]: - RF of loop [41:1]: V V1 ### Specialization of cost equations length/2 * CE 29 is refined into CE [67] * CE 30 is refined into CE [68] ### Cost equations --> "Loop" of length/2 * CEs [68] --> Loop 45 * CEs [67] --> Loop 46 ### Ranking functions of CR length(V1,Out) * RF of phase [45]: [V1] #### Partial ranking functions of CR length(V1,Out) * Partial RF of phase [45]: - RF of loop [45:1]: V1 ### Specialization of cost equations fun/4 * CE 14 is refined into CE [69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110] * CE 15 is refined into CE [111,112,113,114,115,116,117,118,119,120] * CE 12 is refined into CE [121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666,667,668,669,670,671,672,673,674,675,676,677,678,679,680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700,701,702,703,704,705,706,707,708,709,710,711,712,713,714,715,716,717,718,719,720,721,722,723,724,725,726,727,728,729,730,731,732,733,734,735,736,737,738,739,740,741,742,743,744,745,746,747,748,749,750,751,752,753,754,755,756,757,758,759,760,761,762,763,764,765,766,767,768,769,770,771,772,773,774,775,776,777,778,779,780,781,782,783,784,785,786,787,788,789,790,791,792,793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849,850,851,852,853,854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880,881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936,937,938,939,940,941,942,943,944,945,946,947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968,969,970,971,972,973,974,975,976,977,978,979,980,981,982,983,984,985,986,987,988,989,990,991,992,993,994,995,996,997,998,999,1000,1001,1002,1003,1004,1005,1006,1007,1008,1009,1010,1011,1012,1013,1014,1015,1016,1017,1018,1019,1020,1021,1022,1023,1024,1025,1026,1027,1028,1029,1030,1031,1032,1033,1034,1035,1036,1037,1038,1039,1040,1041,1042,1043,1044,1045,1046,1047,1048,1049,1050,1051,1052,1053,1054,1055,1056,1057,1058,1059,1060,1061,1062,1063,1064,1065,1066,1067,1068,1069,1070,1071,1072,1073,1074,1075,1076,1077,1078,1079,1080,1081,1082,1083,1084,1085,1086,1087,1088,1089,1090,1091,1092,1093,1094,1095,1096,1097,1098,1099,1100,1101,1102,1103,1104,1105,1106,1107,1108,1109,1110,1111,1112,1113,1114,1115,1116,1117,1118,1119,1120,1121,1122] * CE 13 is refined into CE [1123,1124,1125,1126,1127,1128,1129,1130,1131,1132,1133,1134,1135,1136,1137,1138,1139,1140,1141,1142,1143,1144,1145,1146,1147,1148,1149,1150,1151,1152,1153,1154,1155,1156,1157,1158,1159,1160,1161,1162,1163,1164,1165,1166,1167,1168,1169,1170,1171,1172,1173,1174,1175,1176,1177,1178,1179,1180,1181,1182,1183,1184,1185,1186,1187,1188,1189,1190,1191,1192,1193,1194,1195,1196,1197,1198,1199,1200,1201,1202,1203,1204,1205,1206,1207,1208,1209,1210,1211,1212,1213,1214,1215,1216,1217,1218,1219,1220,1221,1222,1223,1224,1225,1226,1227,1228,1229,1230,1231,1232,1233,1234,1235,1236,1237,1238,1239,1240,1241,1242,1243,1244,1245,1246,1247,1248,1249,1250,1251,1252,1253,1254,1255,1256,1257,1258,1259,1260,1261,1262,1263,1264,1265,1266,1267,1268,1269,1270,1271,1272,1273,1274,1275,1276,1277,1278,1279,1280,1281,1282,1283,1284,1285,1286,1287,1288,1289,1290,1291,1292,1293,1294,1295,1296,1297,1298,1299,1300,1301,1302,1303,1304,1305,1306,1307,1308,1309,1310,1311,1312,1313,1314,1315,1316,1317,1318,1319,1320,1321,1322,1323,1324,1325,1326,1327,1328,1329,1330,1331,1332,1333,1334,1335,1336,1337,1338,1339,1340,1341,1342,1343,1344,1345,1346,1347,1348,1349,1350,1351,1352,1353,1354,1355,1356,1357,1358,1359,1360,1361,1362,1363,1364,1365,1366,1367,1368] ### Cost equations --> "Loop" of fun/4 * CEs [1128,1134,1174,1180,1244,1250,1290,1296,1332,1338] --> Loop 47 * CEs [1124,1126,1127,1130,1132,1133,1170,1172,1173,1176,1178,1179,1216,1218,1220,1222,1240,1242,1243,1246,1248,1249,1286,1288,1289,1292,1294,1295,1328,1330,1331,1334,1336,1337] --> Loop 48 * CEs [122,124,125,126,128,130,131,132,134,136,137,138,139,140,141,142,143,144,146,148,149,150,152,154,155,156,158,160,161,162,163,164,165,166,167,168,170,172,173,174,176,178,179,180,182,184,185,186,187,188,189,190,191,192,194,196,197,198,200,202,203,204,206,208,209,210,211,212,213,214,215,216,218,220,221,222,224,226,227,228,230,232,233,234,236,238,239,240,242,244,245,246,248,250,251,252,253,254,255,256,257,258,260,262,263,264,266,268,269,270,272,274,275,276,277,278,279,280,281,282,284,286,287,288,290,292,293,294,296,298,299,300,301,302,303,304,305,306,308,310,311,312,314,316,317,318,320,322,323,324,325,326,327,328,329,330,332,334,335,336,338,340,341,342,344,346,347,348,349,350,351,352,353,354,356,358,359,360,362,364,365,366,368,370,371,372,373,374,375,376,377,378,380,382,383,384,386,388,389,390,392,394,395,396,397,398,399,400,401,402,404,406,407,408,410,412,413,414,416,418,419,420,422,424,425,426,428,430,431,432,434,436,437,438,439,440,441,442,443,444,446,448,449,450,452,454,455,456,458,460,461,462,463,464,465,466,467,468,470,472,473,474,476,478,479,480,482,484,485,486,487,488,489,490,491,492,494,496,497,498,500,502,503,504,506,508,509,510,512,514,515,516,518,520,521,522,524,526,527,528,530,532,533,534,536,538,539,540,542,544,545,546,548,550,551,552,554,556,557,558,560,562,563,564,566,568,569,570,572,574,575,576,578,580,581,582,584,586,587,588,590,592,593,594,596,598,599,600,602,604,605,606,608,610,611,612,614,616,617,618,619,620,621,622,623,624,626,628,629,630,632,634,635,636,638,640,641,642,643,644,645,646,647,648,650,652,653,654,656,658,659,660,662,664,665,666,667,668,669,670,671,672,674,676,677,678,680,682,683,684,686,688,689,690,691,692,693,694,695,696,698,700,701,702,704,706,707,708,710,712,713,714,716,718,719,720,722,724,725,726,728,730,731,732,733,734,735,736,737,738,740,742,743,744,746,748,749,750,752,754,755,756,757,758,759,760,761,762,764,766,767,768,770,772,773,774,776,778,779,780,781,782,783,784,785,786,788,790,791,792,794,796,797,798,800,802,803,804,805,806,807,808,809,810,812,814,815,816,818,820,821,822,824,826,827,828,829,830,831,832,833,834,836,838,839,840,842,844,845,846,848,850,851,852,853,854,855,856,857,858,860,862,863,864,866,868,869,870,872,874,875,876,877,878,879,880,881,882,884,886,887,888,890,892,893,894,896,898,899,900,901,902,903,904,905,906,908,910,911,912,914,916,917,918,920,922,923,924,925,926,927,928,929,930,932,934,935,936,938,940,941,942,944,946,947,948,949,950,951,952,953,954,956,958,959,960,962,964,965,966,968,970,971,972,973,974,975,976,977,978,980,982,983,984,986,988,989,990,992,994,995,996,997,998,999,1000,1001,1002,1004,1006,1007,1008,1010,1012,1013,1014,1016,1018,1019,1020,1021,1022,1023,1024,1025,1026,1028,1030,1031,1032,1034,1036,1037,1038,1040,1042,1043,1044,1045,1046,1047,1048,1049,1050,1052,1054,1055,1056,1058,1060,1061,1062,1064,1066,1067,1068,1069,1070,1071,1072,1073,1074,1076,1078,1079,1080,1082,1084,1085,1086,1088,1090,1091,1092,1093,1094,1095,1096,1097,1098,1100,1102,1103,1104,1106,1108,1109,1110,1112,1114,1115,1116,1117,1118,1119,1120,1121,1122,1136,1138,1139,1140,1142,1144,1145,1146,1148,1150,1152,1154,1155,1156,1158,1160,1161,1162,1164,1166,1167,1168,1182,1184,1185,1186,1188,1190,1191,1192,1194,1196,1198,1200,1201,1202,1204,1206,1207,1208,1210,1212,1213,1214,1224,1226,1228,1230,1232,1234,1236,1238,1252,1254,1255,1256,1258,1260,1261,1262,1264,1266,1268,1270,1271,1272,1274,1276,1277,1278,1280,1282,1283,1284,1298,1300,1301,1302,1304,1306,1307,1308,1310,1312,1313,1314,1316,1318,1319,1320,1322,1324,1325,1326,1340,1342,1343,1344,1346,1348,1349,1350,1352,1354,1355,1356,1358,1360,1361,1362,1364,1366,1367,1368] --> Loop 49 * CEs [493,511,1215,1217,1219,1221] --> Loop 50 * CEs [121,123,127,129,133,135,145,147,151,153,157,159,169,171,175,177,181,183,193,195,199,201,205,207,217,219,223,225,229,231,235,237,241,243,247,249,259,261,265,267,271,273,283,285,289,291,295,297,307,309,313,315,319,321,331,333,337,339,343,345,355,357,361,363,367,369,379,381,385,387,391,393,403,405,409,411,415,417,421,423,427,429,433,435,445,447,451,453,457,459,469,471,475,477,481,483,495,499,501,505,507,513,517,519,523,525,529,531,535,537,541,543,547,549,553,555,559,561,565,567,571,573,577,579,583,585,589,591,595,597,601,603,607,609,613,615,625,627,631,633,637,639,649,651,655,657,661,663,673,675,679,681,685,687,697,699,703,705,709,711,715,717,721,723,727,729,739,741,745,747,751,753,763,765,769,771,775,777,787,789,793,795,799,801,811,813,817,819,823,825,835,837,841,843,847,849,859,861,865,867,871,873,883,885,889,891,895,897,907,909,913,915,919,921,931,933,937,939,943,945,955,957,961,963,967,969,979,981,985,987,991,993,1003,1005,1009,1011,1015,1017,1027,1029,1033,1035,1039,1041,1051,1053,1057,1059,1063,1065,1075,1077,1081,1083,1087,1089,1099,1101,1105,1107,1111,1113,1123,1125,1129,1131,1135,1137,1141,1143,1147,1149,1151,1153,1157,1159,1163,1165,1169,1171,1175,1177,1181,1183,1187,1189,1193,1195,1197,1199,1203,1205,1209,1211,1223,1225,1227,1229,1231,1233,1235,1237,1239,1241,1245,1247,1251,1253,1257,1259,1263,1265,1267,1269,1273,1275,1279,1281,1285,1287,1291,1293,1297,1299,1303,1305,1309,1311,1315,1317,1321,1323,1327,1329,1333,1335,1339,1341,1345,1347,1351,1353,1357,1359,1363,1365] --> Loop 51 * CEs [87,89,93,95,99,101,115,117] --> Loop 52 * CEs [88,90,91,92,94,96,97,98,100,102,103,104,105,106,107,108,109,110,116,118,119,120] --> Loop 53 * CEs [70,72,73,74,76,78,79,80,82,84,85,86,112,114] --> Loop 54 * CEs [69,71,75,77,81,83,111,113] --> Loop 55 ### Ranking functions of CR fun(V1,V,V2,Out) * RF of phase [52,53]: [V-V2,V1-V2] #### Partial ranking functions of CR fun(V1,V,V2,Out) * Partial RF of phase [52,53]: - RF of loop [52:1,53:1]: V-V2 V1-V2 ### Specialization of cost equations start/5 * CE 1 is refined into CE [1369] * CE 2 is refined into CE [1370,1371,1372,1373] * CE 3 is refined into CE [1374,1375,1376,1377,1378] * CE 4 is refined into CE [1379,1380] * CE 5 is refined into CE [1381,1382] * CE 6 is refined into CE [1383,1384] * CE 7 is refined into CE [1385,1386] * CE 8 is refined into CE [1387,1388,1389,1390,1391] * CE 9 is refined into CE [1392,1393] * CE 10 is refined into CE [1394,1395] * CE 11 is refined into CE [1396,1397,1398,1399] ### Cost equations --> "Loop" of start/5 * CEs [1376] --> Loop 56 * CEs [1388] --> Loop 57 * CEs [1370,1371,1372,1373] --> Loop 58 * CEs [1369,1374,1375,1377,1378,1379,1380,1381,1382,1383,1384,1385,1386,1387,1389,1390,1391,1392,1393,1394,1395,1396,1397,1398,1399] --> Loop 59 ### Ranking functions of CR start(V1,V,V2,V13,V9) #### Partial ranking functions of CR start(V1,V,V2,V13,V9) Computing Bounds ===================================== #### Cost of chains of append(V1,V,Out): * Chain [[23],25]: 0 with precondition: [V+V1=Out,V1>=1,V>=0] * Chain [[23],24]: 0 with precondition: [V>=0,Out>=1,V1>=Out] * Chain [25]: 0 with precondition: [V1=0,V=Out,V>=0] * Chain [24]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun2(V1,V,Out): * Chain [[26],27]: 1*it(26)+0 Such that:it(26) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [27]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun3(V1,Out): * Chain [[28],29]: 1*it(28)+0 Such that:it(28) =< V1 with precondition: [Out>=1,V1>=Out] * Chain [29]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of fun5(V1,V,Out): * Chain [[30],31]: 1*it(30)+0 Such that:it(30) =< V1 with precondition: [V>=0,Out>=1,V1>=Out] * Chain [31]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of toList(V1,Out): * Chain [36]: 0 with precondition: [Out=0,V1>=0] * Chain [multiple([32,33,34,35],[[36]])]: 0 with precondition: [V1>=1,Out>=0,V1>=Out] #### Cost of chains of fun4(V1,Out): * Chain [[37,38,39],40]: 5*it(37)+2*s(9)+0 Such that:aux(10) =< V1 it(37) =< aux(10) s(10) =< it(37)*aux(10) s(9) =< s(10) with precondition: [V1>=1,Out>=1] * Chain [40]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of le(V1,V,Out): * Chain [[41],44]: 0 with precondition: [Out=2,V1>=1,V>=V1] * Chain [[41],43]: 0 with precondition: [Out=1,V>=1,V1>=V+1] * Chain [[41],42]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [44]: 0 with precondition: [V1=0,Out=2,V>=0] * Chain [43]: 0 with precondition: [V=0,Out=1,V1>=1] * Chain [42]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of length(V1,Out): * Chain [[45],46]: 0 with precondition: [Out>=1,V1>=Out] * Chain [46]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of fun(V1,V,V2,Out): * Chain [[52,53],51]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+1 Such that:aux(24) =< V1 s(83) =< V aux(27) =< V-V2 aux(29) =< V1-V2 it(52) =< aux(29) it(52) =< aux(27) aux(20) =< s(83) aux(21) =< aux(24) s(98) =< it(52)*aux(24) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*s(83) s(92) =< s(97) with precondition: [V2>=1,Out>=3,V1>=V2+1,V>=V2+1] * Chain [[52,53],49]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+2959*s(103)+1002*s(105)+229*s(144)+1 Such that:aux(27) =< V-V2 aux(294) =< V1 aux(295) =< V1-V2 aux(296) =< V s(144) =< aux(294) s(103) =< aux(296) s(104) =< s(103)*aux(296) s(105) =< s(104) it(52) =< aux(295) it(52) =< aux(27) aux(20) =< aux(296) aux(21) =< aux(294) s(98) =< it(52)*aux(294) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(296) s(92) =< s(97) with precondition: [V2>=1,Out>=4,V1>=V2+1,V>=V2+1] * Chain [[52,53],48]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+24*s(2789)+10*s(2791)+1 Such that:aux(25) =< V1-V2 aux(299) =< V1 aux(300) =< V aux(301) =< V-V2 s(2789) =< aux(299) s(2791) =< aux(300) it(52) =< aux(25) it(52) =< aux(301) aux(20) =< aux(300) aux(21) =< aux(299) s(98) =< it(52)*aux(299) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(300) s(92) =< s(97) with precondition: [V2>=1,Out>=4,V1>=V2+1,V>=V2+1] * Chain [[52,53],47]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+18*s(2823)+2*s(2835)+1 Such that:aux(25) =< V1-V2 aux(312) =< V1 aux(313) =< V aux(314) =< V-V2 s(2823) =< aux(312) s(2835) =< aux(313) it(52) =< aux(25) it(52) =< aux(314) aux(20) =< aux(313) aux(21) =< aux(312) s(98) =< it(52)*aux(312) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(313) s(92) =< s(97) with precondition: [V2>=1,Out>=5,V1>=V2+1,V>=V2+1] * Chain [55,[52,53],51]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+3 Such that:aux(315) =< V1 aux(316) =< V it(52) =< aux(315) it(52) =< aux(316) aux(20) =< aux(316) aux(21) =< aux(315) s(98) =< it(52)*aux(315) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(316) s(92) =< s(97) with precondition: [V2=0,V1>=2,V>=2,Out>=5] * Chain [55,[52,53],49]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+2959*s(103)+1002*s(105)+229*s(144)+3 Such that:aux(317) =< V1 aux(318) =< V s(144) =< aux(317) s(103) =< aux(318) s(104) =< s(103)*aux(318) s(105) =< s(104) it(52) =< aux(317) it(52) =< aux(318) aux(20) =< aux(318) aux(21) =< aux(317) s(98) =< it(52)*aux(317) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(318) s(92) =< s(97) with precondition: [V2=0,V1>=2,V>=2,Out>=6] * Chain [55,[52,53],48]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+24*s(2789)+10*s(2791)+3 Such that:aux(319) =< V1 aux(320) =< V s(2789) =< aux(319) s(2791) =< aux(320) it(52) =< aux(319) it(52) =< aux(320) aux(20) =< aux(320) aux(21) =< aux(319) s(98) =< it(52)*aux(319) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(320) s(92) =< s(97) with precondition: [V2=0,V1>=2,V>=2,Out>=6] * Chain [55,[52,53],47]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+18*s(2823)+2*s(2835)+3 Such that:aux(321) =< V1 aux(322) =< V s(2823) =< aux(321) s(2835) =< aux(322) it(52) =< aux(321) it(52) =< aux(322) aux(20) =< aux(322) aux(21) =< aux(321) s(98) =< it(52)*aux(321) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(322) s(92) =< s(97) with precondition: [V2=0,V1>=2,V>=2,Out>=7] * Chain [55,51]: 3 with precondition: [V2=0,Out=3,V1>=1,V>=1] * Chain [55,49]: 2959*s(103)+1002*s(105)+120*s(144)+109*s(2650)+3 Such that:aux(293) =< 1 aux(291) =< V1 aux(292) =< V s(2650) =< aux(291) s(103) =< aux(292) s(144) =< aux(293) s(104) =< s(103)*aux(292) s(105) =< s(104) with precondition: [V2=0,V1>=1,V>=1,Out>=4] * Chain [55,48]: 24*s(2789)+10*s(2791)+3 Such that:aux(298) =< 1 aux(297) =< V1 s(2789) =< aux(297) s(2791) =< aux(298) with precondition: [V2=0,V>=1,Out>=4,V1+3>=Out] * Chain [55,47]: 18*s(2823)+2*s(2835)+3 Such that:aux(311) =< 1 aux(310) =< V1 s(2823) =< aux(310) s(2835) =< aux(311) with precondition: [V2=0,V>=1,Out>=5,V1+4>=Out] * Chain [54,[52,53],51]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+51*s(2844)+18*s(2846)+2*s(2885)+3 Such that:aux(329) =< V1 aux(330) =< V it(52) =< aux(329) it(52) =< aux(330) aux(20) =< aux(330) aux(21) =< aux(329) s(98) =< it(52)*aux(329) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(330) s(92) =< s(97) s(2885) =< aux(329) s(2844) =< aux(330) s(2845) =< s(2844)*aux(330) s(2846) =< s(2845) with precondition: [V2=0,V1>=2,V>=2,Out>=6] * Chain [54,[52,53],49]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+3010*s(103)+1020*s(105)+231*s(144)+3 Such that:aux(331) =< V1 aux(332) =< V s(144) =< aux(331) s(103) =< aux(332) s(104) =< s(103)*aux(332) s(105) =< s(104) it(52) =< aux(331) it(52) =< aux(332) aux(20) =< aux(332) aux(21) =< aux(331) s(98) =< it(52)*aux(331) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(332) s(92) =< s(97) with precondition: [V2=0,V1>=2,V>=2,Out>=7] * Chain [54,[52,53],48]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+26*s(2789)+61*s(2791)+18*s(2846)+3 Such that:aux(333) =< V1 aux(334) =< V s(2789) =< aux(333) s(2791) =< aux(334) it(52) =< aux(333) it(52) =< aux(334) aux(20) =< aux(334) aux(21) =< aux(333) s(98) =< it(52)*aux(333) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(334) s(92) =< s(97) s(2845) =< s(2791)*aux(334) s(2846) =< s(2845) with precondition: [V2=0,V1>=2,V>=2,Out>=7] * Chain [54,[52,53],47]: 4*it(52)+68*s(91)+24*s(92)+10*s(94)+1*s(96)+20*s(2823)+53*s(2835)+18*s(2846)+3 Such that:aux(335) =< V1 aux(336) =< V s(2823) =< aux(335) s(2835) =< aux(336) it(52) =< aux(335) it(52) =< aux(336) aux(20) =< aux(336) aux(21) =< aux(335) s(98) =< it(52)*aux(335) s(99) =< it(52)*aux(20) s(96) =< it(52)*aux(21) s(94) =< s(98) s(91) =< s(99) s(97) =< s(91)*aux(336) s(92) =< s(97) s(2845) =< s(2835)*aux(336) s(2846) =< s(2845) with precondition: [V2=0,V1>=2,V>=2,Out>=8] * Chain [54,51]: 51*s(2844)+18*s(2846)+2*s(2885)+3 Such that:aux(326) =< V1 aux(337) =< V s(2885) =< aux(326) s(2844) =< aux(337) s(2845) =< s(2844)*aux(337) s(2846) =< s(2845) with precondition: [V2=0,V1>=1,V>=1,Out>=4] * Chain [54,49]: 3010*s(103)+1020*s(105)+120*s(144)+111*s(2650)+3 Such that:aux(293) =< 1 aux(338) =< V1 aux(339) =< V s(2650) =< aux(338) s(103) =< aux(339) s(144) =< aux(293) s(104) =< s(103)*aux(339) s(105) =< s(104) with precondition: [V2=0,V1>=1,V>=1,Out>=5] * Chain [54,48]: 26*s(2789)+10*s(2791)+51*s(2844)+18*s(2846)+3 Such that:aux(298) =< 1 aux(340) =< V1 aux(341) =< V s(2789) =< aux(340) s(2791) =< aux(298) s(2844) =< aux(341) s(2845) =< s(2844)*aux(341) s(2846) =< s(2845) with precondition: [V2=0,V1>=1,V>=1,Out>=5] * Chain [54,47]: 20*s(2823)+2*s(2835)+51*s(2844)+18*s(2846)+3 Such that:aux(311) =< 1 aux(342) =< V1 aux(343) =< V s(2823) =< aux(342) s(2835) =< aux(311) s(2844) =< aux(343) s(2845) =< s(2844)*aux(343) s(2846) =< s(2845) with precondition: [V2=0,V1>=1,V>=1,Out>=6] * Chain [51]: 1 with precondition: [Out=1,V1>=0,V>=0,V2>=0] * Chain [50]: 1 with precondition: [V2=0,Out=1,V1>=1,V>=0] * Chain [49]: 2959*s(103)+1002*s(105)+120*s(144)+109*s(2650)+1 Such that:aux(291) =< V1 aux(292) =< V aux(293) =< V2 s(2650) =< aux(291) s(103) =< aux(292) s(144) =< aux(293) s(104) =< s(103)*aux(292) s(105) =< s(104) with precondition: [V1>=0,V>=1,V2>=0,Out>=2] * Chain [48]: 24*s(2789)+10*s(2791)+1 Such that:aux(297) =< V1 aux(298) =< V2 s(2789) =< aux(297) s(2791) =< aux(298) with precondition: [V>=0,V2>=0,Out>=2,V1+1>=Out] * Chain [47]: 18*s(2823)+2*s(2835)+1 Such that:aux(310) =< V1 aux(311) =< V2 s(2823) =< aux(310) s(2835) =< aux(311) with precondition: [V>=0,V2>=1,Out>=3,2*V1+1>=Out,V1+V2+1>=Out] #### Cost of chains of start(V1,V,V2,V13,V9): * Chain [59]: 429*s(3130)+5931*s(3131)+132*s(3132)+2004*s(3134)+16*s(3135)+4*s(3140)+40*s(3141)+272*s(3142)+96*s(3144)+2*s(3157)+3 Such that:s(3127) =< V1-V2 s(3129) =< V-V2 aux(351) =< V1 aux(352) =< V aux(353) =< V2 s(3130) =< aux(351) s(3131) =< aux(352) s(3132) =< aux(353) s(3133) =< s(3131)*aux(352) s(3134) =< s(3133) s(3135) =< s(3127) s(3135) =< s(3129) s(3136) =< aux(352) s(3137) =< aux(351) s(3138) =< s(3135)*aux(351) s(3139) =< s(3135)*s(3136) s(3140) =< s(3135)*s(3137) s(3141) =< s(3138) s(3142) =< s(3139) s(3143) =< s(3142)*aux(352) s(3144) =< s(3143) s(3156) =< s(3130)*aux(351) s(3157) =< s(3156) with precondition: [V1>=0] * Chain [58]: 422*s(3165)+5930*s(3166)+132*s(3167)+2004*s(3169)+16*s(3170)+4*s(3175)+40*s(3176)+272*s(3177)+96*s(3179)+4 Such that:s(3162) =< V2-V9 s(3163) =< V13 s(3164) =< V13-V9 aux(354) =< V2 aux(355) =< V9+1 s(3165) =< aux(354) s(3166) =< s(3163) s(3167) =< aux(355) s(3168) =< s(3166)*s(3163) s(3169) =< s(3168) s(3170) =< s(3162) s(3170) =< s(3164) s(3171) =< s(3163) s(3172) =< aux(354) s(3173) =< s(3170)*aux(354) s(3174) =< s(3170)*s(3171) s(3175) =< s(3170)*s(3172) s(3176) =< s(3173) s(3177) =< s(3174) s(3178) =< s(3177)*s(3163) s(3179) =< s(3178) with precondition: [V1=1,V=1,V2>=0,V13>=0,V9>=0] * Chain [57]: 0 with precondition: [V=0,V1>=1] * Chain [56]: 860*s(3191)+264*s(3192)+12268*s(3193)+4152*s(3195)+32*s(3196)+8*s(3201)+80*s(3202)+544*s(3203)+192*s(3205)+3 Such that:s(3188) =< 1 s(3189) =< V1 s(3190) =< V s(3191) =< s(3189) s(3192) =< s(3188) s(3193) =< s(3190) s(3194) =< s(3193)*s(3190) s(3195) =< s(3194) s(3196) =< s(3189) s(3196) =< s(3190) s(3197) =< s(3190) s(3198) =< s(3189) s(3199) =< s(3196)*s(3189) s(3200) =< s(3196)*s(3197) s(3201) =< s(3196)*s(3198) s(3202) =< s(3199) s(3203) =< s(3200) s(3204) =< s(3203)*s(3190) s(3205) =< s(3204) with precondition: [V2=0,V1>=1,V>=1] Closed-form bounds of start(V1,V,V2,V13,V9): ------------------------------------- * Chain [59] with precondition: [V1>=0] - Upper bound: 429*V1+3+2*V1*V1+44*V1*nat(V1-V2)+nat(V)*5931+nat(V)*2004*nat(V)+nat(V)*96*nat(V)*nat(V1-V2)+nat(V)*272*nat(V1-V2)+nat(V2)*132+nat(V1-V2)*16 - Complexity: n^3 * Chain [58] with precondition: [V1=1,V=1,V2>=0,V13>=0,V9>=0] - Upper bound: 422*V2+4+44*V2*nat(V2-V9)+5930*V13+2004*V13*V13+96*V13*V13*nat(V2-V9)+272*V13*nat(V2-V9)+(132*V9+132)+nat(V2-V9)*16 - Complexity: n^3 * Chain [57] with precondition: [V=0,V1>=1] - Upper bound: 0 - Complexity: constant * Chain [56] with precondition: [V2=0,V1>=1,V>=1] - Upper bound: 892*V1+267+88*V1*V1+544*V1*V+192*V1*V*V+12268*V+4152*V*V - Complexity: n^3 ### Maximum cost of start(V1,V,V2,V13,V9): max([429*V1+3+2*V1*V1+nat(V)*5931+nat(V)*2004*nat(V)+max([nat(V)*96*nat(V)*nat(V1-V2)+44*V1*nat(V1-V2)+nat(V)*272*nat(V1-V2)+nat(V2)*132+nat(V1-V2)*16,463*V1+264+86*V1*V1+544*V1*nat(V)+192*V1*nat(V)*nat(V)+nat(V)*6337+nat(V)*2148*nat(V)]),nat(V2)*422+4+nat(V2)*44*nat(V2-V9)+nat(V13)*5930+nat(V13)*2004*nat(V13)+nat(V13)*96*nat(V13)*nat(V2-V9)+nat(V13)*272*nat(V2-V9)+nat(V9+1)*132+nat(V2-V9)*16]) Asymptotic class: n^3 * Total analysis performed in 23928 ms. ---------------------------------------- (18) BOUNDS(1, n^3)