WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (?,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, 1 + A, .+ 1) (<1,0,A>, A, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (?,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] Sizebounds: (<0,0,A>, ?) (<1,0,A>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, 2) (<1,0,A>, A) * Step 3: LocationConstraintsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (?,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] Sizebounds: (<0,0,A>, 2) (<1,0,A>, A) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 0 : [2*B >= 0] 1 : True . * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (?,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] Sizebounds: (<0,0,A>, 2) (<1,0,A>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval) = x1 p(start) = x1 The following rules are strictly oriented: [2*B >= 0 && A = 1 + 2*B] ==> eval(A) = A > 2*B = eval(2*B) The following rules are weakly oriented: True ==> start(A) = A >= A = eval(A) * Step 5: LoopRecurrenceProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (A,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] Sizebounds: (<0,0,A>, 2) (<1,0,A>, A) + Applied Processor: LoopRecurrenceProcessor [0] + Details: Applying the recurrence pattern linear * f to the expression A yields the solution A . * Step 6: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(2*B) [2*B >= 0 && A = 1 + 2*B] (A,1) 1. start(A) -> eval(A) True (1,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{0},1->{0}] Sizebounds: (<0,0,A>, 2) (<1,0,A>, A) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^1))