YES(?,O(n^1)) * Step 1: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A) -> eval(A) True (1,1) 1. eval(A) -> eval(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (?,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{1},1->{1}] + 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*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] ==> eval(A) = A > -1 + 2*C = eval(-1 + 2*C) Following rules are weakly oriented: True ==> start(A) = A >= A = eval(A) * Step 2: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A) -> eval(A) True (1,1) 1. eval(A) -> eval(-1 + 2*C) [2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C] (A,1) Signature: {(eval,1);(start,1)} Flow Graph: [0->{1},1->{1}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))