WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1014 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxWeightedTrs (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxTypedWeightedTrs (7) CompletionProof [UPPER BOUND(ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 14 ms] (10) CpxRNTS (11) CompleteCoflocoProof [FINISHED, 22.8 s] (12) BOUNDS(1, n^2) (13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (14) TRS for Loop Detection (15) DecreasingLoopProof [LOWER BOUND(ID), 2 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) PLUS(z0, 0) -> c2 PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) LENGTH(nil) -> c4 LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) GE(z0, 0) -> c7 GE(0, s(z0)) -> c8 GE(s(z0), s(z1)) -> c9(GE(z0, z1)) IF(true, z0, z1, z2, z3) -> c10 IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) TAKE(0, cons(z0, xs), z1) -> c12 TAKE(0, nil, cons(z0, z1)) -> c13 TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) The (relative) TRS S consists of the following rules: app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) plus(z0, 0) -> z0 plus(z0, s(z1)) -> s(plus(z0, z1)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) if(true, z0, z1, z2, z3) -> nil if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) take(0, cons(z0, xs), z1) -> z0 take(0, nil, cons(z0, z1)) -> z0 take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) PLUS(z0, 0) -> c2 PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) LENGTH(nil) -> c4 LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) GE(z0, 0) -> c7 GE(0, s(z0)) -> c8 GE(s(z0), s(z1)) -> c9(GE(z0, z1)) IF(true, z0, z1, z2, z3) -> c10 IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) TAKE(0, cons(z0, xs), z1) -> c12 TAKE(0, nil, cons(z0, z1)) -> c13 TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) The (relative) TRS S consists of the following rules: app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) plus(z0, 0) -> z0 plus(z0, s(z1)) -> s(plus(z0, z1)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) if(true, z0, z1, z2, z3) -> nil if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) take(0, cons(z0, xs), z1) -> z0 take(0, nil, cons(z0, z1)) -> z0 take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) [1] APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) [1] PLUS(z0, 0) -> c2 [1] PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1] LENGTH(nil) -> c4 [1] LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1] HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1] GE(z0, 0) -> c7 [1] GE(0, s(z0)) -> c8 [1] GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1] IF(true, z0, z1, z2, z3) -> c10 [1] IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1] TAKE(0, cons(z0, xs), z1) -> c12 [1] TAKE(0, nil, cons(z0, z1)) -> c13 [1] TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) [1] TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1] HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1] HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1] app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) [0] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] if(true, z0, z1, z2, z3) -> nil [0] if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) [0] take(0, cons(z0, xs), z1) -> z0 [0] take(0, nil, cons(z0, z1)) -> z0 [0] take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) [0] take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) [0] helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) [1] APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) [1] PLUS(z0, 0) -> c2 [1] PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1] LENGTH(nil) -> c4 [1] LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1] HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1] GE(z0, 0) -> c7 [1] GE(0, s(z0)) -> c8 [1] GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1] IF(true, z0, z1, z2, z3) -> c10 [1] IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1] TAKE(0, cons(z0, xs), z1) -> c12 [1] TAKE(0, nil, cons(z0, z1)) -> c13 [1] TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) [1] TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1] HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1] HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1] app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) [0] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] if(true, z0, z1, z2, z3) -> nil [0] if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) [0] take(0, cons(z0, xs), z1) -> z0 [0] take(0, nil, cons(z0, z1)) -> z0 [0] take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) [0] take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) [0] helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) [0] The TRS has the following type information: APP :: nil:cons:xs -> nil:cons:xs -> c:c1 c :: c6 -> c2:c3 -> c4:c5 -> c:c1 HELPA :: 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> c6 0 :: 0:s plus :: 0:s -> 0:s -> 0:s length :: nil:cons:xs -> 0:s PLUS :: 0:s -> 0:s -> c2:c3 LENGTH :: nil:cons:xs -> c4:c5 c1 :: c6 -> c2:c3 -> c4:c5 -> c:c1 c2 :: c2:c3 s :: 0:s -> 0:s c3 :: c2:c3 -> c2:c3 nil :: nil:cons:xs c4 :: c4:c5 cons :: take -> nil:cons:xs -> nil:cons:xs c5 :: c4:c5 -> c4:c5 c6 :: c10:c11 -> c7:c8:c9 -> c6 IF :: true:false -> 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> c10:c11 ge :: 0:s -> 0:s -> true:false GE :: 0:s -> 0:s -> c7:c8:c9 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 true :: true:false c10 :: c10:c11 false :: true:false c11 :: c16:c17 -> c10:c11 HELPB :: 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> c16:c17 TAKE :: 0:s -> nil:cons:xs -> nil:cons:xs -> c12:c13:c14:c15 xs :: nil:cons:xs c12 :: c12:c13:c14:c15 c13 :: c12:c13:c14:c15 c14 :: c12:c13:c14:c15 -> c12:c13:c14:c15 c15 :: c12:c13:c14:c15 -> c12:c13:c14:c15 c16 :: c12:c13:c14:c15 -> c16:c17 c17 :: c6 -> c16:c17 app :: nil:cons:xs -> nil:cons:xs -> nil:cons:xs helpa :: 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs if :: true:false -> 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs helpb :: 0:s -> 0:s -> nil:cons:xs -> nil:cons:xs -> nil:cons:xs take :: 0:s -> nil:cons:xs -> nil:cons:xs -> take Rewrite Strategy: INNERMOST ---------------------------------------- (7) 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: app(v0, v1) -> null_app [0] plus(v0, v1) -> null_plus [0] length(v0) -> null_length [0] helpa(v0, v1, v2, v3) -> null_helpa [0] ge(v0, v1) -> null_ge [0] if(v0, v1, v2, v3, v4) -> null_if [0] take(v0, v1, v2) -> null_take [0] helpb(v0, v1, v2, v3) -> null_helpb [0] PLUS(v0, v1) -> null_PLUS [0] LENGTH(v0) -> null_LENGTH [0] GE(v0, v1) -> null_GE [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] TAKE(v0, v1, v2) -> null_TAKE [0] And the following fresh constants: null_app, null_plus, null_length, null_helpa, null_ge, null_if, null_take, null_helpb, null_PLUS, null_LENGTH, null_GE, null_IF, null_TAKE, const, const1, const2 ---------------------------------------- (8) 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: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) [1] APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) [1] PLUS(z0, 0) -> c2 [1] PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) [1] LENGTH(nil) -> c4 [1] LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) [1] HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) [1] GE(z0, 0) -> c7 [1] GE(0, s(z0)) -> c8 [1] GE(s(z0), s(z1)) -> c9(GE(z0, z1)) [1] IF(true, z0, z1, z2, z3) -> c10 [1] IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) [1] TAKE(0, cons(z0, xs), z1) -> c12 [1] TAKE(0, nil, cons(z0, z1)) -> c13 [1] TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) [1] TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) [1] HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) [1] HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) [1] app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] length(nil) -> 0 [0] length(cons(z0, z1)) -> s(length(z1)) [0] helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) [0] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] if(true, z0, z1, z2, z3) -> nil [0] if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) [0] take(0, cons(z0, xs), z1) -> z0 [0] take(0, nil, cons(z0, z1)) -> z0 [0] take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) [0] take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) [0] helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) [0] app(v0, v1) -> null_app [0] plus(v0, v1) -> null_plus [0] length(v0) -> null_length [0] helpa(v0, v1, v2, v3) -> null_helpa [0] ge(v0, v1) -> null_ge [0] if(v0, v1, v2, v3, v4) -> null_if [0] take(v0, v1, v2) -> null_take [0] helpb(v0, v1, v2, v3) -> null_helpb [0] PLUS(v0, v1) -> null_PLUS [0] LENGTH(v0) -> null_LENGTH [0] GE(v0, v1) -> null_GE [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] TAKE(v0, v1, v2) -> null_TAKE [0] The TRS has the following type information: APP :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c:c1 c :: c6 -> c2:c3:null_PLUS -> c4:c5:null_LENGTH -> c:c1 HELPA :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c6 0 :: 0:s:null_plus:null_length plus :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> 0:s:null_plus:null_length length :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> 0:s:null_plus:null_length PLUS :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> c2:c3:null_PLUS LENGTH :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c4:c5:null_LENGTH c1 :: c6 -> c2:c3:null_PLUS -> c4:c5:null_LENGTH -> c:c1 c2 :: c2:c3:null_PLUS s :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length c3 :: c2:c3:null_PLUS -> c2:c3:null_PLUS nil :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb c4 :: c4:c5:null_LENGTH cons :: null_take -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb c5 :: c4:c5:null_LENGTH -> c4:c5:null_LENGTH c6 :: c10:c11:null_IF -> c7:c8:c9:null_GE -> c6 IF :: true:false:null_ge -> 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c10:c11:null_IF ge :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> true:false:null_ge GE :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> c7:c8:c9:null_GE c7 :: c7:c8:c9:null_GE c8 :: c7:c8:c9:null_GE c9 :: c7:c8:c9:null_GE -> c7:c8:c9:null_GE true :: true:false:null_ge c10 :: c10:c11:null_IF false :: true:false:null_ge c11 :: c16:c17 -> c10:c11:null_IF HELPB :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c16:c17 TAKE :: 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> c12:c13:c14:c15:null_TAKE xs :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb c12 :: c12:c13:c14:c15:null_TAKE c13 :: c12:c13:c14:c15:null_TAKE c14 :: c12:c13:c14:c15:null_TAKE -> c12:c13:c14:c15:null_TAKE c15 :: c12:c13:c14:c15:null_TAKE -> c12:c13:c14:c15:null_TAKE c16 :: c12:c13:c14:c15:null_TAKE -> c16:c17 c17 :: c6 -> c16:c17 app :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb helpa :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb if :: true:false:null_ge -> 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb helpb :: 0:s:null_plus:null_length -> 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb take :: 0:s:null_plus:null_length -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> nil:cons:xs:null_app:null_helpa:null_if:null_helpb -> null_take null_app :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb null_plus :: 0:s:null_plus:null_length null_length :: 0:s:null_plus:null_length null_helpa :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb null_ge :: true:false:null_ge null_if :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb null_take :: null_take null_helpb :: nil:cons:xs:null_app:null_helpa:null_if:null_helpb null_PLUS :: c2:c3:null_PLUS null_LENGTH :: c4:c5:null_LENGTH null_GE :: c7:c8:c9:null_GE null_IF :: c10:c11:null_IF null_TAKE :: c12:c13:c14:c15:null_TAKE const :: c:c1 const1 :: c6 const2 :: c16:c17 Rewrite Strategy: INNERMOST ---------------------------------------- (9) 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 c2 => 0 nil => 0 c4 => 0 c7 => 0 c8 => 1 true => 2 c10 => 0 false => 1 xs => 1 c12 => 0 c13 => 1 null_app => 0 null_plus => 0 null_length => 0 null_helpa => 0 null_ge => 0 null_if => 0 null_take => 0 null_helpb => 0 null_PLUS => 0 null_LENGTH => 0 null_GE => 0 null_IF => 0 null_TAKE => 0 const => 0 const1 => 0 const2 => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: APP(z, z') -{ 1 }-> 1 + HELPA(0, plus(length(z0), length(z1)), z0, z1) + PLUS(length(z0), length(z1)) + LENGTH(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 APP(z, z') -{ 1 }-> 1 + HELPA(0, plus(length(z0), length(z1)), z0, z1) + PLUS(length(z0), length(z1)) + LENGTH(z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 GE(z, z') -{ 1 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0 GE(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0 GE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GE(z, z') -{ 1 }-> 1 + GE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 HELPA(z, z', z'', z4) -{ 1 }-> 1 + IF(ge(z0, z1), z0, z1, z2, z3) + GE(z0, z1) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0 HELPB(z, z', z'', z4) -{ 1 }-> 1 + TAKE(z0, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0 HELPB(z, z', z'', z4) -{ 1 }-> 1 + HELPA(1 + z0, z1, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 IF(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 1 + HELPB(z0, z1, z2, z3) :|: z1 >= 0, z = 1, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 LENGTH(z) -{ 1 }-> 0 :|: z = 0 LENGTH(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 LENGTH(z) -{ 1 }-> 1 + LENGTH(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 PLUS(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0 PLUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 PLUS(z, z') -{ 1 }-> 1 + PLUS(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 TAKE(z, z', z'') -{ 1 }-> 1 :|: z1 >= 0, z'' = 1 + z0 + z1, z0 >= 0, z = 0, z' = 0 TAKE(z, z', z'') -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 0, z' = 1 + z0 + 1, z'' = z1 TAKE(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 TAKE(z, z', z'') -{ 1 }-> 1 + TAKE(z0, 1, z2) :|: z' = 1 + z1 + 1, z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0 TAKE(z, z', z'') -{ 1 }-> 1 + TAKE(z0, 0, z2) :|: z1 >= 0, z'' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0 app(z, z') -{ 0 }-> helpa(0, plus(length(z0), length(z1)), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 app(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ge(z, z') -{ 0 }-> ge(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ge(z, z') -{ 0 }-> 2 :|: z = z0, z0 >= 0, z' = 0 ge(z, z') -{ 0 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0 ge(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 helpa(z, z', z'', z4) -{ 0 }-> if(ge(z0, z1), z0, z1, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0 helpa(z, z', z'', z4) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 helpb(z, z', z'', z4) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 helpb(z, z', z'', z4) -{ 0 }-> 1 + take(z0, z2, z3) + helpa(1 + z0, z1, z2, z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0 if(z, z', z'', z4, z5) -{ 0 }-> helpb(z0, z1, z2, z3) :|: z1 >= 0, z = 1, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 if(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 if(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 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 plus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 plus(z, z') -{ 0 }-> 1 + plus(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 take(z, z', z'') -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 0, z' = 1 + z0 + 1, z'' = z1 take(z, z', z'') -{ 0 }-> z0 :|: z1 >= 0, z'' = 1 + z0 + z1, z0 >= 0, z = 0, z' = 0 take(z, z', z'') -{ 0 }-> take(z0, 1, z2) :|: z' = 1 + z1 + 1, z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0 take(z, z', z'') -{ 0 }-> take(z0, 0, z2) :|: z1 >= 0, z'' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0 take(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (11) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V14, V12, V23),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun3(V1, Out)],[V1 >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun1(V1, V, V14, V12, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun5(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun4(V1, V, V14, V12, V23, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0,V23 >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun7(V1, V, V14, Out)],[V1 >= 0,V >= 0,V14 >= 0]). eq(start(V1, V, V14, V12, V23),0,[fun6(V1, V, V14, V12, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0]). eq(start(V1, V, V14, V12, V23),0,[app(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[plus(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[length(V1, Out)],[V1 >= 0]). eq(start(V1, V, V14, V12, V23),0,[helpa(V1, V, V14, V12, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0]). eq(start(V1, V, V14, V12, V23),0,[ge(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V14, V12, V23),0,[if(V1, V, V14, V12, V23, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0,V23 >= 0]). eq(start(V1, V, V14, V12, V23),0,[take(V1, V, V14, Out)],[V1 >= 0,V >= 0,V14 >= 0]). eq(start(V1, V, V14, V12, V23),0,[helpb(V1, V, V14, V12, Out)],[V1 >= 0,V >= 0,V14 >= 0,V12 >= 0]). eq(fun(V1, V, Out),1,[length(V3, Ret00110),length(V2, Ret00111),plus(Ret00110, Ret00111, Ret0011),fun1(0, Ret0011, V3, V2, Ret001),length(V3, Ret010),length(V2, Ret011),fun2(Ret010, Ret011, Ret01),fun3(V3, Ret1)],[Out = 1 + Ret001 + Ret01 + Ret1,V1 = V3,V2 >= 0,V = V2,V3 >= 0]). eq(fun(V1, V, Out),1,[length(V5, Ret001101),length(V4, Ret001111),plus(Ret001101, Ret001111, Ret00112),fun1(0, Ret00112, V5, V4, Ret0012),length(V5, Ret0101),length(V4, Ret0111),fun2(Ret0101, Ret0111, Ret012),fun3(V4, Ret11)],[Out = 1 + Ret0012 + Ret012 + Ret11,V1 = V5,V4 >= 0,V = V4,V5 >= 0]). eq(fun2(V1, V, Out),1,[],[Out = 0,V1 = V6,V6 >= 0,V = 0]). eq(fun2(V1, V, Out),1,[fun2(V7, V8, Ret12)],[Out = 1 + Ret12,V1 = V7,V8 >= 0,V7 >= 0,V = 1 + V8]). eq(fun3(V1, Out),1,[],[Out = 0,V1 = 0]). eq(fun3(V1, Out),1,[fun3(V10, Ret13)],[Out = 1 + Ret13,V10 >= 0,V9 >= 0,V1 = 1 + V10 + V9]). eq(fun1(V1, V, V14, V12, Out),1,[ge(V13, V11, Ret0102),fun4(Ret0102, V13, V11, V16, V15, Ret013),fun5(V13, V11, Ret14)],[Out = 1 + Ret013 + Ret14,V14 = V16,V1 = V13,V11 >= 0,V = V11,V13 >= 0,V12 = V15,V16 >= 0,V15 >= 0]). eq(fun5(V1, V, Out),1,[],[Out = 0,V1 = V17,V17 >= 0,V = 0]). eq(fun5(V1, V, Out),1,[],[Out = 1,V18 >= 0,V = 1 + V18,V1 = 0]). eq(fun5(V1, V, Out),1,[fun5(V20, V19, Ret15)],[Out = 1 + Ret15,V19 >= 0,V1 = 1 + V20,V20 >= 0,V = 1 + V19]). eq(fun4(V1, V, V14, V12, V23, Out),1,[],[Out = 0,V1 = 2,V22 >= 0,V21 >= 0,V23 = V25,V = V21,V24 >= 0,V25 >= 0,V14 = V22,V12 = V24]). eq(fun4(V1, V, V14, V12, V23, Out),1,[fun6(V29, V26, V28, V27, Ret16)],[Out = 1 + Ret16,V26 >= 0,V1 = 1,V29 >= 0,V23 = V27,V = V29,V28 >= 0,V27 >= 0,V14 = V26,V12 = V28]). eq(fun7(V1, V, V14, Out),1,[],[Out = 0,V31 >= 0,V30 >= 0,V1 = 0,V = 2 + V30,V14 = V31]). eq(fun7(V1, V, V14, Out),1,[],[Out = 1,V33 >= 0,V14 = 1 + V32 + V33,V32 >= 0,V1 = 0,V = 0]). eq(fun7(V1, V, V14, Out),1,[fun7(V34, 1, V35, Ret17)],[Out = 1 + Ret17,V = 2 + V36,V14 = V35,V36 >= 0,V1 = 1 + V34,V34 >= 0,V35 >= 0]). eq(fun7(V1, V, V14, Out),1,[fun7(V39, 0, V38, Ret18)],[Out = 1 + Ret18,V37 >= 0,V14 = 1 + V37 + V38,V1 = 1 + V39,V39 >= 0,V38 >= 0,V = 0]). eq(fun6(V1, V, V14, V12, Out),1,[fun7(V43, V40, V41, Ret19)],[Out = 1 + Ret19,V14 = V40,V1 = V43,V42 >= 0,V = V42,V43 >= 0,V12 = V41,V40 >= 0,V41 >= 0]). eq(fun6(V1, V, V14, V12, Out),1,[fun1(1 + V46, V47, V44, V45, Ret110)],[Out = 1 + Ret110,V14 = V44,V1 = V46,V47 >= 0,V = V47,V46 >= 0,V12 = V45,V44 >= 0,V45 >= 0]). eq(app(V1, V, Out),0,[length(V48, Ret10),length(V49, Ret111),plus(Ret10, Ret111, Ret112),helpa(0, Ret112, V48, V49, Ret)],[Out = Ret,V1 = V48,V49 >= 0,V = V49,V48 >= 0]). eq(plus(V1, V, Out),0,[],[Out = V50,V1 = V50,V50 >= 0,V = 0]). eq(plus(V1, V, Out),0,[plus(V51, V52, Ret113)],[Out = 1 + Ret113,V1 = V51,V52 >= 0,V51 >= 0,V = 1 + V52]). eq(length(V1, Out),0,[],[Out = 0,V1 = 0]). eq(length(V1, Out),0,[length(V54, Ret114)],[Out = 1 + Ret114,V54 >= 0,V53 >= 0,V1 = 1 + V53 + V54]). eq(helpa(V1, V, V14, V12, Out),0,[ge(V56, V58, Ret0),if(Ret0, V56, V58, V55, V57, Ret2)],[Out = Ret2,V14 = V55,V1 = V56,V58 >= 0,V = V58,V56 >= 0,V12 = V57,V55 >= 0,V57 >= 0]). eq(ge(V1, V, Out),0,[],[Out = 2,V1 = V59,V59 >= 0,V = 0]). eq(ge(V1, V, Out),0,[],[Out = 1,V60 >= 0,V = 1 + V60,V1 = 0]). eq(ge(V1, V, Out),0,[ge(V61, V62, Ret3)],[Out = Ret3,V62 >= 0,V1 = 1 + V61,V61 >= 0,V = 1 + V62]). eq(if(V1, V, V14, V12, V23, Out),0,[],[Out = 0,V1 = 2,V64 >= 0,V66 >= 0,V23 = V63,V = V66,V65 >= 0,V63 >= 0,V14 = V64,V12 = V65]). eq(if(V1, V, V14, V12, V23, Out),0,[helpb(V70, V68, V69, V67, Ret4)],[Out = Ret4,V68 >= 0,V1 = 1,V70 >= 0,V23 = V67,V = V70,V69 >= 0,V67 >= 0,V14 = V68,V12 = V69]). eq(take(V1, V, V14, Out),0,[],[Out = V72,V71 >= 0,V72 >= 0,V1 = 0,V = 2 + V72,V14 = V71]). eq(take(V1, V, V14, Out),0,[],[Out = V74,V73 >= 0,V14 = 1 + V73 + V74,V74 >= 0,V1 = 0,V = 0]). eq(take(V1, V, V14, Out),0,[take(V75, 1, V76, Ret5)],[Out = Ret5,V = 2 + V77,V14 = V76,V77 >= 0,V1 = 1 + V75,V75 >= 0,V76 >= 0]). eq(take(V1, V, V14, Out),0,[take(V78, 0, V79, Ret6)],[Out = Ret6,V80 >= 0,V14 = 1 + V79 + V80,V1 = 1 + V78,V78 >= 0,V79 >= 0,V = 0]). eq(helpb(V1, V, V14, V12, Out),0,[take(V81, V83, V82, Ret014),helpa(1 + V81, V84, V83, V82, Ret115)],[Out = 1 + Ret014 + Ret115,V14 = V83,V1 = V81,V84 >= 0,V = V84,V81 >= 0,V12 = V82,V83 >= 0,V82 >= 0]). eq(app(V1, V, Out),0,[],[Out = 0,V86 >= 0,V85 >= 0,V1 = V86,V = V85]). eq(plus(V1, V, Out),0,[],[Out = 0,V88 >= 0,V87 >= 0,V1 = V88,V = V87]). eq(length(V1, Out),0,[],[Out = 0,V89 >= 0,V1 = V89]). eq(helpa(V1, V, V14, V12, Out),0,[],[Out = 0,V90 >= 0,V14 = V93,V91 >= 0,V1 = V90,V = V91,V12 = V92,V93 >= 0,V92 >= 0]). eq(ge(V1, V, Out),0,[],[Out = 0,V94 >= 0,V95 >= 0,V1 = V94,V = V95]). eq(if(V1, V, V14, V12, V23, Out),0,[],[Out = 0,V23 = V99,V97 >= 0,V99 >= 0,V14 = V98,V96 >= 0,V1 = V97,V = V96,V12 = V100,V98 >= 0,V100 >= 0]). eq(take(V1, V, V14, Out),0,[],[Out = 0,V102 >= 0,V14 = V103,V101 >= 0,V1 = V102,V = V101,V103 >= 0]). eq(helpb(V1, V, V14, V12, Out),0,[],[Out = 0,V104 >= 0,V14 = V107,V105 >= 0,V1 = V104,V = V105,V12 = V106,V107 >= 0,V106 >= 0]). eq(fun2(V1, V, Out),0,[],[Out = 0,V108 >= 0,V109 >= 0,V1 = V108,V = V109]). eq(fun3(V1, Out),0,[],[Out = 0,V110 >= 0,V1 = V110]). eq(fun5(V1, V, Out),0,[],[Out = 0,V112 >= 0,V111 >= 0,V1 = V112,V = V111]). eq(fun4(V1, V, V14, V12, V23, Out),0,[],[Out = 0,V23 = V117,V114 >= 0,V117 >= 0,V14 = V116,V113 >= 0,V1 = V114,V = V113,V12 = V115,V116 >= 0,V115 >= 0]). eq(fun7(V1, V, V14, Out),0,[],[Out = 0,V120 >= 0,V14 = V118,V119 >= 0,V1 = V120,V = V119,V118 >= 0]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,V,Out),[V1,V],[Out]). input_output_vars(fun3(V1,Out),[V1],[Out]). input_output_vars(fun1(V1,V,V14,V12,Out),[V1,V,V14,V12],[Out]). input_output_vars(fun5(V1,V,Out),[V1,V],[Out]). input_output_vars(fun4(V1,V,V14,V12,V23,Out),[V1,V,V14,V12,V23],[Out]). input_output_vars(fun7(V1,V,V14,Out),[V1,V,V14],[Out]). input_output_vars(fun6(V1,V,V14,V12,Out),[V1,V,V14,V12],[Out]). input_output_vars(app(V1,V,Out),[V1,V],[Out]). input_output_vars(plus(V1,V,Out),[V1,V],[Out]). input_output_vars(length(V1,Out),[V1],[Out]). input_output_vars(helpa(V1,V,V14,V12,Out),[V1,V,V14,V12],[Out]). input_output_vars(ge(V1,V,Out),[V1,V],[Out]). input_output_vars(if(V1,V,V14,V12,V23,Out),[V1,V,V14,V12,V23],[Out]). input_output_vars(take(V1,V,V14,Out),[V1,V,V14],[Out]). input_output_vars(helpb(V1,V,V14,V12,Out),[V1,V,V14,V12],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [ge/3] 1. recursive : [take/4] 2. recursive : [helpa/5,helpb/5,if/6] 3. recursive : [length/2] 4. recursive : [plus/3] 5. non_recursive : [app/3] 6. recursive : [fun7/4] 7. recursive : [fun5/3] 8. recursive [non_tail] : [fun1/5,fun4/6,fun6/5] 9. recursive : [fun2/3] 10. recursive : [fun3/2] 11. non_recursive : [fun/3] 12. non_recursive : [start/5] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into ge/3 1. SCC is partially evaluated into take/4 2. SCC is partially evaluated into helpa/5 3. SCC is partially evaluated into length/2 4. SCC is partially evaluated into plus/3 5. SCC is partially evaluated into app/3 6. SCC is partially evaluated into fun7/4 7. SCC is partially evaluated into fun5/3 8. SCC is partially evaluated into fun1/5 9. SCC is partially evaluated into fun2/3 10. SCC is partially evaluated into fun3/2 11. SCC is partially evaluated into fun/3 12. SCC is partially evaluated into start/5 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations ge/3 * CE 60 is refined into CE [61] * CE 57 is refined into CE [62] * CE 58 is refined into CE [63] * CE 59 is refined into CE [64] ### Cost equations --> "Loop" of ge/3 * CEs [64] --> Loop 34 * CEs [61] --> Loop 35 * CEs [62] --> Loop 36 * CEs [63] --> Loop 37 ### Ranking functions of CR ge(V1,V,Out) * RF of phase [34]: [V,V1] #### Partial ranking functions of CR ge(V1,V,Out) * Partial RF of phase [34]: - RF of loop [34:1]: V V1 ### Specialization of cost equations take/4 * CE 34 is refined into CE [65] * CE 30 is refined into CE [66] * CE 31 is refined into CE [67] * CE 32 is refined into CE [68] * CE 33 is refined into CE [69] ### Cost equations --> "Loop" of take/4 * CEs [68] --> Loop 38 * CEs [69] --> Loop 39 * CEs [65] --> Loop 40 * CEs [66] --> Loop 41 * CEs [67] --> Loop 42 ### Ranking functions of CR take(V1,V,V14,Out) * RF of phase [39]: [V1,V14] #### Partial ranking functions of CR take(V1,V,V14,Out) * Partial RF of phase [39]: - RF of loop [39:1]: V1 V14 ### Specialization of cost equations helpa/5 * CE 35 is refined into CE [70,71,72,73,74] * CE 37 is refined into CE [75] * CE 36 is refined into CE [76,77,78,79,80] ### Cost equations --> "Loop" of helpa/5 * CEs [79] --> Loop 43 * CEs [80] --> Loop 44 * CEs [77] --> Loop 45 * CEs [78] --> Loop 46 * CEs [76] --> Loop 47 * CEs [71] --> Loop 48 * CEs [70,72,73,74,75] --> Loop 49 ### Ranking functions of CR helpa(V1,V,V14,V12,Out) * RF of phase [43,44]: [-V1+V] #### Partial ranking functions of CR helpa(V1,V,V14,V12,Out) * Partial RF of phase [43,44]: - RF of loop [43:1,44:1]: -V1+V - RF of loop [44:1]: -V1+V12 ### Specialization of cost equations length/2 * CE 55 is refined into CE [81] * CE 56 is refined into CE [82] ### Cost equations --> "Loop" of length/2 * CEs [82] --> Loop 50 * CEs [81] --> Loop 51 ### Ranking functions of CR length(V1,Out) * RF of phase [50]: [V1] #### Partial ranking functions of CR length(V1,Out) * Partial RF of phase [50]: - RF of loop [50:1]: V1 ### Specialization of cost equations plus/3 * CE 54 is refined into CE [83] * CE 52 is refined into CE [84] * CE 53 is refined into CE [85] ### Cost equations --> "Loop" of plus/3 * CEs [85] --> Loop 52 * CEs [83] --> Loop 53 * CEs [84] --> Loop 54 ### Ranking functions of CR plus(V1,V,Out) * RF of phase [52]: [V] #### Partial ranking functions of CR plus(V1,V,Out) * Partial RF of phase [52]: - RF of loop [52:1]: V ### Specialization of cost equations app/3 * CE 50 is refined into CE [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,111,112] * CE 51 is refined into CE [113] ### Cost equations --> "Loop" of app/3 * CEs [99] --> Loop 55 * CEs [105] --> Loop 56 * CEs [90,95,109] --> Loop 57 * CEs [92,97,101,107,111] --> Loop 58 * CEs [100] --> Loop 59 * CEs [91,96,106,110] --> Loop 60 * CEs [86,87,88,93,98,102,103,104,108,112,113] --> Loop 61 * CEs [89,94] --> Loop 62 ### Ranking functions of CR app(V1,V,Out) #### Partial ranking functions of CR app(V1,V,Out) ### Specialization of cost equations fun7/4 * CE 21 is refined into CE [114] * CE 25 is refined into CE [115] * CE 22 is refined into CE [116] * CE 23 is refined into CE [117] * CE 24 is refined into CE [118] ### Cost equations --> "Loop" of fun7/4 * CEs [117] --> Loop 63 * CEs [118] --> Loop 64 * CEs [114,115] --> Loop 65 * CEs [116] --> Loop 66 ### Ranking functions of CR fun7(V1,V,V14,Out) * RF of phase [64]: [V1,V14] #### Partial ranking functions of CR fun7(V1,V,V14,Out) * Partial RF of phase [64]: - RF of loop [64:1]: V1 V14 ### Specialization of cost equations fun5/3 * CE 46 is refined into CE [119] * CE 49 is refined into CE [120] * CE 47 is refined into CE [121] * CE 48 is refined into CE [122] ### Cost equations --> "Loop" of fun5/3 * CEs [122] --> Loop 67 * CEs [119,120] --> Loop 68 * CEs [121] --> Loop 69 ### Ranking functions of CR fun5(V1,V,Out) * RF of phase [67]: [V,V1] #### Partial ranking functions of CR fun5(V1,V,Out) * Partial RF of phase [67]: - RF of loop [67:1]: V V1 ### Specialization of cost equations fun1/5 * CE 29 is refined into CE [123,124,125,126,127] * CE 26 is refined into CE [128,129,130,131,132,133,134,135,136,137,138,139] * CE 27 is refined into CE [140,141,142] * CE 28 is refined into CE [143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158] ### Cost equations --> "Loop" of fun1/5 * CEs [158] --> Loop 70 * CEs [139,142] --> Loop 71 * CEs [134,137] --> Loop 72 * CEs [133,136] --> Loop 73 * CEs [154] --> Loop 74 * CEs [157] --> Loop 75 * CEs [156] --> Loop 76 * CEs [153] --> Loop 77 * CEs [149,151] --> Loop 78 * CEs [150,155] --> Loop 79 * CEs [148] --> Loop 80 * CEs [147,152] --> Loop 81 * CEs [130,140] --> Loop 82 * CEs [146] --> Loop 83 * CEs [128,131] --> Loop 84 * CEs [129,132,135,138,141] --> Loop 85 * CEs [143] --> Loop 86 * CEs [144,145] --> Loop 87 * CEs [127] --> Loop 88 * CEs [126] --> Loop 89 * CEs [125] --> Loop 90 * CEs [123] --> Loop 91 * CEs [124] --> Loop 92 ### Ranking functions of CR fun1(V1,V,V14,V12,Out) * RF of phase [88,89,90]: [-V1+V] #### Partial ranking functions of CR fun1(V1,V,V14,V12,Out) * Partial RF of phase [88,89,90]: - RF of loop [88:1,89:1,90:1]: -V1+V ### Specialization of cost equations fun2/3 * CE 40 is refined into CE [159] * CE 42 is refined into CE [160] * CE 41 is refined into CE [161] ### Cost equations --> "Loop" of fun2/3 * CEs [161] --> Loop 93 * CEs [159,160] --> Loop 94 ### Ranking functions of CR fun2(V1,V,Out) * RF of phase [93]: [V] #### Partial ranking functions of CR fun2(V1,V,Out) * Partial RF of phase [93]: - RF of loop [93:1]: V ### Specialization of cost equations fun3/2 * CE 43 is refined into CE [162] * CE 45 is refined into CE [163] * CE 44 is refined into CE [164] ### Cost equations --> "Loop" of fun3/2 * CEs [164] --> Loop 95 * CEs [162,163] --> Loop 96 ### Ranking functions of CR fun3(V1,Out) * RF of phase [95]: [V1] #### Partial ranking functions of CR fun3(V1,Out) * Partial RF of phase [95]: - RF of loop [95:1]: V1 ### Specialization of cost equations fun/3 * CE 38 is refined into CE [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] * CE 39 is refined into CE [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,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,1369,1370,1371,1372,1373,1374,1375,1376,1377,1378,1379,1380,1381,1382,1383,1384,1385,1386,1387,1388,1389,1390,1391,1392,1393,1394,1395,1396,1397,1398,1399,1400,1401,1402,1403,1404,1405,1406,1407,1408,1409,1410,1411,1412,1413,1414,1415,1416,1417,1418,1419,1420,1421,1422,1423,1424,1425,1426,1427,1428,1429,1430,1431,1432,1433,1434,1435,1436,1437,1438,1439,1440,1441,1442,1443,1444,1445,1446,1447,1448,1449,1450,1451,1452,1453,1454,1455,1456,1457,1458,1459,1460,1461,1462,1463,1464,1465,1466,1467,1468,1469,1470,1471,1472,1473,1474,1475,1476,1477,1478,1479,1480,1481,1482,1483,1484,1485,1486,1487,1488,1489,1490,1491,1492,1493,1494,1495,1496,1497,1498,1499,1500,1501,1502,1503,1504,1505,1506,1507,1508,1509,1510,1511,1512,1513,1514,1515,1516,1517,1518,1519,1520,1521,1522,1523,1524,1525,1526,1527,1528,1529,1530,1531,1532,1533,1534,1535,1536,1537,1538,1539,1540,1541,1542,1543,1544,1545,1546,1547,1548,1549,1550,1551,1552,1553,1554,1555,1556] ### Cost equations --> "Loop" of fun/3 * CEs [478,484] --> Loop 97 * CEs [290,296,422,428,542,548,686,692,806,812] --> Loop 98 * CEs [278,284,410,416,530,536,674,680,794,800] --> Loop 99 * CEs [266,272,398,404,518,524,662,668,782,788] --> Loop 100 * CEs [170,176,182,188,194,200,326,332,458,464,578,584,590,596,602,608,722,728,842,848] --> Loop 101 * CEs [309,311,315,317,441,443,447,449,561,563,567,569,705,707,711,713,825,827,831,833,1005,1007,1011,1013,1149,1151,1155,1157,1269,1271,1275,1277,1413,1415,1419,1421,1533,1535,1539,1541] --> Loop 102 * CEs [501,507,1209,1215] --> Loop 103 * CEs [503,509,645,647,651,653,1211,1217,1353,1355,1359,1361] --> Loop 104 * CEs [240,242,246,248,372,374,378,380,765,767,771,773,902,927,929,933,935,1046,1071,1073,1077,1079,1473,1475,1479,1481] --> Loop 105 * CEs [489,490,495,496,502,508,549,550,555,556,562,568,1197,1203,1257,1263] --> Loop 106 * CEs [206,212,214,216,218,220,222,224,338,344,346,348,350,352,354,356,470,476,480,482,486,488,491,492,493,494,497,498,499,500,504,505,506,510,511,512,551,552,553,554,557,558,559,560,564,565,566,570,571,572,614,620,622,624,626,628,630,632,633,634,635,636,637,638,639,640,641,642,643,644,646,648,649,650,652,654,655,656,693,694,695,696,697,698,699,700,701,702,703,704,706,708,709,710,712,714,715,716,734,740,742,744,746,748,750,752,908,1052,1190,1196,1198,1199,1200,1201,1202,1204,1205,1206,1207,1208,1210,1212,1213,1214,1216,1218,1219,1220,1258,1259,1260,1261,1262,1264,1265,1266,1267,1268,1270,1272,1273,1274,1276,1278,1279,1280,1334,1340,1341,1342,1343,1344,1345,1346,1347,1348,1349,1350,1351,1352,1354,1356,1357,1358,1360,1362,1363,1364,1401,1402,1403,1404,1405,1406,1407,1408,1409,1410,1411,1412,1414,1416,1417,1418,1420,1422,1423,1424,1454,1460] --> Loop 107 * CEs [217,297,299,303,305,349,429,431,435,437,813,815,819,821,898,900,901,993,995,999,1001,1042,1044,1045,1137,1139,1143,1145,1521,1523,1527,1529] --> Loop 108 * CEs [202,204,208,210,334,336,340,342,466,468,472,474,477,483,610,612,616,618,730,732,736,738,1185,1191] --> Loop 109 * CEs [213,215,219,221,345,347,351,353,479,485,621,623,627,629,741,743,747,749,897,899,903,905,1041,1043,1047,1049,1187,1193,1329,1331,1335,1337,1449,1451,1455,1457] --> Loop 110 * CEs [286,288,292,294,418,420,424,426,465,471,538,540,544,546,682,684,688,690,802,804,808,810,1173,1179] --> Loop 111 * CEs [274,276,280,282,406,408,412,414,526,528,532,534,537,543,670,672,676,678,790,792,796,798,1245,1251] --> Loop 112 * CEs [277,283,285,287,291,293,409,415,417,419,423,425,529,535,539,545,673,679,681,683,687,689,793,799,801,803,807,809,962,968,970,972,973,976,978,979,981,983,987,989,1106,1112,1114,1116,1117,1120,1122,1123,1125,1127,1131,1133,1226,1232,1234,1236,1237,1240,1242,1243,1247,1253,1370,1376,1378,1380,1381,1384,1386,1387,1389,1391,1395,1397,1490,1496,1498,1500,1501,1504,1506,1507,1509,1511,1515,1517] --> Loop 113 * CEs [262,264,268,270,394,396,400,402,514,516,520,522,525,531,658,660,664,666,778,780,784,786,1233,1239] --> Loop 114 * CEs [265,271,273,275,279,281,397,403,405,407,411,413,517,523,527,533,661,667,669,671,675,677,781,787,789,791,795,797,854,860,866,872,878,884,958,960,961,964,966,967,969,971,975,977,1022,1028,1102,1104,1105,1108,1110,1111,1113,1115,1119,1121,1166,1172,1222,1224,1225,1228,1230,1231,1235,1241,1286,1292,1298,1304,1310,1316,1366,1368,1369,1372,1374,1375,1377,1379,1383,1385,1430,1436,1486,1488,1489,1492,1494,1495,1497,1499,1503,1505,1550,1556] --> Loop 115 * CEs [166,168,172,174,178,180,184,186,190,192,196,198,322,324,328,330,454,456,460,462,513,519,574,576,580,582,586,588,592,594,598,600,604,606,718,720,724,726,838,840,844,846,1221,1227] --> Loop 116 * CEs [169,175,181,187,193,199,261,263,267,269,325,331,393,395,399,401,457,463,515,521,577,583,589,595,601,607,657,659,663,665,721,727,777,779,783,785,841,847,850,852,853,856,858,859,862,864,865,868,870,871,874,876,877,880,882,883,957,959,963,965,1018,1020,1021,1024,1026,1027,1101,1103,1107,1109,1162,1164,1165,1168,1170,1171,1223,1229,1282,1284,1285,1288,1290,1291,1294,1296,1297,1300,1302,1303,1306,1308,1309,1312,1314,1315,1365,1367,1371,1373,1426,1428,1429,1432,1434,1435,1485,1487,1491,1493,1546,1548,1549,1552,1554,1555] --> Loop 117 * CEs [165,167,171,173,177,179,183,185,189,191,195,197,321,323,327,329,453,455,459,461,573,575,579,581,585,587,591,593,597,599,603,605,717,719,723,725,837,839,843,845,849,851,855,857,861,863,867,869,873,875,879,881,1017,1019,1023,1025,1161,1163,1167,1169,1281,1283,1287,1289,1293,1295,1299,1301,1305,1307,1311,1313,1425,1427,1431,1433,1545,1547,1551,1553] --> Loop 118 * CEs [223,355,481,487,625,631,745,751,890,896,904,906,907,914,1034,1040,1048,1050,1051,1058,1178,1184,1186,1188,1189,1192,1194,1195,1322,1328,1330,1332,1333,1336,1338,1339,1442,1448,1450,1452,1453,1456,1458,1459] --> Loop 119 * CEs [205,211,227,337,343,359,469,475,613,619,733,739,886,888,889,892,894,895,910,912,913,986,992,1030,1032,1033,1036,1038,1039,1054,1056,1057,1130,1136,1174,1176,1177,1180,1182,1183,1250,1256,1318,1320,1321,1324,1326,1327,1394,1400,1438,1440,1441,1444,1446,1447,1514,1520] --> Loop 120 * CEs [258,259,260,390,391,392,951,952,953,954,955,956,1095,1096,1097,1098,1099,1100] --> Loop 121 * CEs [950,1094] --> Loop 122 * CEs [257,389,944,946,948,949,1088,1090,1092,1093] --> Loop 123 * CEs [254,255,256,386,387,388,940,942,943,945,947,1084,1086,1087,1089,1091] --> Loop 124 * CEs [228,229,230,231,232,233,234,235,236,237,238,239,241,243,244,245,247,249,250,251,252,253,298,300,301,302,304,306,307,308,310,312,313,314,316,318,319,320,360,361,362,363,364,365,366,367,368,369,370,371,373,375,376,377,379,381,382,383,384,385,430,432,433,434,436,438,439,440,442,444,445,446,448,450,451,452,753,754,755,756,757,758,759,760,761,762,763,764,766,768,769,770,772,774,775,776,814,816,817,818,820,822,823,824,826,828,829,830,832,834,835,836,915,916,917,918,919,920,921,922,923,924,925,926,928,930,931,932,934,936,937,938,939,941,994,996,997,998,1000,1002,1003,1004,1006,1008,1009,1010,1012,1014,1015,1016,1059,1060,1061,1062,1063,1064,1065,1066,1067,1068,1069,1070,1072,1074,1075,1076,1078,1080,1081,1082,1083,1085,1138,1140,1141,1142,1144,1146,1147,1148,1150,1152,1153,1154,1156,1158,1159,1160,1461,1462,1463,1464,1465,1466,1467,1468,1469,1470,1471,1472,1474,1476,1477,1478,1480,1482,1483,1484,1522,1524,1525,1526,1528,1530,1531,1532,1534,1536,1537,1538,1540,1542,1543,1544] --> Loop 125 * CEs [201,203,207,209,225,226,289,295,333,335,339,341,357,358,421,427,467,473,541,547,609,611,615,617,685,691,729,731,735,737,805,811,885,887,891,893,909,911,974,980,982,984,985,988,990,991,1029,1031,1035,1037,1053,1055,1118,1124,1126,1128,1129,1132,1134,1135,1175,1181,1238,1244,1246,1248,1249,1252,1254,1255,1317,1319,1323,1325,1382,1388,1390,1392,1393,1396,1398,1399,1437,1439,1443,1445,1502,1508,1510,1512,1513,1516,1518,1519] --> Loop 126 ### Ranking functions of CR fun(V1,V,Out) #### Partial ranking functions of CR fun(V1,V,Out) ### Specialization of cost equations start/5 * CE 2 is refined into CE [1557] * CE 1 is refined into CE [1558] * CE 3 is refined into CE [1559,1560,1561,1562,1563] * CE 4 is refined into CE [1564,1565,1566,1567,1568,1569,1570,1571,1572,1573,1574] * CE 5 is refined into CE [1575,1576,1577,1578,1579,1580,1581,1582,1583,1584,1585] * CE 6 is refined into CE [1586,1587,1588,1589,1590] * CE 7 is refined into CE [1591,1592,1593,1594,1595,1596,1597,1598] * CE 8 is refined into CE [1599,1600,1601,1602,1603,1604,1605,1606] * CE 9 is refined into CE [1607,1608,1609,1610,1611,1612,1613,1614,1615,1616,1617,1618,1619,1620,1621,1622,1623,1624,1625,1626,1627,1628,1629,1630,1631] * CE 10 is refined into CE [1632,1633] * CE 11 is refined into CE [1634,1635] * CE 12 is refined into CE [1636,1637,1638,1639,1640,1641,1642,1643,1644,1645,1646,1647,1648,1649,1650,1651,1652,1653,1654,1655,1656,1657,1658,1659] * CE 13 is refined into CE [1660,1661,1662,1663] * CE 14 is refined into CE [1664,1665,1666,1667,1668] * CE 15 is refined into CE [1669,1670,1671,1672,1673,1674,1675,1676] * CE 16 is refined into CE [1677,1678,1679,1680] * CE 17 is refined into CE [1681,1682] * CE 18 is refined into CE [1683,1684,1685,1686,1687,1688] * CE 19 is refined into CE [1689,1690,1691,1692,1693] * CE 20 is refined into CE [1694,1695,1696,1697] ### Cost equations --> "Loop" of start/5 * CEs [1587,1588,1605,1652,1653] --> Loop 127 * CEs [1577,1578,1579,1606,1651] --> Loop 128 * CEs [1557] --> Loop 129 * CEs [1560,1561,1597] --> Loop 130 * CEs [1566,1567,1568,1598] --> Loop 131 * CEs [1593,1594] --> Loop 132 * CEs [1559,1562,1563,1564,1565,1569,1570,1571,1572,1573,1574,1591,1592,1595,1596] --> Loop 133 * CEs [1608,1609,1610,1636,1637,1639,1640,1644,1645,1646,1647,1660,1669,1684,1685,1689,1695] --> Loop 134 * CEs [1601,1602,1648,1686] --> Loop 135 * CEs [1586,1599,1600,1638,1641,1642,1643,1683] --> Loop 136 * CEs [1558,1575,1576,1580,1581,1582,1583,1584,1585,1589,1590,1603,1604,1607,1611,1612,1613,1614,1615,1616,1617,1618,1619,1620,1621,1622,1623,1624,1625,1626,1627,1628,1629,1630,1631,1632,1633,1634,1635,1649,1650,1654,1655,1656,1657,1658,1659,1661,1662,1663,1664,1665,1666,1667,1668,1670,1671,1672,1673,1674,1675,1676,1677,1678,1679,1680,1681,1682,1687,1688,1690,1691,1692,1693,1694,1696,1697] --> Loop 137 ### Ranking functions of CR start(V1,V,V14,V12,V23) #### Partial ranking functions of CR start(V1,V,V14,V12,V23) Computing Bounds ===================================== #### Cost of chains of ge(V1,V,Out): * Chain [[34],37]: 0 with precondition: [Out=1,V1>=1,V>=V1+1] * Chain [[34],36]: 0 with precondition: [Out=2,V>=1,V1>=V] * Chain [[34],35]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [37]: 0 with precondition: [V1=0,Out=1,V>=1] * Chain [36]: 0 with precondition: [V=0,Out=2,V1>=0] * Chain [35]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of take(V1,V,V14,Out): * Chain [[39],42]: 0 with precondition: [V=0,V1>=1,Out>=0,V14>=Out+V1+1] * Chain [[39],40]: 0 with precondition: [V=0,Out=0,V1>=1,V14>=1] * Chain [42]: 0 with precondition: [V1=0,V=0,Out>=0,V14>=Out+1] * Chain [41]: 0 with precondition: [V1=0,V=Out+2,V>=2,V14>=0] * Chain [40]: 0 with precondition: [Out=0,V1>=0,V>=0,V14>=0] * Chain [38,40]: 0 with precondition: [Out=0,V1>=1,V>=2,V14>=0] #### Cost of chains of helpa(V1,V,V14,V12,Out): * Chain [[43,44],49]: 0 with precondition: [V1>=1,V14>=0,V12>=0,Out>=1,V>=V1+1] * Chain [49]: 0 with precondition: [Out=0,V1>=0,V>=0,V14>=0,V12>=0] * Chain [48]: 0 with precondition: [V=0,Out=0,V1>=0,V14>=0,V12>=0] * Chain [47,[43,44],49]: 0 with precondition: [V1=0,V14=0,V>=2,V12>=1,Out>=2] * Chain [47,49]: 0 with precondition: [V1=0,V14=0,V>=1,Out>=1,V12>=Out] * Chain [46,[43,44],49]: 0 with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=2] * Chain [46,49]: 0 with precondition: [V1=0,Out=1,V>=1,V14>=0,V12>=0] * Chain [45,[43,44],49]: 0 with precondition: [V1=0,V>=2,V14>=2,V12>=0,Out>=V14] * Chain [45,49]: 0 with precondition: [V1=0,V14=Out+1,V>=1,V14>=2,V12>=0] #### Cost of chains of length(V1,Out): * Chain [[50],51]: 0 with precondition: [Out>=1,V1>=Out] * Chain [51]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of plus(V1,V,Out): * Chain [[52],54]: 0 with precondition: [V+V1=Out,V1>=0,V>=1] * Chain [[52],53]: 0 with precondition: [V1>=0,Out>=1,V>=Out] * Chain [54]: 0 with precondition: [V=0,V1=Out,V1>=0] * Chain [53]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of app(V1,V,Out): * Chain [62]: 0 with precondition: [V1=0,Out>=1,V>=Out] * Chain [61]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [60]: 0 with precondition: [Out=1,V1>=0,V>=1] * Chain [59]: 0 with precondition: [Out=1,V1>=1,V>=0] * Chain [58]: 0 with precondition: [V1=Out+1,V1>=2,V>=0] * Chain [57]: 0 with precondition: [V1>=0,V>=2,Out>=2] * Chain [56]: 0 with precondition: [V1>=1,V>=1,Out>=2] * Chain [55]: 0 with precondition: [V1>=2,V>=0,Out>=2] #### Cost of chains of fun7(V1,V,V14,Out): * Chain [[64],66]: 1*it(64)+1 Such that:it(64) =< Out with precondition: [V=0,V1+1=Out,V1>=1,V14>=V1+1] * Chain [[64],65]: 1*it(64)+1 Such that:it(64) =< Out with precondition: [V=0,Out>=1,V1>=Out,V14>=Out] * Chain [66]: 1 with precondition: [V1=0,V=0,Out=1,V14>=1] * Chain [65]: 1 with precondition: [Out=0,V1>=0,V>=0,V14>=0] * Chain [63,65]: 2 with precondition: [Out=1,V1>=1,V>=2,V14>=0] #### Cost of chains of fun5(V1,V,Out): * Chain [[67],69]: 1*it(67)+1 Such that:it(67) =< Out with precondition: [V1+1=Out,V1>=1,V>=V1+1] * Chain [[67],68]: 1*it(67)+1 Such that:it(67) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [69]: 1 with precondition: [V1=0,Out=1,V>=1] * Chain [68]: 1 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun1(V1,V,V14,V12,Out): * Chain [[88,89,90],85]: 12*it(88)+1*s(5)+1*s(6)+3 Such that:aux(3) =< V aux(7) =< -V1+V it(88) =< aux(7) aux(4) =< aux(3) s(5) =< it(88)*aux(3) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,Out>=4,V>=V1+1] * Chain [[88,89,90],81]: 12*it(88)+1*s(5)+1*s(6)+3*s(7)+5 Such that:aux(9) =< -V1+V aux(10) =< V s(7) =< aux(10) it(88) =< aux(9) aux(4) =< aux(10) s(5) =< it(88)*aux(10) s(6) =< it(88)*aux(4) with precondition: [V14=0,V1>=1,V12>=1,Out>=8,V>=V1+2] * Chain [[88,89,90],80]: 12*it(88)+1*s(5)+1*s(6)+2*s(10)+5 Such that:aux(5) =< -V1+V aux(6) =< -V1+V12 aux(3) =< V aux(11) =< V12 s(10) =< aux(11) it(88) =< aux(5) it(88) =< aux(6) aux(4) =< aux(3) s(5) =< it(88)*aux(3) s(6) =< it(88)*aux(4) with precondition: [V14=0,V1>=1,Out>=2*V1+10,V>=V1+2,V12>=V1+2] * Chain [[88,89,90],79]: 12*it(88)+1*s(5)+1*s(6)+1*s(12)+1*s(13)+5 Such that:s(12) =< V12 aux(12) =< -V1+V aux(13) =< V s(13) =< aux(13) it(88) =< aux(12) aux(4) =< aux(13) s(5) =< it(88)*aux(13) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,Out>=7,V>=V1+2] * Chain [[88,89,90],78]: 12*it(88)+1*s(5)+1*s(6)+4*s(14)+5 Such that:aux(16) =< -V1+V aux(17) =< V s(14) =< aux(17) it(88) =< aux(16) aux(4) =< aux(17) s(5) =< it(88)*aux(17) s(6) =< it(88)*aux(4) with precondition: [V14=0,V1>=1,V12>=1,V>=V1+2,Out>=V1+9] * Chain [[88,89,90],77]: 12*it(88)+1*s(5)+1*s(6)+5 Such that:aux(3) =< V aux(18) =< -V1+V it(88) =< aux(18) aux(4) =< aux(3) s(5) =< it(88)*aux(3) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,Out>=6,V>=V1+2] * Chain [[88,89,90],76]: 12*it(88)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(19) =< -V1+V it(88) =< aux(19) aux(4) =< aux(3) s(5) =< it(88)*aux(3) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=2,V12>=0,Out>=7,V>=V1+2] * Chain [[88,89,90],75]: 12*it(88)+1*s(5)+1*s(6)+1*s(18)+6 Such that:aux(20) =< -V1+V aux(21) =< V s(18) =< aux(21) it(88) =< aux(20) aux(4) =< aux(21) s(5) =< it(88)*aux(21) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=2,V12>=0,V>=V1+2,Out>=V1+9] * Chain [[88,89,90],74]: 12*it(88)+1*s(5)+1*s(6)+1*s(19)+5 Such that:aux(22) =< -V1+V aux(23) =< V s(19) =< aux(23) it(88) =< aux(22) aux(4) =< aux(23) s(5) =< it(88)*aux(23) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,V>=V1+2,Out>=V1+8] * Chain [[88,89,90],73]: 12*it(88)+1*s(5)+1*s(6)+2*s(20)+2 Such that:aux(25) =< -V1+V aux(26) =< V s(20) =< aux(26) it(88) =< aux(25) aux(4) =< aux(26) s(5) =< it(88)*aux(26) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,V>=V1+2,Out>=V1+6] * Chain [[88,89,90],72]: 12*it(88)+1*s(5)+1*s(6)+2*s(22)+2 Such that:aux(27) =< -V1+V aux(28) =< V s(22) =< aux(28) it(88) =< aux(27) aux(4) =< aux(28) s(5) =< it(88)*aux(28) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,Out>=5,V>=V1+1] * Chain [[88,89,90],71]: 12*it(88)+1*s(5)+1*s(6)+2*s(24)+3 Such that:aux(30) =< -V1+V aux(31) =< V s(24) =< aux(31) it(88) =< aux(30) aux(4) =< aux(31) s(5) =< it(88)*aux(31) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=0,V12>=0,V>=V1+1,Out+3*V1>=3*V+2] * Chain [[88,89,90],70]: 12*it(88)+1*s(5)+1*s(6)+1*s(26)+6 Such that:aux(32) =< -V1+V aux(33) =< V s(26) =< aux(33) it(88) =< aux(32) aux(4) =< aux(33) s(5) =< it(88)*aux(33) s(6) =< it(88)*aux(4) with precondition: [V1>=1,V14>=2,V12>=0,Out>=8,V>=V1+2] * Chain [92,[88,89,90],85]: 12*it(88)+1*s(5)+1*s(6)+7 Such that:aux(34) =< V it(88) =< aux(34) aux(4) =< aux(34) s(5) =< it(88)*aux(34) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=7] * Chain [92,[88,89,90],81]: 15*it(88)+1*s(5)+1*s(6)+9 Such that:aux(35) =< V it(88) =< aux(35) aux(4) =< aux(35) s(5) =< it(88)*aux(35) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=1,Out>=11] * Chain [92,[88,89,90],80]: 12*it(88)+1*s(5)+1*s(6)+2*s(10)+9 Such that:aux(36) =< V aux(37) =< V12 s(10) =< aux(37) it(88) =< aux(36) it(88) =< aux(37) aux(4) =< aux(36) s(5) =< it(88)*aux(36) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=3,Out>=15] * Chain [92,[88,89,90],79]: 13*it(88)+1*s(5)+1*s(6)+1*s(12)+9 Such that:s(12) =< V12 aux(38) =< V it(88) =< aux(38) aux(4) =< aux(38) s(5) =< it(88)*aux(38) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=10] * Chain [92,[88,89,90],78]: 16*it(88)+1*s(5)+1*s(6)+9 Such that:aux(39) =< V it(88) =< aux(39) aux(4) =< aux(39) s(5) =< it(88)*aux(39) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=1,Out>=13] * Chain [92,[88,89,90],77]: 12*it(88)+1*s(5)+1*s(6)+9 Such that:aux(40) =< V it(88) =< aux(40) aux(4) =< aux(40) s(5) =< it(88)*aux(40) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=9] * Chain [92,[88,89,90],76]: 12*it(88)+1*s(5)+1*s(6)+10 Such that:aux(41) =< V it(88) =< aux(41) aux(4) =< aux(41) s(5) =< it(88)*aux(41) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=10] * Chain [92,[88,89,90],75]: 13*it(88)+1*s(5)+1*s(6)+10 Such that:aux(42) =< V it(88) =< aux(42) aux(4) =< aux(42) s(5) =< it(88)*aux(42) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=13] * Chain [92,[88,89,90],74]: 13*it(88)+1*s(5)+1*s(6)+9 Such that:aux(43) =< V it(88) =< aux(43) aux(4) =< aux(43) s(5) =< it(88)*aux(43) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=12] * Chain [92,[88,89,90],73]: 14*it(88)+1*s(5)+1*s(6)+6 Such that:aux(44) =< V it(88) =< aux(44) aux(4) =< aux(44) s(5) =< it(88)*aux(44) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=10] * Chain [92,[88,89,90],72]: 14*it(88)+1*s(5)+1*s(6)+6 Such that:aux(45) =< V it(88) =< aux(45) aux(4) =< aux(45) s(5) =< it(88)*aux(45) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=8] * Chain [92,[88,89,90],71]: 14*it(88)+1*s(5)+1*s(6)+7 Such that:aux(46) =< V it(88) =< aux(46) aux(4) =< aux(46) s(5) =< it(88)*aux(46) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=3*V+2] * Chain [92,[88,89,90],70]: 13*it(88)+1*s(5)+1*s(6)+10 Such that:aux(47) =< V it(88) =< aux(47) aux(4) =< aux(47) s(5) =< it(88)*aux(47) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=11] * Chain [92,85]: 7 with precondition: [V1=0,Out=4,V>=1,V14>=0,V12>=0] * Chain [92,81]: 1*s(7)+2*s(8)+9 Such that:aux(8) =< 1 s(7) =< 2 s(8) =< aux(8) with precondition: [V1=0,V14=0,Out=8,V>=2,V12>=1] * Chain [92,80]: 2*s(10)+9 Such that:aux(11) =< 2 s(10) =< aux(11) with precondition: [V1=0,V14=0,Out=10,V>=2,V12>=2] * Chain [92,79]: 1*s(12)+1*s(13)+9 Such that:s(13) =< 1 s(12) =< V12 with precondition: [V1=0,Out=7,V>=2,V14>=0,V12>=0] * Chain [92,78]: 2*s(14)+2*s(15)+9 Such that:aux(14) =< 1 aux(15) =< 2 s(15) =< aux(14) s(14) =< aux(15) with precondition: [V1=0,V14=0,Out=9,V>=2,V12>=1] * Chain [92,77]: 9 with precondition: [V1=0,Out=6,V>=2,V14>=0,V12>=0] * Chain [92,76]: 10 with precondition: [V1=0,Out=7,V>=2,V14>=2,V12>=0] * Chain [92,75]: 1*s(18)+10 Such that:s(18) =< 2 with precondition: [V1=0,Out=9,V>=2,V14>=2,V12>=0] * Chain [92,74]: 1*s(19)+9 Such that:s(19) =< 2 with precondition: [V1=0,Out=8,V>=2,V14>=0,V12>=0] * Chain [92,73]: 2*s(20)+6 Such that:aux(24) =< 2 s(20) =< aux(24) with precondition: [V1=0,Out=6,V>=2,V14>=0,V12>=0] * Chain [92,72]: 1*s(22)+1*s(23)+6 Such that:s(23) =< 1 s(22) =< V with precondition: [V1=0,Out=5,V>=1,V14>=0,V12>=0] * Chain [92,71]: 2*s(24)+7 Such that:aux(29) =< 1 s(24) =< aux(29) with precondition: [V1=0,V=1,Out=5,V14>=0,V12>=0] * Chain [92,70]: 1*s(26)+10 Such that:s(26) =< 1 with precondition: [V1=0,Out=8,V>=2,V14>=2,V12>=0] * Chain [91,[88,89,90],85]: 12*it(88)+1*s(5)+1*s(6)+7 Such that:aux(48) =< V it(88) =< aux(48) aux(4) =< aux(48) s(5) =< it(88)*aux(48) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=8] * Chain [91,[88,89,90],81]: 15*it(88)+1*s(5)+1*s(6)+9 Such that:aux(49) =< V it(88) =< aux(49) aux(4) =< aux(49) s(5) =< it(88)*aux(49) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=1,Out>=12] * Chain [91,[88,89,90],80]: 12*it(88)+1*s(5)+1*s(6)+2*s(10)+9 Such that:aux(50) =< V aux(51) =< V12 s(10) =< aux(51) it(88) =< aux(50) it(88) =< aux(51) aux(4) =< aux(50) s(5) =< it(88)*aux(50) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=3,Out>=16] * Chain [91,[88,89,90],79]: 13*it(88)+1*s(5)+1*s(6)+1*s(12)+9 Such that:s(12) =< V12 aux(52) =< V it(88) =< aux(52) aux(4) =< aux(52) s(5) =< it(88)*aux(52) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=11] * Chain [91,[88,89,90],78]: 16*it(88)+1*s(5)+1*s(6)+9 Such that:aux(53) =< V it(88) =< aux(53) aux(4) =< aux(53) s(5) =< it(88)*aux(53) s(6) =< it(88)*aux(4) with precondition: [V1=0,V14=0,V>=3,V12>=1,Out>=14] * Chain [91,[88,89,90],77]: 12*it(88)+1*s(5)+1*s(6)+9 Such that:aux(54) =< V it(88) =< aux(54) aux(4) =< aux(54) s(5) =< it(88)*aux(54) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=10] * Chain [91,[88,89,90],76]: 12*it(88)+1*s(5)+1*s(6)+10 Such that:aux(55) =< V it(88) =< aux(55) aux(4) =< aux(55) s(5) =< it(88)*aux(55) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=11] * Chain [91,[88,89,90],75]: 13*it(88)+1*s(5)+1*s(6)+10 Such that:aux(56) =< V it(88) =< aux(56) aux(4) =< aux(56) s(5) =< it(88)*aux(56) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=14] * Chain [91,[88,89,90],74]: 13*it(88)+1*s(5)+1*s(6)+9 Such that:aux(57) =< V it(88) =< aux(57) aux(4) =< aux(57) s(5) =< it(88)*aux(57) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=13] * Chain [91,[88,89,90],73]: 14*it(88)+1*s(5)+1*s(6)+6 Such that:aux(58) =< V it(88) =< aux(58) aux(4) =< aux(58) s(5) =< it(88)*aux(58) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=0,V12>=0,Out>=11] * Chain [91,[88,89,90],72]: 14*it(88)+1*s(5)+1*s(6)+6 Such that:aux(59) =< V it(88) =< aux(59) aux(4) =< aux(59) s(5) =< it(88)*aux(59) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=9] * Chain [91,[88,89,90],71]: 14*it(88)+1*s(5)+1*s(6)+7 Such that:aux(60) =< V it(88) =< aux(60) aux(4) =< aux(60) s(5) =< it(88)*aux(60) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=2,V14>=0,V12>=0,Out>=3*V+3] * Chain [91,[88,89,90],70]: 13*it(88)+1*s(5)+1*s(6)+10 Such that:aux(61) =< V it(88) =< aux(61) aux(4) =< aux(61) s(5) =< it(88)*aux(61) s(6) =< it(88)*aux(4) with precondition: [V1=0,V>=3,V14>=2,V12>=0,Out>=12] * Chain [91,85]: 7 with precondition: [V1=0,Out=5,V>=1,V14>=0,V12>=0] * Chain [91,81]: 1*s(7)+2*s(8)+9 Such that:aux(8) =< 1 s(7) =< 2 s(8) =< aux(8) with precondition: [V1=0,V14=0,Out=9,V>=2,V12>=1] * Chain [91,80]: 2*s(10)+9 Such that:aux(11) =< 2 s(10) =< aux(11) with precondition: [V1=0,V14=0,Out=11,V>=2,V12>=2] * Chain [91,79]: 1*s(12)+1*s(13)+9 Such that:s(13) =< 1 s(12) =< V12 with precondition: [V1=0,Out=8,V>=2,V14>=0,V12>=0] * Chain [91,78]: 2*s(14)+2*s(15)+9 Such that:aux(14) =< 1 aux(15) =< 2 s(15) =< aux(14) s(14) =< aux(15) with precondition: [V1=0,V14=0,Out=10,V>=2,V12>=1] * Chain [91,77]: 9 with precondition: [V1=0,Out=7,V>=2,V14>=0,V12>=0] * Chain [91,76]: 10 with precondition: [V1=0,Out=8,V>=2,V14>=2,V12>=0] * Chain [91,75]: 1*s(18)+10 Such that:s(18) =< 2 with precondition: [V1=0,Out=10,V>=2,V14>=2,V12>=0] * Chain [91,74]: 1*s(19)+9 Such that:s(19) =< 2 with precondition: [V1=0,Out=9,V>=2,V14>=0,V12>=0] * Chain [91,73]: 2*s(20)+6 Such that:aux(24) =< 2 s(20) =< aux(24) with precondition: [V1=0,Out=7,V>=2,V14>=0,V12>=0] * Chain [91,72]: 1*s(22)+1*s(23)+6 Such that:s(23) =< 1 s(22) =< V with precondition: [V1=0,Out=6,V>=1,V14>=0,V12>=0] * Chain [91,71]: 2*s(24)+7 Such that:aux(29) =< 1 s(24) =< aux(29) with precondition: [V1=0,V=1,Out=6,V14>=0,V12>=0] * Chain [91,70]: 1*s(26)+10 Such that:s(26) =< 1 with precondition: [V1=0,Out=9,V>=2,V14>=2,V12>=0] * Chain [87]: 5 with precondition: [V1=0,Out=4,V>=1,V14>=0,V12>=0] * Chain [86]: 5 with precondition: [V1=0,V14=0,Out=5,V>=1,V12>=1] * Chain [85]: 3 with precondition: [Out=1,V1>=0,V>=0,V14>=0,V12>=0] * Chain [84]: 2 with precondition: [V1=0,Out=2,V>=1,V14>=0,V12>=0] * Chain [83]: 5 with precondition: [V1=0,Out=3,V>=1,V14>=0,V12>=0] * Chain [82]: 3 with precondition: [V=0,Out=1,V1>=0,V14>=0,V12>=0] * Chain [81]: 1*s(7)+2*s(8)+5 Such that:aux(8) =< V1 s(7) =< V1+1 s(8) =< aux(8) with precondition: [V14=0,V12>=1,Out>=5,V>=V1+1,2*V1+3>=Out,V1+V12+3>=Out] * Chain [80]: 2*s(10)+5 Such that:aux(11) =< V1+1 s(10) =< aux(11) with precondition: [V14=0,2*V1+5=Out,V1>=1,V>=V1+1,V12>=V1+1] * Chain [79]: 1*s(12)+1*s(13)+5 Such that:s(13) =< V1 s(12) =< V12 with precondition: [V14>=0,V12>=0,Out>=4,V>=V1+1,V1+3>=Out] * Chain [78]: 2*s(14)+2*s(15)+5 Such that:aux(14) =< V1 aux(15) =< V1+1 s(15) =< aux(14) s(14) =< aux(15) with precondition: [V14=0,V>=V1+1,Out>=V1+5,2*V1+4>=Out,V1+V12+4>=Out] * Chain [77]: 5 with precondition: [Out=3,V1>=1,V14>=0,V12>=0,V>=V1+1] * Chain [76]: 6 with precondition: [Out=4,V1>=1,V14>=2,V12>=0,V>=V1+1] * Chain [75]: 1*s(18)+6 Such that:s(18) =< V1+1 with precondition: [V1+5=Out,V1>=1,V14>=2,V12>=0,V>=V1+1] * Chain [74]: 1*s(19)+5 Such that:s(19) =< V1+1 with precondition: [V1+4=Out,V1>=1,V14>=0,V12>=0,V>=V1+1] * Chain [73]: 2*s(20)+2 Such that:aux(24) =< V1+1 s(20) =< aux(24) with precondition: [V1+2=Out,V1>=1,V14>=0,V12>=0,V>=V1+1] * Chain [72]: 1*s(22)+1*s(23)+2 Such that:s(23) =< V1 s(22) =< V with precondition: [V14>=0,V12>=0,Out>=2,V1+1>=Out,V+1>=Out] * Chain [71]: 2*s(24)+3 Such that:aux(29) =< V s(24) =< aux(29) with precondition: [V14>=0,V12>=0,Out>=2,V1>=V,V+1>=Out] * Chain [70]: 1*s(26)+6 Such that:s(26) =< V1 with precondition: [V14>=2,V12>=0,Out>=5,V>=V1+1,V1+4>=Out] #### Cost of chains of fun2(V1,V,Out): * Chain [[93],94]: 1*it(93)+1 Such that:it(93) =< Out with precondition: [V1>=0,Out>=1,V>=Out] * Chain [94]: 1 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun3(V1,Out): * Chain [[95],96]: 1*it(95)+1 Such that:it(95) =< V1 with precondition: [Out>=1,V1>=Out] * Chain [96]: 1 with precondition: [Out=0,V1>=0] #### Cost of chains of fun(V1,V,Out): * Chain [126]: 84*s(300)+108*s(302)+4*s(328)+8*s(336)+10 Such that:aux(90) =< 1 aux(91) =< V1 aux(92) =< V1+V aux(93) =< V s(328) =< aux(91) s(336) =< aux(92) s(300) =< aux(93) s(302) =< aux(90) with precondition: [V1>=0,Out>=6,2*V+4>=Out] * Chain [125]: 336*s(472)+288*s(473)+19152*s(474)+1440*s(477)+1440*s(478)+72*s(490)+28 Such that:aux(214) =< 1 aux(215) =< 2 aux(216) =< V1 aux(217) =< V s(472) =< aux(214) s(473) =< aux(215) s(490) =< aux(216) s(474) =< aux(217) s(476) =< aux(217) s(477) =< s(474)*aux(217) s(478) =< s(474)*s(476) with precondition: [V1>=0,V>=2,Out>=8] * Chain [124]: 8*s(1740)+16*s(1742)+22 Such that:aux(218) =< 2 aux(219) =< V s(1740) =< aux(219) s(1742) =< aux(218) with precondition: [V1=0,V>=2,Out>=12,V+11>=Out] * Chain [123]: 16*s(1765)+12*s(1766)+22 Such that:aux(222) =< 2 aux(223) =< V s(1766) =< aux(223) s(1765) =< aux(222) with precondition: [V1=0,V>=2,Out>=13,2*V+11>=Out] * Chain [122]: 4*s(1793)+4*s(1794)+12 Such that:aux(226) =< 2 aux(227) =< V s(1794) =< aux(227) s(1793) =< aux(226) with precondition: [V1=0,V>=2,Out>=14,2*V+12>=Out] * Chain [121]: 1632*s(1802)+108*s(1804)+108*s(1805)+12 Such that:aux(246) =< V s(1802) =< aux(246) s(1803) =< aux(246) s(1804) =< s(1802)*aux(246) s(1805) =< s(1802)*s(1803) with precondition: [V1=0,V>=3,Out>=12] * Chain [120]: 92*s(1992)+120*s(1994)+8*s(2010)+8*s(2018)+10 Such that:aux(281) =< 1 aux(282) =< V1 aux(283) =< V1+V aux(284) =< V s(2010) =< aux(282) s(2018) =< aux(283) s(1992) =< aux(284) s(1994) =< aux(281) with precondition: [V1>=0,Out>=7,2*V+5>=Out] * Chain [119]: 78*s(2181)+126*s(2183)+64*s(2184)+10*s(2193)+10*s(2205)+12 Such that:aux(313) =< 1 aux(314) =< 2 aux(315) =< V1 aux(316) =< V1+V aux(317) =< V s(2193) =< aux(315) s(2205) =< aux(316) s(2181) =< aux(317) s(2183) =< aux(313) s(2184) =< aux(314) with precondition: [V1>=0,Out>=8,2*V+6>=Out] * Chain [118]: 6 with precondition: [Out=2,V1>=0,V>=0] * Chain [117]: 80*s(2426)+6 Such that:aux(318) =< V s(2426) =< aux(318) with precondition: [V1>=0,Out>=3,V+2>=Out] * Chain [116]: 40*s(2506)+6 Such that:aux(319) =< V1 s(2506) =< aux(319) with precondition: [V>=0,Out>=3,V1+2>=Out] * Chain [115]: 80*s(2546)+8 Such that:aux(340) =< V s(2546) =< aux(340) with precondition: [V1>=0,Out>=4,2*V+2>=Out] * Chain [114]: 20*s(2626)+8 Such that:aux(341) =< V1 s(2626) =< aux(341) with precondition: [V>=0,Out>=4,V1+3>=Out] * Chain [113]: 60*s(2646)+10 Such that:aux(352) =< V s(2646) =< aux(352) with precondition: [V1>=0,Out>=5,2*V+3>=Out] * Chain [112]: 20*s(2706)+10 Such that:aux(353) =< V1 s(2706) =< aux(353) with precondition: [V>=0,Out>=5,V1+4>=Out] * Chain [111]: 24*s(2726)+12*s(2736)+10 Such that:aux(354) =< 1 aux(355) =< V1 s(2726) =< aux(355) s(2736) =< aux(354) with precondition: [V>=0,Out>=6,V1+5>=Out] * Chain [110]: 24*s(2759)+108*s(2761)+72*s(2762)+4*s(2799)+8*s(2809)+12 Such that:aux(356) =< 1 aux(357) =< 2 aux(358) =< V1 aux(359) =< V1+V aux(360) =< V s(2799) =< aux(358) s(2809) =< aux(359) s(2759) =< aux(360) s(2761) =< aux(356) s(2762) =< aux(357) with precondition: [Out=7,V1>=0,V>=1] * Chain [109]: 12*s(2938)+72*s(2940)+28*s(2941)+8*s(2990)+4*s(2996)+12 Such that:aux(365) =< 1 aux(366) =< 2 aux(367) =< V1 aux(368) =< V1+V aux(369) =< V s(2941) =< aux(367) s(2996) =< aux(368) s(2938) =< aux(369) s(2940) =< aux(365) s(2990) =< aux(366) with precondition: [V>=0,Out>=7,V1+6>=Out] * Chain [108]: 40*s(3039)+48*s(3041)+64*s(3042)+13 Such that:aux(378) =< 1 aux(379) =< 2 aux(380) =< V s(3041) =< aux(378) s(3039) =< aux(380) s(3042) =< aux(379) with precondition: [V1>=0,Out>=8,V+7>=Out] * Chain [107]: 344*s(3182)+348*s(3184)+4766*s(3186)+270*s(3196)+360*s(3323)+360*s(3324)+6250*s(3472)+480*s(3529)+480*s(3530)+28 Such that:aux(467) =< 1 aux(468) =< 2 aux(469) =< V1 aux(470) =< V1+V aux(471) =< V s(3184) =< aux(467) s(3196) =< aux(468) s(3186) =< aux(469) s(3472) =< aux(470) s(3182) =< aux(471) s(3322) =< aux(469) s(3323) =< s(3186)*aux(469) s(3324) =< s(3186)*s(3322) s(3528) =< aux(470) s(3529) =< s(3472)*aux(470) s(3530) =< s(3472)*s(3528) with precondition: [V1>=1,V>=1,Out>=8] * Chain [106]: 30*s(4282)+26*s(4283)+24*s(4284)+1568*s(4285)+120*s(4287)+120*s(4288)+28 Such that:aux(474) =< 1 aux(475) =< 2 aux(476) =< V1 aux(477) =< V s(4282) =< aux(474) s(4283) =< aux(475) s(4285) =< aux(476) s(4284) =< aux(477) s(4286) =< aux(476) s(4287) =< s(4285)*aux(476) s(4288) =< s(4285)*s(4286) with precondition: [V1>=2,V>=0,Out>=8] * Chain [105]: 6*s(4379)+6*s(4381)+4*s(4382)+28 Such that:aux(480) =< 1 aux(481) =< 2 aux(482) =< V s(4379) =< aux(482) s(4381) =< aux(480) s(4382) =< aux(481) with precondition: [V1>=0,Out>=9,2*V+7>=Out] * Chain [104]: 28 with precondition: [Out=10,V1>=1,V>=1] * Chain [103]: 28 with precondition: [Out=10,V1>=2,V>=0] * Chain [102]: 93 with precondition: [Out=11,V1>=2,V>=0] * Chain [101]: 20*s(4432)+20*s(4433)+6 Such that:aux(484) =< V1 aux(485) =< V s(4433) =< aux(484) s(4432) =< aux(485) with precondition: [V1>=1,V>=1,Out>=4,V+V1+2>=Out] * Chain [100]: 10*s(4472)+10*s(4473)+5 Such that:aux(486) =< V1 aux(487) =< V s(4473) =< aux(486) s(4472) =< aux(487) with precondition: [V1>=1,V>=1,Out>=5,V+V1+3>=Out] * Chain [99]: 10*s(4492)+10*s(4493)+8 Such that:aux(488) =< V1 aux(489) =< V s(4493) =< aux(488) s(4492) =< aux(489) with precondition: [V1>=1,V>=1,Out>=6,V+V1+4>=Out] * Chain [98]: 10*s(4512)+10*s(4513)+10 Such that:aux(490) =< V1 aux(491) =< V s(4513) =< aux(490) s(4512) =< aux(491) with precondition: [V1>=1,V>=1,Out>=7,V+V1+5>=Out] * Chain [97]: 4*s(4533)+6*s(4535)+4*s(4536)+12 Such that:aux(494) =< 1 aux(495) =< 2 aux(496) =< V1 s(4533) =< aux(496) s(4535) =< aux(494) s(4536) =< aux(495) with precondition: [V>=0,Out>=8,V1+7>=Out] #### Cost of chains of start(V1,V,V14,V12,V23): * Chain [137]: 11*s(4625)+4*s(4626)+20162*s(4627)+240*s(4628)+20*s(4630)+20*s(4631)+6*s(4632)+1320*s(4644)+816*s(4645)+6622*s(4646)+1440*s(4649)+1440*s(4650)+6288*s(4657)+480*s(4672)+480*s(4673)+480*s(4675)+480*s(4676)+1*s(4785)+93 Such that:s(4785) =< V14 aux(506) =< 1 aux(507) =< 2 aux(508) =< -V1+V aux(509) =< V1 aux(510) =< V1+1 aux(511) =< V1+2 aux(512) =< V1+V aux(513) =< V aux(514) =< V12 s(4646) =< aux(509) s(4625) =< aux(510) s(4632) =< aux(511) s(4627) =< aux(513) s(4644) =< aux(506) s(4645) =< aux(507) s(4629) =< aux(513) s(4649) =< s(4627)*aux(513) s(4650) =< s(4627)*s(4629) s(4657) =< aux(512) s(4671) =< aux(509) s(4672) =< s(4646)*aux(509) s(4673) =< s(4646)*s(4671) s(4674) =< aux(512) s(4675) =< s(4657)*aux(512) s(4676) =< s(4657)*s(4674) s(4626) =< aux(514) s(4628) =< aux(508) s(4630) =< s(4628)*aux(513) s(4631) =< s(4628)*s(4629) with precondition: [V1>=0] * Chain [136]: 2*s(4787)+62*s(4790)+4*s(4792)+4*s(4793)+4*s(4794)+24*s(4795)+2*s(4796)+2*s(4797)+19 Such that:s(4786) =< 2 s(4788) =< V s(4789) =< V12 s(4787) =< s(4786) s(4790) =< s(4788) s(4791) =< s(4788) s(4792) =< s(4790)*s(4788) s(4793) =< s(4790)*s(4791) s(4794) =< s(4789) s(4795) =< s(4788) s(4795) =< s(4789) s(4796) =< s(4795)*s(4788) s(4797) =< s(4795)*s(4791) with precondition: [V1=0,V14=0,V>=0,V12>=1] * Chain [135]: 12 with precondition: [V1=0,V>=0,V14>=2,V12>=0] * Chain [134]: 1910*s(4801)+26*s(4802)+128*s(4810)+128*s(4811)+11*s(4814)+4*s(4826)+25 Such that:aux(515) =< 1 aux(516) =< 2 aux(517) =< V aux(518) =< V12 s(4814) =< aux(515) s(4801) =< aux(517) s(4826) =< aux(518) s(4802) =< aux(516) s(4809) =< aux(517) s(4810) =< s(4801)*aux(517) s(4811) =< s(4801)*s(4809) with precondition: [V1=0,V>=1] * Chain [133]: 3*s(4840)+2*s(4841)+13*s(4842)+120*s(4843)+10*s(4845)+10*s(4846)+6*s(4847)+8 Such that:s(4836) =< -V+V14 s(4839) =< V23 aux(519) =< V+1 aux(520) =< V+2 aux(521) =< V14 s(4840) =< aux(519) s(4847) =< aux(520) s(4841) =< s(4839) s(4842) =< aux(521) s(4843) =< s(4836) s(4844) =< aux(521) s(4845) =< s(4843)*aux(521) s(4846) =< s(4843)*s(4844) with precondition: [V1=1,V>=0,V14>=0,V12>=0,V23>=0] * Chain [132]: 0 with precondition: [V1=1,V=0,V14>=0,V12>=2,V23>=0] * Chain [131]: 7*s(4859)+24*s(4860)+2*s(4862)+2*s(4863)+2*s(4864)+12*s(4865)+1*s(4866)+1*s(4867)+3*s(4869)+4*s(4870)+7 Such that:s(4857) =< -V+V14 s(4855) =< -V+V23 s(4858) =< V14 s(4856) =< V23 aux(522) =< V+1 aux(523) =< V+2 s(4869) =< aux(523) s(4859) =< s(4858) s(4860) =< s(4857) s(4861) =< s(4858) s(4862) =< s(4860)*s(4858) s(4863) =< s(4860)*s(4861) s(4864) =< s(4856) s(4865) =< s(4857) s(4865) =< s(4855) s(4866) =< s(4865)*s(4858) s(4867) =< s(4865)*s(4861) s(4870) =< aux(522) with precondition: [V1=1,V12=0,V>=0,V23>=1,V14>=V+2] * Chain [130]: 1*s(4875)+1*s(4876)+3 Such that:s(4875) =< V+1 s(4876) =< V23 with precondition: [V1=1,V12=0,V>=1,V14>=0,V23>=1] * Chain [129]: 1 with precondition: [V1=2,V>=0,V14>=0,V12>=0,V23>=0] * Chain [128]: 14*s(4881)+48*s(4882)+4*s(4884)+4*s(4885)+4*s(4886)+24*s(4887)+2*s(4888)+2*s(4889)+3*s(4891)+4*s(4892)+6 Such that:aux(524) =< -V1+V aux(525) =< -V1+V12 aux(526) =< V1+1 aux(527) =< V1+2 aux(528) =< V aux(529) =< V12 s(4891) =< aux(527) s(4881) =< aux(528) s(4882) =< aux(524) s(4883) =< aux(528) s(4884) =< s(4882)*aux(528) s(4885) =< s(4882)*s(4883) s(4886) =< aux(529) s(4887) =< aux(524) s(4887) =< aux(525) s(4888) =< s(4887)*aux(528) s(4889) =< s(4887)*s(4883) s(4892) =< aux(526) with precondition: [V14=0,V1>=0,V12>=1,V>=V1+2] * Chain [127]: 4*s(4910)+1*s(4911)+4*s(4914)+5 Such that:s(4911) =< V12 aux(530) =< V1 aux(531) =< V1+1 s(4910) =< aux(531) s(4914) =< aux(530) with precondition: [V14=0,V1>=1,V>=0,V12>=1] Closed-form bounds of start(V1,V,V14,V12,V23): ------------------------------------- * Chain [137] with precondition: [V1>=0] - Upper bound: 6622*V1+3045+960*V1*V1+nat(V)*20162+nat(V)*2880*nat(V)+nat(V)*40*nat(-V1+V)+nat(V14)+nat(V12)*4+nat(V1+V)*6288+nat(V1+V)*960*nat(V1+V)+(11*V1+11)+(6*V1+12)+nat(-V1+V)*240 - Complexity: n^2 * Chain [136] with precondition: [V1=0,V14=0,V>=0,V12>=1] - Upper bound: 86*V+23+12*V*V+4*V12 - Complexity: n^2 * Chain [135] with precondition: [V1=0,V>=0,V14>=2,V12>=0] - Upper bound: 12 - Complexity: constant * Chain [134] with precondition: [V1=0,V>=1] - Upper bound: 1910*V+88+256*V*V+nat(V12)*4 - Complexity: n^2 * Chain [133] with precondition: [V1=1,V>=0,V14>=0,V12>=0,V23>=0] - Upper bound: 13*V14+8+20*V14*nat(-V+V14)+2*V23+(3*V+3)+(6*V+12)+nat(-V+V14)*120 - Complexity: n^2 * Chain [132] with precondition: [V1=1,V=0,V14>=0,V12>=2,V23>=0] - Upper bound: 0 - Complexity: constant * Chain [131] with precondition: [V1=1,V12=0,V>=0,V23>=1,V14>=V+2] - Upper bound: 7*V14+7+(-V+V14)*(6*V14)+2*V23+(4*V+4)+(3*V+6)+(-36*V+36*V14) - Complexity: n^2 * Chain [130] with precondition: [V1=1,V12=0,V>=1,V14>=0,V23>=1] - Upper bound: V+V23+4 - Complexity: n * Chain [129] with precondition: [V1=2,V>=0,V14>=0,V12>=0,V23>=0] - Upper bound: 1 - Complexity: constant * Chain [128] with precondition: [V14=0,V1>=0,V12>=1,V>=V1+2] - Upper bound: 14*V+6+(-V1+V)*(12*V)+4*V12+(4*V1+4)+(3*V1+6)+(-72*V1+72*V) - Complexity: n^2 * Chain [127] with precondition: [V14=0,V1>=1,V>=0,V12>=1] - Upper bound: 8*V1+V12+9 - Complexity: n ### Maximum cost of start(V1,V,V14,V12,V23): max([max([12,nat(V14)*7+4+nat(V14)*6*nat(-V+V14)+nat(V23)+nat(V+1)*2+nat(V+2)*3+nat(-V+V14)*36+max([nat(V+1),nat(V14)*6+1+nat(V14)*14*nat(-V+V14)+nat(V+2)*3+nat(-V+V14)*84])+(nat(V23)+3+nat(V+1))]),nat(V12)+5+max([8*V1+4,nat(V)*14+1+nat(V12)*3+max([4*V1+4+nat(V)*12*nat(-V1+V)+(3*V1+6)+nat(-V1+V)*72,6622*V1+2957+960*V1*V1+nat(V)*18252+nat(V)*2624*nat(V)+nat(V)*40*nat(-V1+V)+nat(V14)+nat(V1+V)*6288+nat(V1+V)*960*nat(V1+V)+(11*V1+11)+(6*V1+12)+nat(-V1+V)*240+(nat(V)*1824+65+nat(V)*244*nat(V))+(nat(V)*72+17+nat(V)*12*nat(V))])])]) Asymptotic class: n^2 * Total analysis performed in 21132 ms. ---------------------------------------- (12) BOUNDS(1, n^2) ---------------------------------------- (13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (14) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) PLUS(z0, 0) -> c2 PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) LENGTH(nil) -> c4 LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) GE(z0, 0) -> c7 GE(0, s(z0)) -> c8 GE(s(z0), s(z1)) -> c9(GE(z0, z1)) IF(true, z0, z1, z2, z3) -> c10 IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) TAKE(0, cons(z0, xs), z1) -> c12 TAKE(0, nil, cons(z0, z1)) -> c13 TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) The (relative) TRS S consists of the following rules: app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) plus(z0, 0) -> z0 plus(z0, s(z1)) -> s(plus(z0, z1)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) if(true, z0, z1, z2, z3) -> nil if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) take(0, cons(z0, xs), z1) -> z0 take(0, nil, cons(z0, z1)) -> z0 take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (15) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence LENGTH(cons(z0, z1)) ->^+ c5(LENGTH(z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / cons(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) PLUS(z0, 0) -> c2 PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) LENGTH(nil) -> c4 LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) GE(z0, 0) -> c7 GE(0, s(z0)) -> c8 GE(s(z0), s(z1)) -> c9(GE(z0, z1)) IF(true, z0, z1, z2, z3) -> c10 IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) TAKE(0, cons(z0, xs), z1) -> c12 TAKE(0, nil, cons(z0, z1)) -> c13 TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) The (relative) TRS S consists of the following rules: app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) plus(z0, 0) -> z0 plus(z0, s(z1)) -> s(plus(z0, z1)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) if(true, z0, z1, z2, z3) -> nil if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) take(0, cons(z0, xs), z1) -> z0 take(0, nil, cons(z0, z1)) -> z0 take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: APP(z0, z1) -> c(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z0)) APP(z0, z1) -> c1(HELPA(0, plus(length(z0), length(z1)), z0, z1), PLUS(length(z0), length(z1)), LENGTH(z1)) PLUS(z0, 0) -> c2 PLUS(z0, s(z1)) -> c3(PLUS(z0, z1)) LENGTH(nil) -> c4 LENGTH(cons(z0, z1)) -> c5(LENGTH(z1)) HELPA(z0, z1, z2, z3) -> c6(IF(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1)) GE(z0, 0) -> c7 GE(0, s(z0)) -> c8 GE(s(z0), s(z1)) -> c9(GE(z0, z1)) IF(true, z0, z1, z2, z3) -> c10 IF(false, z0, z1, z2, z3) -> c11(HELPB(z0, z1, z2, z3)) TAKE(0, cons(z0, xs), z1) -> c12 TAKE(0, nil, cons(z0, z1)) -> c13 TAKE(s(z0), cons(z1, xs), z2) -> c14(TAKE(z0, xs, z2)) TAKE(s(z0), nil, cons(z1, z2)) -> c15(TAKE(z0, nil, z2)) HELPB(z0, z1, z2, z3) -> c16(TAKE(z0, z2, z3)) HELPB(z0, z1, z2, z3) -> c17(HELPA(s(z0), z1, z2, z3)) The (relative) TRS S consists of the following rules: app(z0, z1) -> helpa(0, plus(length(z0), length(z1)), z0, z1) plus(z0, 0) -> z0 plus(z0, s(z1)) -> s(plus(z0, z1)) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) helpa(z0, z1, z2, z3) -> if(ge(z0, z1), z0, z1, z2, z3) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) if(true, z0, z1, z2, z3) -> nil if(false, z0, z1, z2, z3) -> helpb(z0, z1, z2, z3) take(0, cons(z0, xs), z1) -> z0 take(0, nil, cons(z0, z1)) -> z0 take(s(z0), cons(z1, xs), z2) -> take(z0, xs, z2) take(s(z0), nil, cons(z1, z2)) -> take(z0, nil, z2) helpb(z0, z1, z2, z3) -> cons(take(z0, z2, z3), helpa(s(z0), z1, z2, z3)) Rewrite Strategy: INNERMOST