The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 25 + 5 * |#0|).

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * A very simple loop over an array.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class Loop1 {
    public static void main(int j) {
	for (int i = 0; i < j; i++) {}
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 43 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 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.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 43 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

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

obtained
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
by chaining
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38

obtained
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
by chaining
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54

obtained
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
by chaining
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

(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(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

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

Moved arithmethic from lhss to constraints.

main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
was transformed to
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0

(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_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0

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

Moved arithmethic from constraints to rhss.

main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
was transformed to
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0

main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
was transformed to
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

(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_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

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

Simplified expressions.

main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0
was transformed to
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

(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_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= i10 && x = 0
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

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

Transformed 43 jbc graph edges to a weighted ITS with 43 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 43 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

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

obtained
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
by chaining
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38

obtained
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
by chaining
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54

obtained
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
by chaining
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

(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(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

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

Moved arithmethic from lhss to constraints.

main_GE_58(i10, 0, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2
was transformed to
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0

(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_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0

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

Moved arithmethic from constraints to rhss.

main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, iconst_0, env, static) :|: i9 <= 0 && iconst_0 = 0
was transformed to
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0

main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
was transformed to
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

(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_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

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

Simplified expressions.

main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= 1 && 1 <= i10 && 1 <= 3 && 1 <= 2 && x = 0
was transformed to
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

(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_GE_202(i53, i54, env, static) -{3,3}> main_Load_192(i53, i54 + 1, env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_Load_192(i53, i54, env, static) -{2,2}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_206(i53, i54, env, static) :|: i53 <= i54 && 1 <= i54
main_GE_58(i9, iconst_0, env, static) -{0,0}> main_GE_59(i9, 0, env, static) :|: i9 <= 0 && iconst_0 = 0
main_GE_58(i10, x, env, static) -{3,3}> main_Load_192(i10, 1, env, static) :|: 0 < i10 && 1 <= i10 && x = 0
main_ConstantStackPush_1(i1, env, static) -{19,19}> main_GE_58(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

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

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

(26) Obligation:

Set of 41 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 41 jbc graph edges to a weighted ITS with 41 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 41 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

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

obtained
main_ConstantStackPush_1(i1, env, static) -{22,22}> main_Load_192(i1, 1, env, static'1) :|: static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 1 <= 2 && 0 < i1 && 0 < 2 && 0 >= 0
by chaining
main_ConstantStackPush_1(i1, env, static) -{0,0}> main_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_24(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_28(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, env, static) -{1,1}> main_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i1, env, static) -{0,0}> main_ConstantStackPush_49(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, env, static) -{0,0}> main_ConstantStackPush_50(i1, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, env, static) -{0,0}> main_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, env, static) -{0,0}> main_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, env, static) -{1,1}> main_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, iconst_0, env, static) -{1,1}> main_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, iconst_0, env, static) -{1,1}> main_Load_55(i1, iconst_0, env, static) :|: iconst_0 = 0
main_Load_55(i1, iconst_0, env, static) -{1,1}> main_GE_58(i1, iconst_0, env, static) :|: iconst_0 = 0
main_GE_58(i10, iconst_0, env, static) -{0,0}> main_GE_60(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 = 0
main_GE_60(i10, iconst_0, env, static) -{1,1}> main_Inc_65(i10, iconst_0, env, static) :|: 1 <= i10 && iconst_0 < i10 && iconst_0 = 0
main_Inc_65(i10, iconst_0, env, static) -{1,1}> main_JMP_69(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1 && iconst_0 = 0
main_JMP_69(i10, iconst_1, env, static) -{1,1}> main_Load_74(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 = 1
main_Load_74(i10, iconst_1, env, static) -{0,0}> main_Load_112(i10, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= i10 && 1 <= iconst_1 && iconst_1 = 1
main_Load_112(i24, i25, env, static) -{0,0}> main_Load_158(i24, i25, env, static) :|: 1 <= i25 && i25 <= 2 && 1 <= i24 && i25 <= 3
main_Load_158(i37, i38, env, static) -{0,0}> main_Load_192(i37, i38, env, static) :|: i38 <= 3 && 1 <= i37 && 1 <= i38

obtained
main_Load_192(i53, i54, env, static) -{5,5}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
by chaining
main_Load_192(i53, i54, env, static) -{1,1}> main_Load_195(i53, i54, env, static) :|: 1 <= i54
main_Load_195(i53, i54, env, static) -{1,1}> main_GE_202(i53, i54, env, static) :|: 1 <= i54
main_GE_202(i53, i54, env, static) -{0,0}> main_GE_207(i53, i54, env, static) :|: 1 <= i54 && i54 < i53
main_GE_207(i53, i54, env, static) -{1,1}> main_Inc_212(i53, i54, env, static) :|: 2 <= i53 && 1 <= i54 && i54 < i53
main_Inc_212(i53, i54, env, static) -{1,1}> main_JMP_217(i53, i65, env, static) :|: 2 <= i53 && i54 + 1 = i65 && 1 <= i54 && 2 <= i65
main_JMP_217(i53, i65, env, static) -{1,1}> main_Load_221(i53, i65, env, static) :|: 2 <= i53 && 2 <= i65
main_Load_221(i53, i65, env, static) -{0,0}> main_Load_192(i53, i65, env, static) :|: 2 <= i53 && 1 <= i65 && 2 <= i65

(30) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i1, env, static) -{22,22}> main_Load_192(i1, 1, env, static'1) :|: static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 1 <= 2 && 0 < i1 && 0 < 2 && 0 >= 0
main_Load_192(i53, i54, env, static) -{5,5}> main_Load_192(i53, i65', env, static) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

(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_192(x1, x2, x3, x4) → main_Load_192(x1, x2)

(32) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(i1, static) -{22,22}> main_Load_192(i1, 1) :|: static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 1 <= 2 && 0 < i1 && 0 < 2 && 0 >= 0
main_Load_192(i53, i54) -{5,5}> main_Load_192(i53, i65') :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

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

Moved arithmethic from constraints to rhss.

main_Load_192(i53, i54) -{5,5}> main_Load_192(i53, i65') :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
was transformed to
main_Load_192(i53, i54) -{5,5}> main_Load_192(i53, i54 + 1) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'

(34) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_192(i53, i54) -{5,5}> main_Load_192(i53, i54 + 1) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_ConstantStackPush_1(i1, static) -{22,22}> main_Load_192(i1, 1) :|: static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 1 <= 2 && 0 < i1 && 0 < 2 && 0 >= 0

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

Simplified expressions.

main_ConstantStackPush_1(i1, static) -{22,22}> main_Load_192(i1, 1) :|: static'1 <= static''' + 1 && 1 <= 1 && 0 <= 2 && 1 <= 3 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 1 <= 2 && 0 < i1 && 0 < 2 && 0 >= 0
was transformed to
main_ConstantStackPush_1(i1, static) -{22,22}> main_Load_192(i1, 1) :|: static'1 <= static''' + 1 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && 0 < i1

(36) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_192(i53, i54) -{5,5}> main_Load_192(i53, i54 + 1) :|: 1 <= i54 && 2 <= i65' && i54 < i53 && 2 <= i53 && 1 <= i65' && i54 + 1 = i65'
main_ConstantStackPush_1(i1, static) -{22,22}> main_Load_192(i1, 1) :|: static'1 <= static''' + 1 && 1 <= i1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && 0 < i1

(37) koat Proof (EQUIVALENT transformation)

YES(?, 5*ar_0 + 22)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) main_Load_192(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= i65' /\ ar_1 < ar_0 /\ 2 <= ar_0 /\ 1 <= i65' /\ ar_1 + 1 = i65' ]
(Comp: ?, Cost: 22) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, 1)) [ static'1 <= static''' + 1 /\ 1 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(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: ?, Cost: 5) main_Load_192(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= i65' /\ ar_1 < ar_0 /\ 2 <= ar_0 /\ 1 <= i65' /\ ar_1 + 1 = i65' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, 1)) [ static'1 <= static''' + 1 /\ 1 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(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_192) = V_1 - V_2
Pol(main_ConstantStackPush_1) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_Load_192(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= i65' /\ ar_1 < ar_0 /\ 2 <= ar_0 /\ 1 <= i65' /\ ar_1 + 1 = i65' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0, Cost: 5) main_Load_192(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, ar_1 + 1)) [ 1 <= ar_1 /\ 2 <= i65' /\ ar_1 < ar_0 /\ 2 <= ar_0 /\ 1 <= i65' /\ ar_1 + 1 = i65' ]
(Comp: 1, Cost: 22) main_ConstantStackPush_1(ar_0, ar_1) -> Com_1(main_Load_192(ar_0, 1)) [ static'1 <= static''' + 1 /\ 1 <= ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(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 5*ar_0 + 22

Time: 0.052 sec (SMT: 0.046 sec)

(38) BOUNDS(CONSTANT, 22 + 5 * |#0|)