YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f3(A,B,C,D) -> f1(0,B,C,D) True (1,1) 1. f1(A,B,C,D) -> f2(A,B,C,E) [-1*A >= 0 && A >= 0 && B >= C] (?,1) 2. f1(A,B,C,D) -> f2(1,1 + B,C,E) [-1*A >= 0 && A >= 0 && 1 + B = C && A = 0] (?,1) 3. f1(A,B,C,D) -> f1(0,1 + B,-1 + C,D) [-1*A >= 0 && A >= 0 && C >= 2 + B && C >= 1 + B && A = 0] (?,1) Signature: {(f1,4);(f2,4);(f3,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{1,2,3}] + 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. f3(A,B,C,D) -> f1(0,B,C,D) True (1,1) 1. f1(A,B,C,D) -> f2(A,B,C,E) [-1*A >= 0 && A >= 0 && B >= C] (1,1) 2. f1(A,B,C,D) -> f2(1,1 + B,C,E) [-1*A >= 0 && A >= 0 && 1 + B = C && A = 0] (1,1) 3. f1(A,B,C,D) -> f1(0,1 + B,-1 + C,D) [-1*A >= 0 && A >= 0 && C >= 2 + B && C >= 1 + B && A = 0] (?,1) Signature: {(f1,4);(f2,4);(f3,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = -1*x2 + x3 p(f2) = x1 + -1*x2 + x3 p(f3) = -1*x2 + x3 Following rules are strictly oriented: [-1*A >= 0 && A >= 0 && C >= 2 + B && C >= 1 + B && A = 0] ==> f1(A,B,C,D) = -1*B + C > -2 + -1*B + C = f1(0,1 + B,-1 + C,D) Following rules are weakly oriented: True ==> f3(A,B,C,D) = -1*B + C >= -1*B + C = f1(0,B,C,D) [-1*A >= 0 && A >= 0 && B >= C] ==> f1(A,B,C,D) = -1*B + C >= A + -1*B + C = f2(A,B,C,E) [-1*A >= 0 && A >= 0 && 1 + B = C && A = 0] ==> f1(A,B,C,D) = -1*B + C >= -1*B + C = f2(1,1 + B,C,E) * Step 3: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f3(A,B,C,D) -> f1(0,B,C,D) True (1,1) 1. f1(A,B,C,D) -> f2(A,B,C,E) [-1*A >= 0 && A >= 0 && B >= C] (1,1) 2. f1(A,B,C,D) -> f2(1,1 + B,C,E) [-1*A >= 0 && A >= 0 && 1 + B = C && A = 0] (1,1) 3. f1(A,B,C,D) -> f1(0,1 + B,-1 + C,D) [-1*A >= 0 && A >= 0 && C >= 2 + B && C >= 1 + B && A = 0] (B + C,1) Signature: {(f1,4);(f2,4);(f3,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{1,2,3}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))