YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 1 >= A && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 2 && B = C && D = A] (?,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && A >= 2 && D = 1 && B = C] 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && D >= 2 && D >= 1 && A >= 1 + D && B = C] 4. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl32,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{2,3},4->{0,1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 1 >= A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 2 && B = C && D = A] (1,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [-1 + A + -1*D >= 0 (1,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && A >= 2 && D = 1 && B = C] 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && D >= 2 && D >= 1 && A >= 1 + D && B = C] 4. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl32,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{2,3},4->{0,1}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl32) = 1 + x4 p(start) = x4 p(start0) = x1 p(stop) = x4 Following rules are strictly oriented: [-1 + A + -1*D >= 0 ==> && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && A >= 2 && D = 1 && B = C] lbl32(A,B,C,D) = 1 + D > D = stop(A,B,C,D) [-1 + A + -1*D >= 0 ==> && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && D >= 2 && D >= 1 && A >= 1 + D && B = C] lbl32(A,B,C,D) = 1 + D > D = lbl32(A,B,C,-1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 1 >= A && B = C && D = A] ==> start(A,B,C,D) = D >= D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 2 && B = C && D = A] ==> start(A,B,C,D) = D >= D = lbl32(A,B,C,-1 + D) True ==> start0(A,B,C,D) = A >= A = start(A,C,C,A) * Step 3: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 1 >= A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 2 && B = C && D = A] (1,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [-1 + A + -1*D >= 0 (1,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && A >= 2 && D = 1 && B = C] 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [-1 + A + -1*D >= 0 (A,1) && -1 + D >= 0 && -3 + A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && -2 + A >= 0 && D >= 2 && D >= 1 && A >= 1 + D && B = C] 4. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl32,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{2,3},2->{},3->{2,3},4->{0,1}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))