WORST_CASE(?,O(n^2)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (?,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (?,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, A, .= 0) (<0,0,B>, 0, .= 0) (<1,0,A>, A, .= 0) (<1,0,B>, 1 + B, .+ 1) (<2,0,A>, 1 + A, .+ 1) (<2,0,B>, B, .= 0) (<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (?,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (?,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, ?) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, ?) (<3,0,B>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, ?) (<0,0,B>, 0) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, A) (<3,0,B>, B) * Step 3: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (?,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (?,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, 0) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, A) (<3,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval1) = 2 + x1 p(eval2) = 1 + x1 p(start) = 2 + x1 The following rules are strictly oriented: [A >= 0] ==> eval1(A,B) = 2 + A > 1 + A = eval2(A,0) The following rules are weakly oriented: [A >= 1 + B] ==> eval2(A,B) = 1 + A >= 1 + A = eval2(A,1 + B) [B >= A] ==> eval2(A,B) = 1 + A >= 1 + A = eval1(-1 + A,B) True ==> start(A,B) = 2 + A >= 2 + A = eval1(A,B) * Step 4: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (2 + A,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (?,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, 0) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, A) (<3,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,1], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval1) = 0 p(eval2) = 1 The following rules are strictly oriented: [B >= A] ==> eval2(A,B) = 1 > 0 = eval1(-1 + A,B) The following rules are weakly oriented: [A >= 1 + B] ==> eval2(A,B) = 1 >= 1 = eval2(A,1 + B) We use the following global sizebounds: (<0,0,A>, ?) (<0,0,B>, 0) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, A) (<3,0,B>, B) * Step 5: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (2 + A,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (2 + A,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, 0) (<1,0,A>, ?) (<1,0,B>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<3,0,A>, A) (<3,0,B>, B) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, 2 + 2*A) (<0,0,B>, 0) (<1,0,A>, 2 + 2*A) (<1,0,B>, 2 + 2*A) (<2,0,A>, 2 + 2*A) (<2,0,B>, 2 + 2*A) (<3,0,A>, A) (<3,0,B>, B) * Step 6: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (2 + A,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (?,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (2 + A,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, 2 + 2*A) (<0,0,B>, 0) (<1,0,A>, 2 + 2*A) (<1,0,B>, 2 + 2*A) (<2,0,A>, 2 + 2*A) (<2,0,B>, 2 + 2*A) (<3,0,A>, A) (<3,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [1], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(eval2) = x1 + -1*x2 The following rules are strictly oriented: [A >= 1 + B] ==> eval2(A,B) = A + -1*B > -1 + A + -1*B = eval2(A,1 + B) The following rules are weakly oriented: We use the following global sizebounds: (<0,0,A>, 2 + 2*A) (<0,0,B>, 0) (<1,0,A>, 2 + 2*A) (<1,0,B>, 2 + 2*A) (<2,0,A>, 2 + 2*A) (<2,0,B>, 2 + 2*A) (<3,0,A>, A) (<3,0,B>, B) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. eval1(A,B) -> eval2(A,0) [A >= 0] (2 + A,1) 1. eval2(A,B) -> eval2(A,1 + B) [A >= 1 + B] (4 + 6*A + 2*A^2,1) 2. eval2(A,B) -> eval1(-1 + A,B) [B >= A] (2 + A,1) 3. start(A,B) -> eval1(A,B) True (1,1) Signature: {(eval1,2);(eval2,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{0},3->{0}] Sizebounds: (<0,0,A>, 2 + 2*A) (<0,0,B>, 0) (<1,0,A>, 2 + 2*A) (<1,0,B>, 2 + 2*A) (<2,0,A>, 2 + 2*A) (<2,0,B>, 2 + 2*A) (<3,0,A>, A) (<3,0,B>, B) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^2))