WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (?,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(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (?,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>, 1) (<1,0,A>, A) * Step 3: LocationConstraintsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (?,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) (<1,0,A>, A) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 0 : [2*C >= 1] 1 : True . * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. eval(A) -> eval(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (?,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) (<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*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] ==> eval(A) = A > -1 + 2*C = eval(-1 + 2*C) 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(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (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>, 1) (<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(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (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>, 1) (<1,0,A>, A) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^1))