The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 166088 + 3260 * |#0| + 16 * |#0|^2).

(0) Obligation:

Need to prove time_complexity of the following program:

public class McCarthyIterative {
  public static int main(int x) {
    int c = 1;
    while (c > 0) {
      if (x > 100) {
        x -= 10;
        c--;
      } else {
        x += 11;
        c++;
      }
    }
    return x;
  }

}

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
McCarthyIterative.main(I)I: Graph of 46 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 44 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 44 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  

Considered paths: nonterm paths and paths from start to sinks

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 44 jbc graph edges to a weighted ITS with 44 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 44 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1

obtained
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
by chaining
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100

obtained
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
by chaining
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

obtained
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
by chaining
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341

(8) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
was transformed to
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100

(10) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0

(11) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
was transformed to
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100

main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
was transformed to
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0

(12) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332

(13) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 - 10, i332 - 1, env, static) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
was transformed to
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 1 <= i332 && 0 < i332

(14) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 - 10, i332 - 1, env, static) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 1 <= i332 && 0 < i332
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320

(15) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 44 jbc graph edges to a weighted ITS with 44 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(16) Obligation:

IntTrs with 44 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

(17) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1

obtained
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
by chaining
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100

obtained
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
by chaining
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

obtained
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
by chaining
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341

(18) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(19) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
was transformed to
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100

(20) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0

(21) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
was transformed to
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100

main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, iconst_0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
was transformed to
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0

(22) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332

(23) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 + -10, i332 + -1, env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
was transformed to
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 - 10, i332 - 1, env, static) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100

main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 0 <= i332 && 1 <= i332 && 0 < i332
was transformed to
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 1 <= i332 && 0 < i332

(24) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_473(i214, iconst_0, i319, env, static) -{0,0}> main_LE_474(i214, 0, i319, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_481(i214, i338, x, i332, env, static) -{4,4}> main_Load_471(i214, i338 - 10, i332 - 1, env, static) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338 && x = 100
main_LE_481(i214, i337, x, i332, env, static) -{4,4}> main_Load_471(i214, i337 + 11, i332 + 1, env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332 && x = 100
main_LE_473(i214, i332, i319, env, static) -{3,3}> main_LE_481(i214, i319, 100, i332, env, static) :|: 1 <= i332 && 0 < i332
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)

Extracted set of 43 edges for the analysis of TIME complexity. Dropped leaves.

(26) Obligation:

Set of 43 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

(27) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 43 jbc graph edges to a weighted ITS with 43 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(28) Obligation:

IntTrs with 43 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

(29) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
main_ConstantStackPush_1(i2, env, static) -{0,0}> main_ConstantStackPush_3(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, env, static) -{1,1}> main_ConstantStackPush_41(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_41(i2, env, static) -{0,0}> main_ConstantStackPush_42(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_42(i2, env, static) -{0,0}> main_ConstantStackPush_44(i2, env, static) :|: 0 <= static
main_ConstantStackPush_44(i2, env, static) -{0,0}> main_ConstantStackPush_45(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_45(i2, env, static) -{0,0}> main_ConstantStackPush_47(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, env, static) -{1,1}> main_Store_50(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Store_50(i2, iconst_1, env, static) -{1,1}> main_Load_52(i2, iconst_1, env, static) :|: iconst_1 = 1
main_Load_52(i2, iconst_1, env, static) -{0,0}> main_Load_471(i2, i2, iconst_1, env, static) :|: 0 <= iconst_1 && iconst_1 = 1

obtained
main_Load_471(i214, i319, i320, env, static) -{4,4}> main_LE_481(i214, i319, 100, i320, env, static) :|: 0 <= i320 && 1 <= i320 && 0 < i320
by chaining
main_Load_471(i214, i319, i320, env, static) -{1,1}> main_LE_473(i214, i320, i319, env, static) :|: 0 <= i320
main_LE_473(i214, i332, i319, env, static) -{0,0}> main_LE_475(i214, i332, i319, env, static) :|: 1 <= i332 && 0 <= i332
main_LE_475(i214, i332, i319, env, static) -{1,1}> main_Load_477(i214, i319, i332, env, static) :|: 1 <= i332 && 0 < i332
main_Load_477(i214, i319, i332, env, static) -{1,1}> main_ConstantStackPush_479(i214, i319, i332, env, static) :|: 1 <= i332
main_ConstantStackPush_479(i214, i319, i332, env, static) -{1,1}> main_LE_481(i214, i319, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100

obtained
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
by chaining
main_LE_481(i214, i338, iconst_100, i332, env, static) -{0,0}> main_LE_483(i214, i338, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338
main_LE_483(i214, i338, iconst_100, i332, env, static) -{1,1}> main_Inc_485(i214, i338, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && 101 <= i338 && iconst_100 < i338
main_Inc_485(i214, i338, i332, env, static) -{1,1}> main_Inc_488(i214, i340, i332, env, static) :|: 1 <= i332 && i338 + -10 = i340 && 91 <= i340 && 101 <= i338
main_Inc_488(i214, i340, i332, env, static) -{1,1}> main_JMP_490(i214, i340, i342, env, static) :|: 1 <= i332 && 0 <= i342 && 91 <= i340 && i332 + -1 = i342
main_JMP_490(i214, i340, i342, env, static) -{1,1}> main_Load_493(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340
main_Load_493(i214, i340, i342, env, static) -{0,0}> main_Load_471(i214, i340, i342, env, static) :|: 0 <= i342 && 91 <= i340

obtained
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
by chaining
main_LE_481(i214, i337, iconst_100, i332, env, static) -{0,0}> main_LE_482(i214, i337, iconst_100, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= 100
main_LE_482(i214, i337, iconst_100, i332, env, static) -{1,1}> main_Inc_484(i214, i337, i332, env, static) :|: 1 <= i332 && iconst_100 = 100 && i337 <= iconst_100 && i337 <= 100
main_Inc_484(i214, i337, i332, env, static) -{1,1}> main_Inc_486(i214, i339, i332, env, static) :|: 1 <= i332 && i339 <= 111 && i337 + 11 = i339 && i337 <= 100
main_Inc_486(i214, i339, i332, env, static) -{1,1}> main_JMP_489(i214, i339, i341, env, static) :|: 1 <= i332 && i339 <= 111 && i332 + 1 = i341 && 2 <= i341
main_JMP_489(i214, i339, i341, env, static) -{1,1}> main_Load_491(i214, i339, i341, env, static) :|: i339 <= 111 && 2 <= i341
main_Load_491(i214, i339, i341, env, static) -{0,0}> main_Load_471(i214, i339, i341, env, static) :|: 0 <= i341 && i339 <= 111 && 2 <= i341

(30) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i2, env, static) -{17,17}> main_Load_471(i2, i2, 1, env, static'1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i214, i319, i320, env, static) -{4,4}> main_LE_481(i214, i319, 100, i320, env, static) :|: 0 <= i320 && 1 <= i320 && 0 < i320
main_LE_481(i214, i338, 100, i332, env, static) -{4,4}> main_Load_471(i214, i340', i342', env, static) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_LE_481(i214, i337, 100, i332, env, static) -{4,4}> main_Load_471(i214, i339', i341', env, static) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(31) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:

main_ConstantStackPush_1(x1, x2, x3) → main_ConstantStackPush_1(x1, x3)
main_Load_471(x1, x2, x3, x4, x5) → main_Load_471(x2, x3)
main_LE_481(x1, x2, x3, x4, x5, x6) → main_LE_481(x2, x4)

(32) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i2, static) -{17,17}> main_Load_471(i2, 1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_Load_471(i319, i320) -{4,4}> main_LE_481(i319, i320) :|: 0 <= i320 && 1 <= i320 && 0 < i320
main_LE_481(i338, i332) -{4,4}> main_Load_471(i340', i342') :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_LE_481(i337, i332) -{4,4}> main_Load_471(i339', i341') :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(33) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_LE_481(i338, i332) -{4,4}> main_Load_471(i340', i342') :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
was transformed to
main_LE_481(i338, i332) -{4,4}> main_Load_471(i338 + -10, i332 + -1) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338

main_LE_481(i337, i332) -{4,4}> main_Load_471(i339', i341') :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332
was transformed to
main_LE_481(i337, i332) -{4,4}> main_Load_471(i337 + 11, i332 + 1) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(34) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i2, static) -{17,17}> main_Load_471(i2, 1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_LE_481(i338, i332) -{4,4}> main_Load_471(i338 + -10, i332 + -1) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_Load_471(i319, i320) -{4,4}> main_LE_481(i319, i320) :|: 0 <= i320 && 1 <= i320 && 0 < i320
main_LE_481(i337, i332) -{4,4}> main_Load_471(i337 + 11, i332 + 1) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(35) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_ConstantStackPush_1(i2, static) -{17,17}> main_Load_471(i2, 1) :|: 0 <= 2 && 0 <= 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
main_ConstantStackPush_1(i2, static) -{17,17}> main_Load_471(i2, 1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_Load_471(i319, i320) -{4,4}> main_LE_481(i319, i320) :|: 0 <= i320 && 1 <= i320 && 0 < i320
was transformed to
main_Load_471(i319, i320) -{4,4}> main_LE_481(i319, i320) :|: 1 <= i320 && 0 < i320

main_LE_481(i338, i332) -{4,4}> main_Load_471(i338 + -10, i332 + -1) :|: i332 + -1 = i342' && 0 <= i342' && 91 <= i340' && i338 + -10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
was transformed to
main_LE_481(i338, i332) -{4,4}> main_Load_471(i338 - 10, i332 - 1) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338

(36) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i2, static) -{17,17}> main_Load_471(i2, 1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_481(i338, i332) -{4,4}> main_Load_471(i338 - 10, i332 - 1) :|: i332 - 1 = i342' && 0 <= i342' && 91 <= i340' && i338 - 10 = i340' && 100 < i338 && 1 <= i332 && 101 <= i338
main_Load_471(i319, i320) -{4,4}> main_LE_481(i319, i320) :|: 1 <= i320 && 0 < i320
main_LE_481(i337, i332) -{4,4}> main_Load_471(i337 + 11, i332 + 1) :|: i337 + 11 = i339' && 2 <= i341' && i332 + 1 = i341' && 0 <= i341' && i339' <= 111 && i337 <= 100 && 1 <= i332

(37) koat Proof (EQUIVALENT transformation)

YES(?, 16*ar_0^2 + 3260*ar_0 + 166085)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 17) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
(Comp: ?, Cost: 4) main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\ 2 <= i341' /\ ar_1 + 1 = i341' /\ 0 <= i341' /\ i339' <= 111 /\ ar_0 <= 100 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 17) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
(Comp: ?, Cost: 4) main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\ 2 <= i341' /\ ar_1 + 1 = i341' /\ 0 <= i341' /\ i339' <= 111 /\ ar_0 <= 100 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_ConstantStackPush_1) = -V_1 + 101
Pol(main_Load_471) = -V_1 + 10*V_2 + 91
Pol(main_LE_481) = -V_1 + 10*V_2 + 91
Pol(koat_start) = -V_1 + 101
orients all transitions weakly and the transition
main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\ 2 <= i341' /\ ar_1 + 1 = i341' /\ 0 <= i341' /\ i339' <= 111 /\ ar_0 <= 100 /\ 1 <= ar_1 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 17) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
(Comp: ?, Cost: 4) main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ar_0 + 101, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\ 2 <= i341' /\ ar_1 + 1 = i341' /\ 0 <= i341' /\ i339' <= 111 /\ ar_0 <= 100 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_471) = 2*V_2 + 1
Pol(main_LE_481) = 2*V_2
and size complexities
S("koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]", 0-1) = ar_1
S("main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\\ 2 <= i341' /\\ ar_1 + 1 = i341' /\\ 0 <= i341' /\\ i339' <= 111 /\\ ar_0 <= 100 /\\ 1 <= ar_1 ]", 0-0) = ar_0 + 111
S("main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\\ 2 <= i341' /\\ ar_1 + 1 = i341' /\\ 0 <= i341' /\\ i339' <= 111 /\\ ar_0 <= 100 /\\ 1 <= ar_1 ]", 0-1) = ar_0 + 102
S("main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\\ 0 < ar_1 ]", 0-0) = ar_0 + 111
S("main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\\ 0 < ar_1 ]", 0-1) = ar_0 + 102
S("main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\\ 0 <= i342' /\\ 91 <= i340' /\\ ar_0 - 10 = i340' /\\ 100 < ar_0 /\\ 1 <= ar_1 /\\ 101 <= ar_0 ]", 0-0) = ar_0 + 111
S("main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\\ 0 <= i342' /\\ 91 <= i340' /\\ ar_0 - 10 = i340' /\\ 100 < ar_0 /\\ 1 <= ar_1 /\\ 101 <= ar_0 ]", 0-1) = ar_0 + 102
S("main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_1 + 2 /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_1 + 2 /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-1) = 1
orients the transitions
main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
weakly and the transitions
main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 17) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_471(ar_0, 1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 2*ar_0^2 + 407*ar_0 + 20708, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 - 10, ar_1 - 1)) [ ar_1 - 1 = i342' /\ 0 <= i342' /\ 91 <= i340' /\ ar_0 - 10 = i340' /\ 100 < ar_0 /\ 1 <= ar_1 /\ 101 <= ar_0 ]
(Comp: 2*ar_0^2 + 407*ar_0 + 20708, Cost: 4) main_Load_471(ar_0, ar_1) -> Com_1(main_LE_481(ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ar_0 + 101, Cost: 4) main_LE_481(ar_0, ar_1) -> Com_1(main_Load_471(ar_0 + 11, ar_1 + 1)) [ ar_0 + 11 = i339' /\ 2 <= i341' /\ ar_1 + 1 = i341' /\ 0 <= i341' /\ i339' <= 111 /\ ar_0 <= 100 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_ConstantStackPush_1(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 16*ar_0^2 + 3260*ar_0 + 166085

Time: 0.162 sec (SMT: 0.150 sec)

(38) BOUNDS(CONSTANT, 166085 + 3260 * |#0| + 16 * |#0|^2)