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) [1 >= A && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A >= 2 && B = C && D = A] (?,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [A >= 2 && D = 1 && B = C] (?,1) 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [D >= 2 && D >= 1 && A >= 1 + D && B = C] (?,1) 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) [1 >= A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A >= 2 && B = C && D = A] (1,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [A >= 2 && D = 1 && B = C] (1,1) 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [D >= 2 && D >= 1 && A >= 1 + D && B = C] (?,1) 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) = x4 p(start) = x4 p(start0) = x1 p(stop) = x4 Following rules are strictly oriented: [A >= 2 && B = C && D = A] ==> start(A,B,C,D) = D > -1 + D = lbl32(A,B,C,-1 + D) [D >= 2 && D >= 1 && A >= 1 + D && B = C] ==> lbl32(A,B,C,D) = D > -1 + D = lbl32(A,B,C,-1 + D) Following rules are weakly oriented: [1 >= A && B = C && D = A] ==> start(A,B,C,D) = D >= D = stop(A,B,C,D) [A >= 2 && D = 1 && B = C] ==> lbl32(A,B,C,D) = D >= D = stop(A,B,C,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) [1 >= A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl32(A,B,C,-1 + D) [A >= 2 && B = C && D = A] (1,1) 2. lbl32(A,B,C,D) -> stop(A,B,C,D) [A >= 2 && D = 1 && B = C] (1,1) 3. lbl32(A,B,C,D) -> lbl32(A,B,C,-1 + D) [D >= 2 && D >= 1 && A >= 1 + D && B = C] (A,1) 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))