The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(34 + 13 * #1, 47)).

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 177 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)), 7 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 148 ms)
    ↳6 WeightedIntTrs
    ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 34 ms)
    ↳8 WeightedIntTrs
    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 44 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)), 3 ms)
↳16 JBCComplexityEdges
    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 144 ms)
    ↳18 WeightedIntTrs
        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 20 ms)
        ↳20 WeightedIntTrs
        ↳21 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳22 WeightedIntTrs
        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)
        ↳24 WeightedIntTrs
        ↳25 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳26 WeightedIntTrs
        ↳27 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 3 ms)
        ↳28 WeightedIntTrs
    ↳29 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 164 ms)
    ↳30 WeightedIntTrs
        ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 17 ms)
        ↳32 WeightedIntTrs
        ↳33 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳34 WeightedIntTrs
        ↳35 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳36 WeightedIntTrs
        ↳37 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 1 ms)
        ↳38 WeightedIntTrs
        ↳39 CESProof (⇔, 164 ms)
        ↳40 BOUNDS(CONSTANT, max(22 + 13 * #1, 35))

(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(int i, int x) {
		if (i > 0) {
			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(II)V: Graph of 64 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 49 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 49 jbc graph edges to a weighted ITS with 49 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 49 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && i79 < i75 && 1 <= i75 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

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

obtained
main_Load_1(i2, i3, env, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3, env, static'1) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 0 >= 0 && 1 <= i3 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 < i3 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12

obtained
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{13,13}> divBy_ConstantStackPush_273(i79', i80', i12, i21, env, static) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75
by chaining
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && i79 < i75 && 1 <= i75 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

(8) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, env, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3, env, static'1) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 0 >= 0 && 1 <= i3 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 < i3 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{13,13}> divBy_ConstantStackPush_273(i79', i80', i12, i21, env, static) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75

(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, x4) → main_Load_1(x1, x2, x4)
divBy_ConstantStackPush_273(x1, x2, x3, x4, x5, x6) → divBy_ConstantStackPush_273(x1, x2, x3, x4)

(10) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 0 >= 0 && 1 <= i3 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 < i3 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i80', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75

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

Moved arithmethic from constraints to rhss.

divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i80', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75
was transformed to
divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i64 + i79', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75

(12) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 0 >= 0 && 1 <= i3 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 < i3 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i64 + i79', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75

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

Simplified expressions.

divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i64 + i79', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 <= i79' && 0 < i79' && 0 <= i64 && i79' < i75
was transformed to
divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i64 + i79', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 < i79' && 0 <= i64 && i79' < i75

main_Load_1(i2, i3, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 0 >= 0 && 1 <= i3 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 < i3 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i2, i3, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 1 <= i3 && 0 <= static''' && static''' <= static + 2 && 0 < i3 && 0 <= static && 0 <= static'1

(14) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, static) -{23,23}> divBy_ConstantStackPush_273(i3, 0, i2, i3) :|: 0 < i2 && 1 <= i2 && static'1 <= static''' + 1 && 1 <= i3 && 0 <= static''' && static''' <= static + 2 && 0 < i3 && 0 <= static && 0 <= static'1
divBy_ConstantStackPush_273(i75, i64, i12, i21) -{13,13}> divBy_ConstantStackPush_273(i79', i64 + i79', i12, i21) :|: i64 + i79' = i80' && 1 <= i79' && 1 <= i75 && 1 <= i12 && 1 <= i21 && 0 <= i80' && 0 < i79' && 0 <= i64 && i79' < i75

(15) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)) transformation)

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

(16) Obligation:

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

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

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

(18) Obligation:

IntTrs with 52 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && i75 / iconst_2 = i79 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

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

obtained
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0

obtained
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
by chaining
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12

obtained
divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
by chaining
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12

obtained
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 / 2 = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
by chaining
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && i75 / iconst_2 = i79 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12

obtained
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89
by chaining
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

(20) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 / 2 = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Moved arithmethic from lhss to constraints.

divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
was transformed to
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0

(22) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 / 2 = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Removed div and mod.

divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 / 2 = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
was transformed to
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) :|: div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'

(24) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) :|: div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Moved arithmethic from constraints to rhss.

divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
was transformed to
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'

divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
was transformed to
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12

divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
was transformed to
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12

(26) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) :|: div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Simplified expressions.

divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
was transformed to
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && x = 0

divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i75 - 2 * div < 2 && i75 - 2 * div + 2 > 0 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
was transformed to
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i75 + -2 * div < 2 && 0 < i75 + -2 * div + 2 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'

main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89
was transformed to
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89

(28) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) :|: div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && x = 0
divBy_ConstantStackPush_273'(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i75 + -2 * div < 2 && 0 < i75 + -2 * div + 2 && div = i79' && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89

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

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

(30) Obligation:

IntTrs with 52 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && i79 < i75 && 1 <= i75 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

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

obtained
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_49(i2, i3, env, static) :|: 0 <= static
main_Load_49(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 >= 0
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{1,1}> main_LE_53(i2, i3, env, static) :|: 0 >= 0

obtained
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
by chaining
main_LE_53(i12, i3, env, static) -{0,0}> main_LE_55(i12, i3, env, static) :|: 1 <= i12
main_LE_55(i12, i3, env, static) -{1,1}> main_Load_59(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_59(i12, i3, env, static) -{1,1}> main_InvokeMethod_66(i12, i3, env, static) :|: 1 <= i12
main_InvokeMethod_66(i12, i3, env, static) -{1,1}> divBy_ConstantStackPush_69(i3, i12, env, static) :|: 1 <= i12
divBy_ConstantStackPush_69(i3, i12, env, static) -{1,1}> divBy_Store_80(iconst_0, i3, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Store_80(iconst_0, i3, i12, env, static) -{1,1}> divBy_Load_81(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12
divBy_Load_81(i3, iconst_0, i12, env, static) -{1,1}> divBy_LE_85(i3, iconst_0, i12, env, static) :|: iconst_0 = 0 && 1 <= i12

obtained
divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
by chaining
divBy_LE_85(i21, iconst_0, i12, env, static) -{0,0}> divBy_LE_89(i21, iconst_0, i12, env, static) :|: 1 <= i21 && iconst_0 = 0 && 1 <= i12
divBy_LE_89(i21, iconst_0, i12, env, static) -{1,1}> divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) :|: 1 <= i21 && 0 < i21 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_93(i21, iconst_0, i12, env, static) -{0,0}> divBy_ConstantStackPush_273(i21, iconst_0, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i12

obtained
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
by chaining
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{1,1}> divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Store_274(iconst_2, i75, i64, i12, i21, env, static) -{1,1}> divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_275(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_Load_276(i75, i64, iconst_2, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) :|: 1 <= i21 && 1 <= i75 && 0 <= i64 && iconst_2 = 2 && 1 <= i12
divBy_IntArithmetic_277(i75, iconst_2, i64, i12, i21, env, static) -{1,1}> divBy_Store_278(i79, i64, i12, i21, env, static) :|: 1 <= i21 && i79 < i75 && 1 <= i75 && 0 <= i64 && 0 <= i79 && iconst_2 = 2 && 1 <= i12
divBy_Store_278(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_279(i79, i64, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_279(i79, i64, i12, i21, env, static) -{1,1}> divBy_Load_280(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_Load_280(i64, i79, i12, i21, env, static) -{1,1}> divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i64 && 0 <= i79 && 1 <= i12
divBy_IntArithmetic_281(i64, i79, i12, i21, env, static) -{1,1}> divBy_Store_282(i80, i79, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i64 && 0 <= i79 && 1 <= i12 && i64 + i79 = i80
divBy_Store_282(i80, i79, i12, i21, env, static) -{1,1}> divBy_JMP_283(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_JMP_283(i79, i80, i12, i21, env, static) -{1,1}> divBy_Load_284(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12
divBy_Load_284(i79, i80, i12, i21, env, static) -{1,1}> divBy_LE_312(i79, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i79 && 1 <= i12

obtained
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89
by chaining
divBy_LE_312(i89, i80, i12, i21, env, static) -{0,0}> divBy_LE_314(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 <= i89 && 1 <= i12 && 1 <= i89
divBy_LE_314(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 0 < i89 && 1 <= i12 && 1 <= i89
divBy_ConstantStackPush_322(i89, i80, i12, i21, env, static) -{0,0}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= i80 && 1 <= i12 && 1 <= i89

(32) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Moved arithmethic from lhss to constraints.

divBy_LE_85(i21, 0, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0
was transformed to
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0

(34) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Moved arithmethic from constraints to rhss.

divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i80', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
was transformed to
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'

divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, iconst_0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
was transformed to
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12

divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(iconst_0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
was transformed to
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12

(36) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89

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

Simplified expressions.

divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && 0 <= 0 && x = 0
was transformed to
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && x = 0

main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89 && 0 <= i89
was transformed to
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89

(38) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
divBy_LE_312(iconst_0, i80, i12, i21, env, static) -{0,0}> divBy_LE_313(0, i80, i12, i21, env, static) :|: 1 <= i21 && 0 <= iconst_0 && 0 <= i80 && iconst_0 = 0 && 1 <= i12
divBy_LE_85(i20, iconst_0, i12, env, static) -{0,0}> divBy_LE_87(i20, 0, i12, env, static) :|: i20 <= 0 && iconst_0 = 0 && 1 <= i12
divBy_ConstantStackPush_273(i75, i64, i12, i21, env, static) -{12,12}> divBy_LE_312(i79', i64 + i79', i12, i21, env, static) :|: i79' < i75 && 1 <= i12 && 0 <= i64 && 0 <= i79' && 0 <= i80' && 1 <= i21 && 1 <= i75 && i64 + i79' = i80'
main_Load_1(i2, i3, env, static) -{16,16}> main_LE_53(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
divBy_LE_85(i21, x, i12, env, static) -{1,1}> divBy_ConstantStackPush_273(i21, 0, i12, i21, env, static) :|: 0 < i21 && 1 <= i12 && 1 <= i21 && x = 0
main_LE_53(i12, i3, env, static) -{6,6}> divBy_LE_85(i3, 0, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_53(i11, i3, env, static) -{0,0}> main_LE_54(i11, i3, env, static) :|: i11 <= 0
divBy_LE_312(i89, i80, i12, i21, env, static) -{1,1}> divBy_ConstantStackPush_273(i89, i80, i12, i21, env, static) :|: 0 <= i80 && 1 <= i89 && 1 <= i21 && 1 <= i12 && 0 < i89

(39) CESProof (EQUIVALENT transformation)

proved upper bound max(22 + 13 * #1, 35) using cofloco

(40) BOUNDS(CONSTANT, max(22 + 13 * #1, 35))