time complexity proof of /tmp/tmpZRunSa/costa09-example

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

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 200 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)), 15 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 124 ms)

    ↳6 WeightedIntTrs

    ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 55 ms)

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 23 ms)

    ↳10 WeightedIntTrs

    ↳11 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳12 WeightedIntTrs

    ↳13 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 153 ms)

    ↳16 BOUNDS(CONSTANT, 27 + 13 * |#0|)

↳17 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)), 9 ms)

↳18 JBCComplexityEdges

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 149 ms)

    ↳20 WeightedIntTrs

        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 40 ms)

        ↳22 WeightedIntTrs

        ↳23 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳24 WeightedIntTrs

        ↳25 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳26 WeightedIntTrs

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 179 ms)

    ↳28 WeightedIntTrs

        ↳29 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 44 ms)

        ↳30 WeightedIntTrs

        ↳31 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳32 WeightedIntTrs

        ↳33 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳34 WeightedIntTrs

        ↳35 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳36 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

package example_2;


public class Test {

	public static int divBy(int x){
		int r = 0;
		int y;
		while (x > 0) {
			y = 2;
			x = x/y;
			r = r + x;
		}
		return r;
	}

	public static void main(String[] args) {
		if (args.length > 0) {
		        int x = args[0].length();
			int r = divBy(x);
			// System.out.println("Result: " + r);
		}
		// else System.out.println("Error: Incorrect call");
	}
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 54 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(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_20(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_20(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_25(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_25(o2, env, static) -{0,0}> langle_clinit_rangle_New_27(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_27(o2, env, static) -{0,0}> langle_clinit_rangle_New_29(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_29(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_39(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_51(o2, env, static) -{0,0}> main_Load_52(o2, env, static) :|: 0 < o2
main_Load_52(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ArrayLength_55(o2, env, static) :|: 0 < o2
main_ArrayLength_55(a6, env, static) -{0,0}> main_ArrayLength_58(a6, i5, env, static) :|: i5 < a6 && 0 < a6 && 0 <= i5
main_ArrayLength_58(a6, i5, env, static) -{1,1}> main_LE_61(a6, i5, env, static) :|: 0 < a6 && 0 <= i5
main_LE_61(a6, i8, env, static) -{0,0}> main_LE_63(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 <= i8
main_LE_63(a6, i8, env, static) -{1,1}> main_Load_65(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 < i8
main_Load_65(a6, i8, env, static) -{1,1}> main_ConstantStackPush_68(a6, i8, env, static) :|: 1 <= i8 && 0 < a6
main_ConstantStackPush_68(a6, i8, env, static) -{1,1}> main_ArrayAccess_69(a6, iconst_0, i8, env, static) :|: 1 <= i8 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_69(a6, iconst_0, i8, env, static) -{1,1}> main_InvokeMethod_72(a6, o7, i8, env, static) :|: o7 < a6 && 1 <= i8 && iconst_0 = 0 && 0 <= o7 && 0 < a6 && iconst_0 < i8
main_InvokeMethod_72(a6, o10, i8, env, static) -{0,0}> main_InvokeMethod_74(a6, o10, i8, env, static) :|: 1 <= i8 && 0 <= o10 && 0 < a6 && 0 < o10
main_InvokeMethod_74(a6, o10, i8, env, static) -{1,1}> main_Store_77(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6 && 0 < o10 && i10 <= o10
main_Store_77(a6, i10, i8, env, static) -{1,1}> main_Load_80(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_Load_80(a6, i10, i8, env, static) -{1,1}> main_InvokeMethod_84(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_InvokeMethod_84(a6, i10, i8, env, static) -{1,1}> divBy_ConstantStackPush_86(i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
divBy_ConstantStackPush_86(i10, a6, i8, env, static) -{1,1}> divBy_Store_93(iconst_0, i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Store_93(iconst_0, i10, a6, i8, env, static) -{1,1}> divBy_Load_95(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_95(i10, iconst_0, a6, i8, env, static) -{0,0}> divBy_Load_275(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 0 <= iconst_0 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2 && i57 < i53
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

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

obtained
main_Load_1(o2, env, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5', env, static'1) :|: i10' <= o7' && 0 < o2 && 0 < i5' && 0 <= i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= 0 && 0 < 2 && 0 <= static'1 && i5' < o2 && 0 <= 1 && o7' < o2 && 0 < 1 && 0 <= static && 0 <= static''' && 0 <= o7' && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(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_20(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_20(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_25(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_25(o2, env, static) -{0,0}> langle_clinit_rangle_New_27(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_27(o2, env, static) -{0,0}> langle_clinit_rangle_New_29(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_29(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_39(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_51(o2, env, static) -{0,0}> main_Load_52(o2, env, static) :|: 0 < o2
main_Load_52(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ArrayLength_55(o2, env, static) :|: 0 < o2
main_ArrayLength_55(a6, env, static) -{0,0}> main_ArrayLength_58(a6, i5, env, static) :|: i5 < a6 && 0 < a6 && 0 <= i5
main_ArrayLength_58(a6, i5, env, static) -{1,1}> main_LE_61(a6, i5, env, static) :|: 0 < a6 && 0 <= i5
main_LE_61(a6, i8, env, static) -{0,0}> main_LE_63(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 <= i8
main_LE_63(a6, i8, env, static) -{1,1}> main_Load_65(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 < i8
main_Load_65(a6, i8, env, static) -{1,1}> main_ConstantStackPush_68(a6, i8, env, static) :|: 1 <= i8 && 0 < a6
main_ConstantStackPush_68(a6, i8, env, static) -{1,1}> main_ArrayAccess_69(a6, iconst_0, i8, env, static) :|: 1 <= i8 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_69(a6, iconst_0, i8, env, static) -{1,1}> main_InvokeMethod_72(a6, o7, i8, env, static) :|: o7 < a6 && 1 <= i8 && iconst_0 = 0 && 0 <= o7 && 0 < a6 && iconst_0 < i8
main_InvokeMethod_72(a6, o10, i8, env, static) -{0,0}> main_InvokeMethod_74(a6, o10, i8, env, static) :|: 1 <= i8 && 0 <= o10 && 0 < a6 && 0 < o10
main_InvokeMethod_74(a6, o10, i8, env, static) -{1,1}> main_Store_77(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6 && 0 < o10 && i10 <= o10
main_Store_77(a6, i10, i8, env, static) -{1,1}> main_Load_80(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_Load_80(a6, i10, i8, env, static) -{1,1}> main_InvokeMethod_84(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_InvokeMethod_84(a6, i10, i8, env, static) -{1,1}> divBy_ConstantStackPush_86(i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
divBy_ConstantStackPush_86(i10, a6, i8, env, static) -{1,1}> divBy_Store_93(iconst_0, i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Store_93(iconst_0, i10, a6, i8, env, static) -{1,1}> divBy_Load_95(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_95(i10, iconst_0, a6, i8, env, static) -{0,0}> divBy_Load_275(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 0 <= iconst_0 && 1 <= i8 && iconst_0 = 0 && 0 < a6

obtained
divBy_Load_275(i42, i47, a25, i8, env, static) -{13,13}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42
by chaining
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2 && i57 < i53
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

(8) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, env, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5', env, static'1) :|: i10' <= o7' && 0 < o2 && 0 < i5' && 0 <= i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= 0 && 0 < 2 && 0 <= static'1 && i5' < o2 && 0 <= 1 && o7' < o2 && 0 < 1 && 0 <= static && 0 <= static''' && 0 <= o7' && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
divBy_Load_275(i42, i47, a25, i8, env, static) -{13,13}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42

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

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

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
divBy_Load_275(x1, x2, x3, x4, x5, x6) → divBy_Load_275(x1, x2, x3, x4)

(10) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5') :|: i10' <= o7' && 0 < o2 && 0 < i5' && 0 <= i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= 0 && 0 < 2 && 0 <= static'1 && i5' < o2 && 0 <= 1 && o7' < o2 && 0 < 1 && 0 <= static && 0 <= static''' && 0 <= o7' && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i58', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42

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

Moved arithmethic from constraints to rhss.

divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i58', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42
was transformed to
divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i47 + i57', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42

(12) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i47 + i57', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42
main_Load_1(o2, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5') :|: i10' <= o7' && 0 < o2 && 0 < i5' && 0 <= i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= 0 && 0 < 2 && 0 <= static'1 && i5' < o2 && 0 <= 1 && o7' < o2 && 0 < 1 && 0 <= static && 0 <= static''' && 0 <= o7' && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i47 + i57', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 <= i42 && 0 < i42 && i57' < i42
was transformed to
divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i47 + i57', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 < i42 && i57' < i42

main_Load_1(o2, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5') :|: i10' <= o7' && 0 < o2 && 0 < i5' && 0 <= i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= 0 && 0 < 2 && 0 <= static'1 && i5' < o2 && 0 <= 1 && o7' < o2 && 0 < 1 && 0 <= static && 0 <= static''' && 0 <= o7' && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(o2, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5') :|: i10' <= o7' && 0 < o2 && 0 < i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= static'1 && i5' < o2 && o7' < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1

(14) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, static) -{27,27}> divBy_Load_275(i10', 0, o2, i5') :|: i10' <= o7' && 0 < o2 && 0 < i5' && 1 <= i5' && 0 < o7' && 0 <= i10' && 0 <= static'1 && i5' < o2 && o7' < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1
divBy_Load_275(i42, i47, a25, i8) -{13,13}> divBy_Load_275(i57', i47 + i57', a25, i8) :|: 1 <= i42 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 0 < i42 && i57' < i42

(15) koat Proof (EQUIVALENT transformation)

YES(?, 13*ar_0 + 27)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i10', 0, ar_0, i5')) [ i10' <= o7' /\ 0 < ar_0 /\ 0 < i5' /\ 1 <= i5' /\ 0 < o7' /\ 0 <= i10' /\ 0 <= static'1 /\ i5' < ar_0 /\ o7' < ar_0 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 13) divBy_Load_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i57', ar_1 + i57', ar_2, ar_3)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1 + i57' = i58' /\ 0 <= i58' /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 0 <= i57' /\ 0 < ar_0 /\ i57' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i10', 0, ar_0, i5')) [ i10' <= o7' /\ 0 < ar_0 /\ 0 < i5' /\ 1 <= i5' /\ 0 < o7' /\ 0 <= i10' /\ 0 <= static'1 /\ i5' < ar_0 /\ o7' < ar_0 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 13) divBy_Load_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i57', ar_1 + i57', ar_2, ar_3)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1 + i57' = i58' /\ 0 <= i58' /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 0 <= i57' /\ 0 < ar_0 /\ i57' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = V_1
Pol(divBy_Load_275) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
divBy_Load_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i57', ar_1 + i57', ar_2, ar_3)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1 + i57' = i58' /\ 0 <= i58' /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 0 <= i57' /\ 0 < ar_0 /\ i57' < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i10', 0, ar_0, i5')) [ i10' <= o7' /\ 0 < ar_0 /\ 0 < i5' /\ 1 <= i5' /\ 0 < o7' /\ 0 <= i10' /\ 0 <= static'1 /\ i5' < ar_0 /\ o7' < ar_0 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ static'1 <= static''' + 1 ]
(Comp: ar_0, Cost: 13) divBy_Load_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(divBy_Load_275(i57', ar_1 + i57', ar_2, ar_3)) [ 1 <= ar_0 /\ 0 < ar_2 /\ ar_1 + i57' = i58' /\ 0 <= i58' /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 0 <= i57' /\ 0 < ar_0 /\ i57' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 13*ar_0 + 27

Time: 0.173 sec (SMT: 0.164 sec)

(16) BOUNDS(CONSTANT, 27 + 13 * |#0|)

(17) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)) transformation)

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

(18) Obligation:

Set of 57 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

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

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

(20) Obligation:

IntTrs with 57 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(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_20(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_20(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_25(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_25(o2, env, static) -{0,0}> langle_clinit_rangle_New_27(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_27(o2, env, static) -{0,0}> langle_clinit_rangle_New_29(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_29(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_39(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_51(o2, env, static) -{0,0}> main_Load_52(o2, env, static) :|: 0 < o2
main_Load_52(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ArrayLength_55(o2, env, static) :|: 0 < o2
main_ArrayLength_55(a6, env, static) -{0,0}> main_ArrayLength_58(a6, i5, env, static) :|: i5 < a6 && 0 < a6 && 0 <= i5
main_ArrayLength_58(a6, i5, env, static) -{1,1}> main_LE_61(a6, i5, env, static) :|: 0 < a6 && 0 <= i5
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_LE_61(a6, i8, env, static) -{0,0}> main_LE_63(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 <= i8
main_LE_63(a6, i8, env, static) -{1,1}> main_Load_65(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 < i8
main_Load_65(a6, i8, env, static) -{1,1}> main_ConstantStackPush_68(a6, i8, env, static) :|: 1 <= i8 && 0 < a6
main_ConstantStackPush_68(a6, i8, env, static) -{1,1}> main_ArrayAccess_69(a6, iconst_0, i8, env, static) :|: 1 <= i8 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_69(a6, iconst_0, i8, env, static) -{1,1}> main_InvokeMethod_72(a6, o7, i8, env, static) :|: o7 < a6 && 1 <= i8 && iconst_0 = 0 && 0 <= o7 && 0 < a6 && iconst_0 < i8
main_InvokeMethod_72(a6, o10, i8, env, static) -{0,0}> main_InvokeMethod_74(a6, o10, i8, env, static) :|: 1 <= i8 && 0 <= o10 && 0 < a6 && 0 < o10
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
main_InvokeMethod_74(a6, o10, i8, env, static) -{1,1}> main_Store_77(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6 && 0 < o10 && i10 <= o10
main_Store_77(a6, i10, i8, env, static) -{1,1}> main_Load_80(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_Load_80(a6, i10, i8, env, static) -{1,1}> main_InvokeMethod_84(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_InvokeMethod_84(a6, i10, i8, env, static) -{1,1}> divBy_ConstantStackPush_86(i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
divBy_ConstantStackPush_86(i10, a6, i8, env, static) -{1,1}> divBy_Store_93(iconst_0, i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Store_93(iconst_0, i10, a6, i8, env, static) -{1,1}> divBy_Load_95(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_95(i10, iconst_0, a6, i8, env, static) -{0,0}> divBy_Load_275(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 0 <= iconst_0 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2 && i57 < i53
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

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

obtained
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(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_20(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_20(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_25(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_25(o2, env, static) -{0,0}> langle_clinit_rangle_New_27(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_27(o2, env, static) -{0,0}> langle_clinit_rangle_New_29(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_29(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_39(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_51(o2, env, static) -{0,0}> main_Load_52(o2, env, static) :|: 0 < o2
main_Load_52(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ArrayLength_55(o2, env, static) :|: 0 < o2
main_ArrayLength_55(a6, env, static) -{0,0}> main_ArrayLength_58(a6, i5, env, static) :|: i5 < a6 && 0 < a6 && 0 <= i5
main_ArrayLength_58(a6, i5, env, static) -{1,1}> main_LE_61(a6, i5, env, static) :|: 0 < a6 && 0 <= i5

obtained
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
by chaining
main_LE_61(a6, i8, env, static) -{0,0}> main_LE_63(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 <= i8
main_LE_63(a6, i8, env, static) -{1,1}> main_Load_65(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 < i8
main_Load_65(a6, i8, env, static) -{1,1}> main_ConstantStackPush_68(a6, i8, env, static) :|: 1 <= i8 && 0 < a6
main_ConstantStackPush_68(a6, i8, env, static) -{1,1}> main_ArrayAccess_69(a6, iconst_0, i8, env, static) :|: 1 <= i8 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_69(a6, iconst_0, i8, env, static) -{1,1}> main_InvokeMethod_72(a6, o7, i8, env, static) :|: o7 < a6 && 1 <= i8 && iconst_0 = 0 && 0 <= o7 && 0 < a6 && iconst_0 < i8

obtained
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
by chaining
main_InvokeMethod_72(a6, o10, i8, env, static) -{0,0}> main_InvokeMethod_74(a6, o10, i8, env, static) :|: 1 <= i8 && 0 <= o10 && 0 < a6 && 0 < o10
main_InvokeMethod_74(a6, o10, i8, env, static) -{1,1}> main_Store_77(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6 && 0 < o10 && i10 <= o10
main_Store_77(a6, i10, i8, env, static) -{1,1}> main_Load_80(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_Load_80(a6, i10, i8, env, static) -{1,1}> main_InvokeMethod_84(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_InvokeMethod_84(a6, i10, i8, env, static) -{1,1}> divBy_ConstantStackPush_86(i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
divBy_ConstantStackPush_86(i10, a6, i8, env, static) -{1,1}> divBy_Store_93(iconst_0, i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Store_93(iconst_0, i10, a6, i8, env, static) -{1,1}> divBy_Load_95(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_95(i10, iconst_0, a6, i8, env, static) -{0,0}> divBy_Load_275(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 0 <= iconst_0 && 1 <= i8 && iconst_0 = 0 && 0 < a6

obtained
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53
by chaining
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2 && i57 < i53
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

(22) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53

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

Moved arithmethic from constraints to rhss.

divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
was transformed to
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25

divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53
was transformed to
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53

main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6

main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, 0, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6

(24) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, 0, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6

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

Simplified expressions.

main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
was transformed to
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8

main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && static''' <= static + 2 && 0 <= static''' && 0 <= static && i5' < o2 && 0 <= static'1

main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
was transformed to
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 < a6 && 0 <= o7' && o7' < a6

divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: 0 <= i53 && 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53
was transformed to
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53

(26) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && static''' <= static + 2 && 0 <= static''' && 0 <= static && i5' < o2 && 0 <= static'1
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: 0 < a25 && i47 + i57' = i58' && 0 <= i58' && 0 <= i47 && 1 <= i8 && 0 <= i57' && 1 <= i53 && 0 < i53 && i57' < i53
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, 0, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25

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

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

(28) Obligation:

IntTrs with 57 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(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_20(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_20(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_23(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_25(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_25(o2, env, static) -{0,0}> langle_clinit_rangle_New_27(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_27(o2, env, static) -{0,0}> langle_clinit_rangle_New_29(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_29(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_30(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_36(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_39(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_39(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_51(o2, env, static) -{0,0}> main_Load_52(o2, env, static) :|: 0 < o2
main_Load_52(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ArrayLength_55(o2, env, static) :|: 0 < o2
main_ArrayLength_55(a6, env, static) -{0,0}> main_ArrayLength_58(a6, i5, env, static) :|: i5 < a6 && 0 < a6 && 0 <= i5
main_ArrayLength_58(a6, i5, env, static) -{1,1}> main_LE_61(a6, i5, env, static) :|: 0 < a6 && 0 <= i5
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_LE_61(a6, i8, env, static) -{0,0}> main_LE_63(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 <= i8
main_LE_63(a6, i8, env, static) -{1,1}> main_Load_65(a6, i8, env, static) :|: 1 <= i8 && 0 < a6 && 0 < i8
main_Load_65(a6, i8, env, static) -{1,1}> main_ConstantStackPush_68(a6, i8, env, static) :|: 1 <= i8 && 0 < a6
main_ConstantStackPush_68(a6, i8, env, static) -{1,1}> main_ArrayAccess_69(a6, iconst_0, i8, env, static) :|: 1 <= i8 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_69(a6, iconst_0, i8, env, static) -{1,1}> main_InvokeMethod_72(a6, o7, i8, env, static) :|: o7 < a6 && 1 <= i8 && iconst_0 = 0 && 0 <= o7 && 0 < a6 && iconst_0 < i8
main_InvokeMethod_72(a6, o10, i8, env, static) -{0,0}> main_InvokeMethod_74(a6, o10, i8, env, static) :|: 1 <= i8 && 0 <= o10 && 0 < a6 && 0 < o10
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
main_InvokeMethod_74(a6, o10, i8, env, static) -{1,1}> main_Store_77(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6 && 0 < o10 && i10 <= o10
main_Store_77(a6, i10, i8, env, static) -{1,1}> main_Load_80(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_Load_80(a6, i10, i8, env, static) -{1,1}> main_InvokeMethod_84(a6, i10, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
main_InvokeMethod_84(a6, i10, i8, env, static) -{1,1}> divBy_ConstantStackPush_86(i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && 0 < a6
divBy_ConstantStackPush_86(i10, a6, i8, env, static) -{1,1}> divBy_Store_93(iconst_0, i10, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Store_93(iconst_0, i10, a6, i8, env, static) -{1,1}> divBy_Load_95(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_95(i10, iconst_0, a6, i8, env, static) -{0,0}> divBy_Load_275(i10, iconst_0, a6, i8, env, static) :|: 0 <= i10 && 0 <= iconst_0 && 1 <= i8 && iconst_0 = 0 && 0 < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: i53 / iconst_2 = i57 && 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

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

obtained
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 / 2 = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
by chaining
divBy_LE_280(i53, i47, a25, i8, env, static) -{0,0}> divBy_LE_283(i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i53
divBy_LE_283(i53, i47, a25, i8, env, static) -{1,1}> divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) :|: 0 < i53 && 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25
divBy_ConstantStackPush_287(i53, i47, a25, i8, env, static) -{1,1}> divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_291(iconst_2, i53, i47, a25, i8, env, static) -{1,1}> divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_295(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Load_301(i53, i47, iconst_2, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) :|: 1 <= i53 && 1 <= i8 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_IntArithmetic_305(i53, iconst_2, i47, a25, i8, env, static) -{1,1}> divBy_Store_307(i57, i47, a25, i8, env, static) :|: i53 / iconst_2 = i57 && 1 <= i53 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25 && iconst_2 = 2
divBy_Store_307(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_309(i57, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_309(i57, i47, a25, i8, env, static) -{1,1}> divBy_Load_311(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_Load_311(i47, i57, a25, i8, env, static) -{1,1}> divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 < a25
divBy_IntArithmetic_313(i47, i57, a25, i8, env, static) -{1,1}> divBy_Store_315(i58, i57, a25, i8, env, static) :|: i47 + i57 = i58 && 1 <= i8 && 0 <= i57 && 0 <= i47 && 0 <= i58 && 0 < a25
divBy_Store_315(i58, i57, a25, i8, env, static) -{1,1}> divBy_JMP_317(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_JMP_317(i57, i58, a25, i8, env, static) -{1,1}> divBy_Load_323(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25
divBy_Load_323(i57, i58, a25, i8, env, static) -{0,0}> divBy_Load_275(i57, i58, a25, i8, env, static) :|: 1 <= i8 && 0 <= i57 && 0 <= i58 && 0 < a25

(30) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 / 2 = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

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

Removed div and mod.

divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 / 2 = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
was transformed to
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

(32) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(iconst_0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, NULL, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6

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

Moved arithmethic from constraints to rhss.

divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i58', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
was transformed to
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

(34) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8 && 0 <= 0 && 0 <= o10
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && 0 <= 2 && static''' <= static + 2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && i5' < o2 && 0 <= static'1 && 0 < 2
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 <= i8 && 0 < a6 && 0 <= o7' && o7' < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, 0, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

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

Simplified expressions.

divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: i53 - 2 * div < 2 && i53 - 2 * div + 2 > 0 && div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
was transformed to
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: i53 + -2 * div < 2 && 0 < i53 + -2 * div + 2 && div = i57' && 0 < a25 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i53 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
was transformed to
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53

(36) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{17,17}> main_LE_61(o2, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 < o2 && 0 <= i5' && static''' <= static + 2 && 0 <= static''' && 0 <= static && i5' < o2 && 0 <= static'1
divBy_LE_280(i53, i47, a25, i8, env, static) -{12,12}> divBy_LE_280'(i53, i47, a25, i8, env, static) :|: div = i57' && 0 < a25 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
divBy_LE_280'(i53, i47, a25, i8, env, static) -{12,12}> divBy_Load_275(i57', i47 + i57', a25, i8, env, static) :|: i53 + -2 * div < 2 && 0 < i53 + -2 * div + 2 && div = i57' && 0 < a25 && 0 <= i58' && i47 + i57' = i58' && 1 <= i8 && 0 <= i57' && 0 <= i47 && 0 < i53 && 1 <= i53
main_InvokeMethod_72(a6, NULL, i8, env, static) -{0,0}> main_InvokeMethod_75(a6, 0, i8, env, static) :|: NULL = 0 && 1 <= i8 && 0 <= NULL && 0 < a6
divBy_Load_275(i42, i47, a25, i8, env, static) -{1,1}> divBy_LE_280(i42, i47, a25, i8, env, static) :|: 1 <= i8 && 0 <= i47 && 0 < a25 && 0 <= i42
main_InvokeMethod_72(a6, o10, i8, env, static) -{6,6}> divBy_Load_275(i10', 0, a6, i8, env, static) :|: i10' <= o10 && 0 < a6 && 0 < o10 && 0 <= i10' && 1 <= i8
main_LE_61(a6, i8, env, static) -{4,4}> main_InvokeMethod_72(a6, o7', i8, env, static) :|: 1 <= i8 && 0 < i8 && 0 < a6 && 0 <= o7' && o7' < a6
main_LE_61(a6, iconst_0, env, static) -{0,0}> main_LE_62(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
divBy_LE_280(iconst_0, i47, a25, i8, env, static) -{0,0}> divBy_LE_282(0, i47, a25, i8, env, static) :|: 0 <= iconst_0 && 1 <= i8 && 0 <= i47 && iconst_0 = 0 && 0 < a25