(0) Obligation:

Need to prove time_complexity of the following program:
/**
 * An example of nested iterations.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
 */

public class Nested {
    public static void main(String[] args) {
	for (int i = 0; i < 10; i++)
	    for (int j = 3; j < 12; j += 2) {
		j -= 1;
	    }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Nested.main([Ljava/lang/String;)V: Graph of 57 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 56 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 56 jbc graph edges to a weighted ITS with 56 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.

(6) Obligation:

IntTrs with 56 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

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

obtained
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
by chaining
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2

obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12

obtained
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10

obtained
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
by chaining
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12

(8) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12

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

Moved arithmethic from lhss to constraints.

main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12

main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
was transformed to
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

(10) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

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

Moved arithmethic from constraints to rhss.

main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
was transformed to
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72

main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12

(12) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

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

Simplified expressions.

main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

(14) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72

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

Transformed 56 jbc graph edges to a weighted ITS with 56 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.

(16) Obligation:

IntTrs with 56 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

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

obtained
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
by chaining
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2

obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12

obtained
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10

obtained
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
by chaining
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12

(18) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12

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

Moved arithmethic from lhss to constraints.

main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

main_GE_320(o134, i61, 12, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63'
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12

main_GE_347(o134, i71, 10, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71
was transformed to
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

(20) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

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

Moved arithmethic from constraints to rhss.

main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
was transformed to
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72

main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i63', 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
was transformed to
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12

(22) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10

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

Simplified expressions.

main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12

(24) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_GE_320(o134, i61, x, i52, env, static) -{5,5}> main_GE_347(o134, i52 + 1, 10, env, static) :|: 12 <= i61 && 0 <= i52 && 0 < o134 && 1 <= i63' && i52 + 1 = i63' && x = 12
main_GE_320(o134, i60, x, i52, env, static) -{4,4}> main_Load_312(o134, i52, i60 + 1, env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12 && x = 12
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_347(o134, i71, x, env, static) -{5,5}> main_GE_320(o134, 3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && 0 < o134 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_347(o134, i72, iconst_10, env, static) -{0,0}> main_GE_350(o134, i72, 10, env, static) :|: 0 < o134 && iconst_10 = 10 && 10 <= i72 && 1 <= i72

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

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

(26) Obligation:

Set of 55 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 55 jbc graph edges to a weighted ITS with 55 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 55 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

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

obtained
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
by chaining
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_39(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_40(o2, env, static) -{1,1}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_10, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_GE_56(o2, iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_58(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_58(o2, iconst_0, env, static) -{1,1}> main_Store_60(o2, iconst_3, iconst_0, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Store_60(o2, iconst_3, iconst_0, env, static) -{1,1}> main_Load_62(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_62(o2, iconst_0, iconst_3, env, static) -{0,0}> main_Load_161(o2, iconst_0, iconst_3, env, static) :|: 0 < o2 && iconst_3 = 3 && iconst_0 = 0
main_Load_161(o70, iconst_0, i11, env, static) -{0,0}> main_Load_214(o70, iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0 && 0 < o70
main_Load_214(o94, i24, i25, env, static) -{0,0}> main_Load_263(o94, i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 < o94
main_Load_263(o114, i38, i39, env, static) -{0,0}> main_Load_312(o114, i38, i39, env, static) :|: 0 < o114 && 0 <= i38 && i38 <= 2

obtained
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
by chaining
main_Load_312(o134, i52, i53, env, static) -{1,1}> main_ConstantStackPush_314(o134, i53, i52, env, static) :|: 0 <= i52 && 0 < o134
main_ConstantStackPush_314(o134, i53, i52, env, static) -{1,1}> main_GE_320(o134, i53, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12

obtained
main_GE_320(o134, i61, 12, i52, env, static) -{10,10}> main_GE_320(o134, 3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
by chaining
main_GE_320(o134, i61, iconst_12, i52, env, static) -{0,0}> main_GE_322(o134, i61, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61
main_GE_322(o134, i61, iconst_12, i52, env, static) -{1,1}> main_Inc_328(o134, i52, env, static) :|: 0 <= i52 && 0 < o134 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_328(o134, i52, env, static) -{1,1}> main_JMP_332(o134, i63, env, static) :|: 0 <= i52 && 0 < o134 && 1 <= i63 && i52 + 1 = i63
main_JMP_332(o134, i63, env, static) -{1,1}> main_Load_335(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_Load_335(o134, i63, env, static) -{1,1}> main_ConstantStackPush_341(o134, i63, env, static) :|: 0 < o134 && 1 <= i63
main_ConstantStackPush_341(o134, i63, env, static) -{1,1}> main_GE_347(o134, i63, iconst_10, env, static) :|: 0 < o134 && 1 <= i63 && iconst_10 = 10
main_GE_347(o134, i71, iconst_10, env, static) -{0,0}> main_GE_349(o134, i71, iconst_10, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_349(o134, i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(o134, i71, env, static) :|: 0 < o134 && iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(o134, i71, env, static) -{1,1}> main_Store_364(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_364(o134, iconst_3, i71, env, static) -{1,1}> main_Load_366(o134, i71, iconst_3, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_366(o134, i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_367(o134, iconst_3, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_367(o134, iconst_3, i71, env, static) -{1,1}> main_GE_374(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_374(o134, iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_320(o134, iconst_3, iconst_12, i71, env, static) :|: 0 < o134 && iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

obtained
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_320(o134, i60, iconst_12, i52, env, static) -{0,0}> main_GE_321(o134, i60, iconst_12, i52, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_GE_321(o134, i60, iconst_12, i52, env, static) -{1,1}> main_Inc_324(o134, i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && 0 < o134 && i60 <= 11 && iconst_12 = 12
main_Inc_324(o134, i52, i60, env, static) -{1,1}> main_Inc_330(o134, i52, i62, env, static) :|: 0 <= i52 && 0 < o134 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_330(o134, i52, i62, env, static) -{1,1}> main_JMP_333(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_333(o134, i52, i64, env, static) -{1,1}> main_Load_340(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12
main_Load_340(o134, i52, i64, env, static) -{0,0}> main_Load_312(o134, i52, i64, env, static) :|: 0 <= i52 && 0 < o134 && i64 <= 12

(30) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{22,22}> main_Load_312(o2, 0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53, env, static) -{2,2}> main_GE_320(o134, i53, 12, i52, env, static) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, 12, i52, env, static) -{10,10}> main_GE_320(o134, 3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_GE_320(o134, i60, 12, i52, env, static) -{4,4}> main_Load_312(o134, i52, i64', env, static) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12

(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_2(x1, x2, x3) → main_ConstantStackPush_2(x1, x3)
main_Load_312(x1, x2, x3, x4, x5) → main_Load_312(x1, x2, x3)
main_GE_320(x1, x2, x3, x4, x5, x6) → main_GE_320(x1, x2, x4)

(32) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i64') :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12

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

Moved arithmethic from constraints to rhss.

main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i64') :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12

main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
was transformed to
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52

(34) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1

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

Simplified expressions.

main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + -1 + 2) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 + -1 = i62' && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + 1) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12

main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && 0 <= 2 && static''' <= static + 2 && 0 < o2 && 0 <= 0 && 0 <= static''' && 0 <= static && 0 <= 1 && 0 < 1 && 0 < 2 && 0 <= static'1
was transformed to
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

(36) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(o2, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{22,22}> main_Load_312(o2, 0, 3) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_Load_312(o134, i52, i53) -{2,2}> main_GE_320(o134, i53, i52) :|: 0 <= i52 && 0 < o134
main_GE_320(o134, i60, i52) -{4,4}> main_Load_312(o134, i52, i60 + 1) :|: i60 <= 11 && i64' <= 12 && i62' <= 10 && 0 <= i52 && 0 < o134 && i60 - 1 = i62' && i62' + 2 = i64' && i60 < 12
main_GE_320(o134, i61, i52) -{10,10}> main_GE_320(o134, 3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 < o134 && 0 <= i63' && 12 <= i61 && 0 <= i52

(37) koat Proof (EQUIVALENT transformation)

YES(?, 900*ar_0 + 114)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: ?, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: ?, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_ConstantStackPush_2) = 9*V_1
Pol(main_Load_312) = 9*V_1 - V_2
Pol(main_GE_320) = 9*V_1 - V_3
Pol(koat_start) = 9*V_1
orients all transitions weakly and the transition
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_312) = -V_3 + 12
Pol(main_GE_320) = -V_2 + 12
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-2) = ar_2
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-0) = ar_0
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-1) = 3
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\\ 1 <= i63' /\\ i63' < 10 /\\ i63' <= 9 /\\ 0 < ar_0 /\\ 0 <= i63' /\\ 12 <= ar_1 /\\ 0 <= ar_2 ]", 0-2) = 9
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-0) = ar_0
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-1) = 9
S("main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\\ i64' <= 12 /\\ i62' <= 10 /\\ 0 <= ar_2 /\\ 0 < ar_0 /\\ ar_1 - 1 = i62' /\\ i62' + 2 = i64' /\\ ar_1 < 12 ]", 0-2) = 12
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-0) = ar_0
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-1) = 12
S("main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\\ 0 < ar_0 ]", 0-2) = 9
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-1) = 0
S("main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\\ static''' <= ar_1 + 2 /\\ 0 < ar_0 /\\ 0 <= static''' /\\ 0 <= ar_1 /\\ 0 <= static'1 ]", 0-2) = 3
orients the transitions
main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
weakly and the transition
main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 135*ar_0 + 15, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 1, Cost: 22) main_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, 0, 3)) [ static'1 <= static''' + 1 /\ static''' <= ar_1 + 2 /\ 0 < ar_0 /\ 0 <= static''' /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 135*ar_0 + 16, Cost: 2) main_Load_312(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, ar_2, ar_1)) [ 0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 135*ar_0 + 15, Cost: 4) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_Load_312(ar_0, ar_2, ar_1 + 1)) [ ar_1 <= 11 /\ i64' <= 12 /\ i62' <= 10 /\ 0 <= ar_2 /\ 0 < ar_0 /\ ar_1 - 1 = i62' /\ i62' + 2 = i64' /\ ar_1 < 12 ]
(Comp: 9*ar_0, Cost: 10) main_GE_320(ar_0, ar_1, ar_2) -> Com_1(main_GE_320(ar_0, 3, ar_2 + 1)) [ ar_2 + 1 = i63' /\ 1 <= i63' /\ i63' < 10 /\ i63' <= 9 /\ 0 < ar_0 /\ 0 <= i63' /\ 12 <= ar_1 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 900*ar_0 + 114

Time: 0.114 sec (SMT: 0.102 sec)

(38) BOUNDS(CONSTANT, 114 + 900 * |o2|)