YES(?,O(n^1)) * Step 1: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. a(A) -> a(-1 + A) [A >= 1] (?,1) 1. start(A) -> a(100) [A = 100] (1,1) 2. start(A) -> a(A) [A >= 1] (1,1) Signature: {(a,1);(start,1)} Flow Graph: [0->{0},1->{0},2->{0}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(a) = x1 p(start) = x1 Following rules are strictly oriented: [A >= 1] ==> a(A) = A > -1 + A = a(-1 + A) Following rules are weakly oriented: [A = 100] ==> start(A) = A >= 100 = a(100) [A >= 1] ==> start(A) = A >= A = a(A) * Step 2: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. a(A) -> a(-1 + A) [A >= 1] (A,1) 1. start(A) -> a(100) [A = 100] (1,1) 2. start(A) -> a(A) [A >= 1] (1,1) Signature: {(a,1);(start,1)} Flow Graph: [0->{0},1->{0},2->{0}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))