YES(?,O(n^1)) * Step 1: 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}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval) = x1 p(start) = x1 Following rules are strictly oriented: [2*B >= 0 && A = 1 + 2*B] ==> eval(A) = A > 2*B = eval(2*B) Following rules are weakly oriented: True ==> start(A) = A >= A = eval(A) * Step 2: KnowledgePropagation 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}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))