time complexity proof of /tmp/tmp3ZMLlC/Test2.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

        ↳15 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 15 ms)

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 133 ms)

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

        ↳21 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)), 0 ms)

↳28 JBCComplexityEdges

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

    ↳30 WeightedIntTrs

    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 36 ms)

    ↳32 WeightedIntTrs

    ↳33 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 31 ms)

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 833 ms)

    ↳40 BOUNDS(CONSTANT, 35503 + 605 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Test2 {
    public static void main(int i) {
	iter(i, i % 5, i % 4);
    }

    private static void iter(int x, int y, int z) {
	while (x + y + 3 * z >= 0) {
	    if (x > y)
		x--;
	    else if (y > z) {
		x++;
		y -= 2;
	    }
	    else if (y <= z) {
		x = add(x, 1);
		y = add(y, 1);
		z = z - 1;
	    }
	}
    }

    private static int add(int v, int w) {
	return v + w;
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 100 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4 && i2 % iconst_5 = i4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i2 % iconst_4 = i6 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0
iter_Load_1562(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1563(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1563(i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) :|: i628 + i632 = i639
iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) :|: iconst_3 = 3
iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) -{1,1}> iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) :|: iconst_3 * i471 = i640 && iconst_3 = 3
iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) -{1,1}> iter_LT_1569(i641, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1571(i647, i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_LT_1571(i647, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1573(i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_Load_1573(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1575(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1575(i628, i632, i471, i126, env, static) -{1,1}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1578(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1579(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_LE_1578(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1580(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1579(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1581(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_Load_1580(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1582(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1581(i628, i632, i471, i126, env, static) -{1,1}> iter_JMP_1583(i648, i632, i471, i126, env, static) :|: i628 + -1 = i648
iter_Load_1582(i632, i628, i471, i126, env, static) -{1,1}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_JMP_1583(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1585(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1586(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1587(i632, i471, i628, i126, env, static) :|: i471 < i632
iter_Load_1585(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1588(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1586(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1589(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_LE_1587(i632, i471, i628, i126, env, static) -{1,1}> iter_Inc_1590(i628, i632, i471, i126, env, static) :|: i471 < i632
iter_Load_1588(i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1589(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1592(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1590(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1593(i652, i632, i471, i126, env, static) :|: i628 + 1 = i652
iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) :|: i648 + i632 = i653
iter_Load_1592(i632, i628, i471, i126, env, static) -{1,1}> iter_GT_1595(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_Inc_1593(i652, i632, i471, i126, env, static) -{1,1}> iter_JMP_1596(i652, i656, i471, i126, env, static) :|: i632 + -2 = i656
iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_GT_1595(i632, i471, i628, i126, env, static) -{0,0}> iter_GT_1598(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_JMP_1596(i652, i656, i471, i126, env, static) -{1,1}> iter_Load_1599(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_GT_1598(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1601(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_Load_1599(i652, i656, i471, i126, env, static) -{0,0}> iter_Load_1562(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) -{0,0}> iter_IntArithmetic_1567(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_Load_1601(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Return_1607(i665, i632, i471, i126, env, static) :|: i628 + iconst_1 = i665 && iconst_1 = 1
add_Return_1607(i665, i632, i471, i126, env, static) -{1,1}> iter_Store_1608(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Store_1608(i665, i632, i471, i126, env, static) -{1,1}> iter_Load_1609(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1609(i665, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Return_1615(i672, i665, i471, i126, env, static) :|: iconst_1 = 1 && i632 + iconst_1 = i672
add_Return_1615(i672, i665, i471, i126, env, static) -{1,1}> iter_Store_1616(i672, i665, i471, i126, env, static) :|: 0 >= 0
iter_Store_1616(i672, i665, i471, i126, env, static) -{1,1}> iter_Load_1617(i665, i672, i471, i126, env, static) :|: 0 >= 0
iter_Load_1617(i665, i672, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) -{1,1}> iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) :|: iconst_1 = 1
iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) -{1,1}> iter_Store_1620(i676, i665, i672, i126, env, static) :|: i471 - iconst_1 = i676 && iconst_1 = 1
iter_Store_1620(i676, i665, i672, i126, env, static) -{1,1}> iter_JMP_1621(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_JMP_1621(i665, i672, i676, i126, env, static) -{1,1}> iter_Load_1622(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_Load_1622(i665, i672, i676, i126, env, static) -{0,0}> iter_Load_1562(i665, i672, i676, i126, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 % 4 = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 % 5 = i4' && 0 < 2
by chaining
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4 && i2 % iconst_5 = i4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i2 % iconst_4 = i6 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0

obtained
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
by chaining
iter_Load_1562(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1563(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1563(i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) :|: i628 + i632 = i639
iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) :|: iconst_3 = 3

obtained
iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640
by chaining
iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) -{1,1}> iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) :|: iconst_3 * i471 = i640 && iconst_3 = 3
iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) -{1,1}> iter_LT_1569(i641, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641

obtained
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
by chaining
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1571(i647, i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_LT_1571(i647, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1573(i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_Load_1573(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1575(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1575(i628, i632, i471, i126, env, static) -{1,1}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0

obtained
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
by chaining
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1579(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_LE_1579(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1581(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_Inc_1581(i628, i632, i471, i126, env, static) -{1,1}> iter_JMP_1583(i648, i632, i471, i126, env, static) :|: i628 + -1 = i648
iter_JMP_1583(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1585(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1585(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1588(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1588(i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) :|: i648 + i632 = i653
iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) -{0,0}> iter_IntArithmetic_1567(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3

obtained
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
by chaining
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1578(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1578(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1580(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_Load_1580(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1582(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Load_1582(i632, i628, i471, i126, env, static) -{1,1}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0

obtained
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
by chaining
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1587(i632, i471, i628, i126, env, static) :|: i471 < i632
iter_LE_1587(i632, i471, i628, i126, env, static) -{1,1}> iter_Inc_1590(i628, i632, i471, i126, env, static) :|: i471 < i632
iter_Inc_1590(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1593(i652, i632, i471, i126, env, static) :|: i628 + 1 = i652
iter_Inc_1593(i652, i632, i471, i126, env, static) -{1,1}> iter_JMP_1596(i652, i656, i471, i126, env, static) :|: i632 + -2 = i656
iter_JMP_1596(i652, i656, i471, i126, env, static) -{1,1}> iter_Load_1599(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_Load_1599(i652, i656, i471, i126, env, static) -{0,0}> iter_Load_1562(i652, i656, i471, i126, env, static) :|: 0 >= 0

obtained
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
by chaining
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1586(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_LE_1586(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1589(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_Load_1589(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1592(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Load_1592(i632, i628, i471, i126, env, static) -{1,1}> iter_GT_1595(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_GT_1595(i632, i471, i628, i126, env, static) -{0,0}> iter_GT_1598(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_GT_1598(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1601(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_Load_1601(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Return_1607(i665, i632, i471, i126, env, static) :|: i628 + iconst_1 = i665 && iconst_1 = 1
add_Return_1607(i665, i632, i471, i126, env, static) -{1,1}> iter_Store_1608(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Store_1608(i665, i632, i471, i126, env, static) -{1,1}> iter_Load_1609(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1609(i665, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Return_1615(i672, i665, i471, i126, env, static) :|: iconst_1 = 1 && i632 + iconst_1 = i672
add_Return_1615(i672, i665, i471, i126, env, static) -{1,1}> iter_Store_1616(i672, i665, i471, i126, env, static) :|: 0 >= 0
iter_Store_1616(i672, i665, i471, i126, env, static) -{1,1}> iter_Load_1617(i665, i672, i471, i126, env, static) :|: 0 >= 0
iter_Load_1617(i665, i672, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) -{1,1}> iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) :|: iconst_1 = 1
iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) -{1,1}> iter_Store_1620(i676, i665, i672, i126, env, static) :|: i471 - iconst_1 = i676 && iconst_1 = 1
iter_Store_1620(i676, i665, i672, i126, env, static) -{1,1}> iter_JMP_1621(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_JMP_1621(i665, i672, i676, i126, env, static) -{1,1}> iter_Load_1622(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_Load_1622(i665, i672, i676, i126, env, static) -{0,0}> iter_Load_1562(i665, i672, i676, i126, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 % 4 = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 % 5 = i4' && 0 < 2
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

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

Moved arithmethic from lhss to constraints.

iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640
was transformed to
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 % 4 = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 % 5 = i4' && 0 < 2
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1

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

Removed div and mod.

main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 % 4 = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 % 5 = i4' && 0 < 2
was transformed to
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2

(12) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

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

Moved arithmethic from constraints to rhss.

iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
was transformed to
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'

iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
was transformed to
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i639 + i640, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3

iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
was transformed to
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'

main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
was transformed to
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i2 - 5 * div1, i2 - 4 * div, i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2

iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
was transformed to
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, 3, i471, i628 + -1, i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'

iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
was transformed to
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

(14) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i639 + i640, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i2 - 5 * div1, i2 - 4 * div, i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, 3, i471, i628 + -1, i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1

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

Simplified expressions.

iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
was transformed to
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: i628 <= i632

iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
was transformed to
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: i628 + i632 = i639'

iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
was transformed to
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 - 2, i471, i126, env, static) :|: i471 < i632 && i632 - 2 = i656' && i628 + 1 = i652'

iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, 3, i471, i628 + -1, i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
was transformed to
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 - 1 + i632, 3, i471, i628 - 1, i632, i126, env, static) :|: i632 < i628 && i628 - 1 = i648' && i648' + i632 = i653'

iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
was transformed to
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 <= i647

main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
was transformed to
main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 + -4 * div = i6' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 + -5 * div1 = i4'

main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i2 - 5 * div1, i2 - 4 * div, i2, env, static'1) :|: i2 - 5 * div1 < 5 && i2 - 5 * div1 + 5 > 0 && i2 - 4 * div < 4 && i2 - 4 * div + 4 > 0 && 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 - 4 * div = i6' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 - 5 * div1 = i4' && 0 < 2
was transformed to
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i2 + -5 * div1, i2 + -4 * div, i2, env, static'1) :|: i2 + -5 * div1 < 5 && 0 < i2 + -5 * div1 + 5 && i2 + -4 * div < 4 && 0 < i2 + -4 * div + 4 && i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 + -4 * div = i6' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 + -5 * div1 = i4'

iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
was transformed to
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

(16) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{23,23}> main_Load_2'(i2, env, static) :|: i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 + -4 * div = i6' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 + -5 * div1 = i4'
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 - 2, i471, i126, env, static) :|: i471 < i632 && i632 - 2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i639 + i640, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 - 1 + i632, 3, i471, i628 - 1, i632, i126, env, static) :|: i632 < i628 && i628 - 1 = i648' && i648' + i632 = i653'
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: i628 + i632 = i639'
main_Load_2'(i2, env, static) -{23,23}> iter_Load_1562(i2, i2 + -5 * div1, i2 + -4 * div, i2, env, static'1) :|: i2 + -5 * div1 < 5 && 0 < i2 + -5 * div1 + 5 && i2 + -4 * div < 4 && 0 < i2 + -4 * div + 4 && i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && i2 + -4 * div = i6' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && i2 + -5 * div1 = i4'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: i628 <= i632
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 <= i647

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

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

(18) Obligation:

IntTrs with 100 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0
iter_Load_1562(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1563(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1563(i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) :|: i628 + i632 = i639
iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) :|: iconst_3 = 3
iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) -{1,1}> iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) :|: iconst_3 * i471 = i640 && iconst_3 = 3
iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) -{1,1}> iter_LT_1569(i641, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1571(i647, i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_LT_1571(i647, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1573(i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_Load_1573(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1575(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1575(i628, i632, i471, i126, env, static) -{1,1}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1578(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1579(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_LE_1578(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1580(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1579(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1581(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_Load_1580(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1582(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1581(i628, i632, i471, i126, env, static) -{1,1}> iter_JMP_1583(i648, i632, i471, i126, env, static) :|: i628 + -1 = i648
iter_Load_1582(i632, i628, i471, i126, env, static) -{1,1}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_JMP_1583(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1585(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1586(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1587(i632, i471, i628, i126, env, static) :|: i471 < i632
iter_Load_1585(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1588(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1586(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1589(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_LE_1587(i632, i471, i628, i126, env, static) -{1,1}> iter_Inc_1590(i628, i632, i471, i126, env, static) :|: i471 < i632
iter_Load_1588(i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1589(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1592(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1590(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1593(i652, i632, i471, i126, env, static) :|: i628 + 1 = i652
iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) :|: i648 + i632 = i653
iter_Load_1592(i632, i628, i471, i126, env, static) -{1,1}> iter_GT_1595(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_Inc_1593(i652, i632, i471, i126, env, static) -{1,1}> iter_JMP_1596(i652, i656, i471, i126, env, static) :|: i632 + -2 = i656
iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_GT_1595(i632, i471, i628, i126, env, static) -{0,0}> iter_GT_1598(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_JMP_1596(i652, i656, i471, i126, env, static) -{1,1}> iter_Load_1599(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_GT_1598(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1601(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_Load_1599(i652, i656, i471, i126, env, static) -{0,0}> iter_Load_1562(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) -{0,0}> iter_IntArithmetic_1567(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_Load_1601(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Return_1607(i665, i632, i471, i126, env, static) :|: i628 + iconst_1 = i665 && iconst_1 = 1
add_Return_1607(i665, i632, i471, i126, env, static) -{1,1}> iter_Store_1608(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Store_1608(i665, i632, i471, i126, env, static) -{1,1}> iter_Load_1609(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1609(i665, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Return_1615(i672, i665, i471, i126, env, static) :|: iconst_1 = 1 && i632 + iconst_1 = i672
add_Return_1615(i672, i665, i471, i126, env, static) -{1,1}> iter_Store_1616(i672, i665, i471, i126, env, static) :|: 0 >= 0
iter_Store_1616(i672, i665, i471, i126, env, static) -{1,1}> iter_Load_1617(i665, i672, i471, i126, env, static) :|: 0 >= 0
iter_Load_1617(i665, i672, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) -{1,1}> iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) :|: iconst_1 = 1
iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) -{1,1}> iter_Store_1620(i676, i665, i672, i126, env, static) :|: i471 - iconst_1 = i676 && iconst_1 = 1
iter_Store_1620(i676, i665, i672, i126, env, static) -{1,1}> iter_JMP_1621(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_JMP_1621(i665, i672, i676, i126, env, static) -{1,1}> iter_Load_1622(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_Load_1622(i665, i672, i676, i126, env, static) -{0,0}> iter_Load_1562(i665, i672, i676, i126, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
by chaining
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0

(20) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i641', i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1

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

Moved arithmethic from constraints to rhss.

(24) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i639 + i640, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 0 <= i647
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, 3, i471, i628 + -1, i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

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

Simplified expressions.

(26) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i628 + 1, i632 - 2, i471, i126, env, static) :|: i471 < i632 && i632 - 2 = i656' && i628 + 1 = i652'
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6'
iter_IntArithmetic_1567(i639, x, i471, i628, i632, i126, env, static) -{2,2}> iter_LT_1569(i639 + i640, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641' && 3 * i471 = i640 && x = 3
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i628 - 1 + i632, 3, i471, i628 - 1, i632, i126, env, static) :|: i632 < i628 && i628 - 1 = i648' && i648' + i632 = i653'
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i628 + i632, 3, i471, i628, i632, i126, env, static) :|: i628 + i632 = i639'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1, i126, env, static) :|: i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LT_1569(i646, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1570(i646, i628, i632, i471, i126, env, static) :|: i646 <= -1
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: i628 <= i632
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 <= i647

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

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

(28) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 99 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0
iter_Load_1562(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1563(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1563(i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1564(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) :|: i628 + i632 = i639
iter_ConstantStackPush_1565(i639, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_Load_1566(i639, iconst_3, i628, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) :|: iconst_3 = 3
iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) -{1,1}> iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) :|: iconst_3 * i471 = i640 && iconst_3 = 3
iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) -{1,1}> iter_LT_1569(i641, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1571(i647, i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_LT_1571(i647, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1573(i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_Load_1573(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1575(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1575(i628, i632, i471, i126, env, static) -{1,1}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1578(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1577(i628, i632, i471, i126, env, static) -{0,0}> iter_LE_1579(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_LE_1578(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1580(i628, i632, i471, i126, env, static) :|: i628 <= i632
iter_LE_1579(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1581(i628, i632, i471, i126, env, static) :|: i632 < i628
iter_Load_1580(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1582(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1581(i628, i632, i471, i126, env, static) -{1,1}> iter_JMP_1583(i648, i632, i471, i126, env, static) :|: i628 + -1 = i648
iter_Load_1582(i632, i628, i471, i126, env, static) -{1,1}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_JMP_1583(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1585(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1586(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_LE_1584(i632, i471, i628, i126, env, static) -{0,0}> iter_LE_1587(i632, i471, i628, i126, env, static) :|: i471 < i632
iter_Load_1585(i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1588(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_LE_1586(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1589(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_LE_1587(i632, i471, i628, i126, env, static) -{1,1}> iter_Inc_1590(i628, i632, i471, i126, env, static) :|: i471 < i632
iter_Load_1588(i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1589(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1592(i632, i628, i471, i126, env, static) :|: 0 >= 0
iter_Inc_1590(i628, i632, i471, i126, env, static) -{1,1}> iter_Inc_1593(i652, i632, i471, i126, env, static) :|: i628 + 1 = i652
iter_IntArithmetic_1591(i648, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) :|: i648 + i632 = i653
iter_Load_1592(i632, i628, i471, i126, env, static) -{1,1}> iter_GT_1595(i632, i471, i628, i126, env, static) :|: 0 >= 0
iter_Inc_1593(i652, i632, i471, i126, env, static) -{1,1}> iter_JMP_1596(i652, i656, i471, i126, env, static) :|: i632 + -2 = i656
iter_ConstantStackPush_1594(i653, i648, i632, i471, i126, env, static) -{1,1}> iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) :|: iconst_3 = 3
iter_GT_1595(i632, i471, i628, i126, env, static) -{0,0}> iter_GT_1598(i632, i471, i628, i126, env, static) :|: i632 <= i471
iter_JMP_1596(i652, i656, i471, i126, env, static) -{1,1}> iter_Load_1599(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_Load_1597(i653, iconst_3, i648, i632, i471, i126, env, static) -{1,1}> iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_GT_1598(i632, i471, i628, i126, env, static) -{1,1}> iter_Load_1601(i628, i632, i471, i126, env, static) :|: i632 <= i471
iter_Load_1599(i652, i656, i471, i126, env, static) -{0,0}> iter_Load_1562(i652, i656, i471, i126, env, static) :|: 0 >= 0
iter_IntArithmetic_1600(i653, iconst_3, i471, i648, i632, i126, env, static) -{0,0}> iter_IntArithmetic_1567(i653, iconst_3, i471, i648, i632, i126, env, static) :|: iconst_3 = 3
iter_Load_1601(i628, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1602(i628, i632, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1603(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1604(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1605(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1606(i628, iconst_1, i632, i471, i126, env, static) -{1,1}> add_Return_1607(i665, i632, i471, i126, env, static) :|: i628 + iconst_1 = i665 && iconst_1 = 1
add_Return_1607(i665, i632, i471, i126, env, static) -{1,1}> iter_Store_1608(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Store_1608(i665, i632, i471, i126, env, static) -{1,1}> iter_Load_1609(i665, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1609(i665, i632, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1610(i632, i665, i471, i126, env, static) -{1,1}> iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
iter_InvokeMethod_1611(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1612(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_Load_1613(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) :|: iconst_1 = 1
add_IntArithmetic_1614(i632, iconst_1, i665, i471, i126, env, static) -{1,1}> add_Return_1615(i672, i665, i471, i126, env, static) :|: iconst_1 = 1 && i632 + iconst_1 = i672
add_Return_1615(i672, i665, i471, i126, env, static) -{1,1}> iter_Store_1616(i672, i665, i471, i126, env, static) :|: 0 >= 0
iter_Store_1616(i672, i665, i471, i126, env, static) -{1,1}> iter_Load_1617(i665, i672, i471, i126, env, static) :|: 0 >= 0
iter_Load_1617(i665, i672, i471, i126, env, static) -{1,1}> iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) :|: 0 >= 0
iter_ConstantStackPush_1618(i471, i665, i672, i126, env, static) -{1,1}> iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) :|: iconst_1 = 1
iter_IntArithmetic_1619(i471, iconst_1, i665, i672, i126, env, static) -{1,1}> iter_Store_1620(i676, i665, i672, i126, env, static) :|: i471 - iconst_1 = i676 && iconst_1 = 1
iter_Store_1620(i676, i665, i672, i126, env, static) -{1,1}> iter_JMP_1621(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_JMP_1621(i665, i672, i676, i126, env, static) -{1,1}> iter_Load_1622(i665, i672, i676, i126, env, static) :|: 0 >= 0
iter_Load_1622(i665, i672, i676, i126, env, static) -{0,0}> iter_Load_1562(i665, i672, i676, i126, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
by chaining
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 >= 0
main_Load_44(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{1,1}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_IntArithmetic_54(i2, iconst_5, env, static) :|: iconst_5 = 5
main_IntArithmetic_54(i2, iconst_5, env, static) -{1,1}> main_Load_57(i2, i4, env, static) :|: -4 <= i4 && iconst_5 = 5 && i4 <= 4
main_Load_57(i2, i4, env, static) -{1,1}> main_ConstantStackPush_59(i2, i4, env, static) :|: -4 <= i4 && i4 <= 4
main_ConstantStackPush_59(i2, i4, env, static) -{1,1}> main_IntArithmetic_61(i2, i4, iconst_4, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4
main_IntArithmetic_61(i2, i4, iconst_4, env, static) -{1,1}> main_InvokeMethod_72(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && iconst_4 = 4 && i6 <= 3 && -3 <= i6
main_InvokeMethod_72(i2, i4, i6, env, static) -{1,1}> iter_Load_73(i2, i4, i6, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_73(i2, i4, i6, env, static) -{0,0}> iter_Load_607(i2, i4, i6, i2, env, static) :|: -4 <= i4 && i4 <= 4 && i6 <= 3 && -3 <= i6
iter_Load_607(i264, i265, i6, i126, env, static) -{0,0}> iter_Load_774(i264, i265, i6, i126, env, static) :|: -4 <= i6 && i6 <= 3 && -3 <= i6 && -4 <= i265
iter_Load_774(i327, i329, i330, i126, env, static) -{0,0}> iter_Load_867(i327, i329, i330, i126, env, static) :|: -4 <= i330 && -5 <= i329 && -4 <= i329 && i330 <= 3
iter_Load_867(i360, i361, i330, i126, env, static) -{0,0}> iter_Load_992(i360, i361, i330, i126, env, static) :|: -5 <= i361 && -5 <= i330 && -4 <= i330 && i330 <= 3
iter_Load_992(i411, i412, i413, i126, env, static) -{0,0}> iter_Load_1154(i411, i412, i413, i126, env, static) :|: i413 <= 3 && -5 <= i413
iter_Load_1154(i469, i470, i471, i126, env, static) -{0,0}> iter_Load_1251(i469, i470, i471, i126, env, static) :|: 0 >= 0
iter_Load_1251(i507, i515, i471, i126, env, static) -{0,0}> iter_Load_1404(i507, i515, i471, i126, env, static) :|: 0 >= 0
iter_Load_1404(i560, i564, i471, i126, env, static) -{0,0}> iter_Load_1492(i560, i564, i471, i126, env, static) :|: 0 >= 0
iter_Load_1492(i587, i597, i471, i126, env, static) -{0,0}> iter_Load_1562(i587, i597, i471, i126, env, static) :|: 0 >= 0

obtained
iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{5,5}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
by chaining
iter_IntArithmetic_1567(i639, iconst_3, i471, i628, i632, i126, env, static) -{1,1}> iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) :|: iconst_3 * i471 = i640 && iconst_3 = 3
iter_IntArithmetic_1568(i639, i640, i628, i632, i471, i126, env, static) -{1,1}> iter_LT_1569(i641, i628, i632, i471, i126, env, static) :|: i639 + i640 = i641
iter_LT_1569(i647, i628, i632, i471, i126, env, static) -{0,0}> iter_LT_1571(i647, i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_LT_1571(i647, i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1573(i628, i632, i471, i126, env, static) :|: 0 <= i647
iter_Load_1573(i628, i632, i471, i126, env, static) -{1,1}> iter_Load_1575(i628, i632, i471, i126, env, static) :|: 0 >= 0
iter_Load_1575(i628, i632, i471, i126, env, static) -{1,1}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0

(32) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{23,23}> iter_Load_1562(i2, i4', i6', i2, env, static'1) :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_Load_1562(i628, i632, i471, i126, env, static) -{5,5}> iter_IntArithmetic_1567(i639', 3, i471, i628, i632, i126, env, static) :|: 0 >= 0 && i628 + i632 = i639'
iter_IntArithmetic_1567(i639, 3, i471, i628, i632, i126, env, static) -{5,5}> iter_LE_1577(i628, i632, i471, i126, env, static) :|: 0 >= 0 && 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
iter_LE_1577(i628, i632, i471, i126, env, static) -{8,8}> iter_IntArithmetic_1567(i653', 3, i471, i648', i632, i126, env, static) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LE_1577(i628, i632, i471, i126, env, static) -{3,3}> iter_LE_1584(i632, i471, i628, i126, env, static) :|: 0 >= 0 && i628 <= i632
iter_LE_1584(i632, i471, i628, i126, env, static) -{4,4}> iter_Load_1562(i652', i656', i471, i126, env, static) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_LE_1584(i632, i471, i628, i126, env, static) -{25,25}> iter_Load_1562(i665', i672', i676', i126, env, static) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

(33) 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_2(x1, x2, x3) → main_Load_2(x1, x3)
iter_Load_1562(x1, x2, x3, x4, x5, x6) → iter_Load_1562(x1, x2, x3)
iter_IntArithmetic_1567(x1, x2, x3, x4, x5, x6, x7, x8) → iter_IntArithmetic_1567(x1, x3, x4, x5)
iter_LE_1577(x1, x2, x3, x4, x5, x6) → iter_LE_1577(x1, x2, x3)
iter_LE_1584(x1, x2, x3, x4, x5, x6) → iter_LE_1584(x1, x2, x3)

(34) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, static) -{23,23}> iter_Load_1562(i2, i4', i6') :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i639', i471, i628, i632) :|: 0 >= 0 && i628 + i632 = i639'
iter_IntArithmetic_1567(i639, i471, i628, i632) -{5,5}> iter_LE_1577(i628, i632, i471) :|: 0 >= 0 && 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i653', i471, i648', i632) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
iter_LE_1577(i628, i632, i471) -{3,3}> iter_LE_1584(i632, i471, i628) :|: 0 >= 0 && i628 <= i632
iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i652', i656', i471) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i665', i672', i676') :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

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

Moved arithmethic from constraints to rhss.

iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i639', i471, i628, i632) :|: 0 >= 0 && i628 + i632 = i639'
was transformed to
iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i628 + i632, i471, i628, i632) :|: 0 >= 0 && i628 + i632 = i639'

iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i665', i672', i676') :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
was transformed to
iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i652', i656', i471) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
was transformed to
iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'

iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i653', i471, i648', i632) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
was transformed to
iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, i471, i628 + -1, i632) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'

(36) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i628 + i632, i471, i628, i632) :|: 0 >= 0 && i628 + i632 = i639'
main_Load_2(i2, static) -{23,23}> iter_Load_1562(i2, i4', i6') :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
iter_LE_1577(i628, i632, i471) -{3,3}> iter_LE_1584(i632, i471, i628) :|: 0 >= 0 && i628 <= i632
iter_IntArithmetic_1567(i639, i471, i628, i632) -{5,5}> iter_LE_1577(i628, i632, i471) :|: 0 >= 0 && 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, i471, i628 + -1, i632) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'

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

Simplified expressions.

iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i628 + -1 + i632, i471, i628 + -1, i632) :|: 0 >= 0 && i632 < i628 && i628 + -1 = i648' && i648' + i632 = i653'
was transformed to
iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i628 - 1 + i632, i471, i628 - 1, i632) :|: i632 < i628 && i628 - 1 = i648' && i648' + i632 = i653'

main_Load_2(i2, static) -{23,23}> iter_Load_1562(i2, i4', i6') :|: 0 >= 0 && i6' <= 3 && 0 <= 2 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6' && 0 < 2
was transformed to
main_Load_2(i2, static) -{23,23}> iter_Load_1562(i2, i4', i6') :|: i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6'

iter_LE_1577(i628, i632, i471) -{3,3}> iter_LE_1584(i632, i471, i628) :|: 0 >= 0 && i628 <= i632
was transformed to
iter_LE_1577(i628, i632, i471) -{3,3}> iter_LE_1584(i632, i471, i628) :|: i628 <= i632

iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i628 + 1, i632 + -2, i471) :|: 0 >= 0 && i471 < i632 && i632 + -2 = i656' && i628 + 1 = i652'
was transformed to
iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i628 + 1, i632 - 2, i471) :|: i471 < i632 && i632 - 2 = i656' && i628 + 1 = i652'

iter_IntArithmetic_1567(i639, i471, i628, i632) -{5,5}> iter_LE_1577(i628, i632, i471) :|: 0 >= 0 && 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
was transformed to
iter_IntArithmetic_1567(i639, i471, i628, i632) -{5,5}> iter_LE_1577(i628, i632, i471) :|: 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'

iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i628 + i632, i471, i628, i632) :|: 0 >= 0 && i628 + i632 = i639'
was transformed to
iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i628 + i632, i471, i628, i632) :|: i628 + i632 = i639'

iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1) :|: 0 >= 0 && i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'
was transformed to
iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1) :|: i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

(38) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
iter_LE_1577(i628, i632, i471) -{3,3}> iter_LE_1584(i632, i471, i628) :|: i628 <= i632
main_Load_2(i2, static) -{23,23}> iter_Load_1562(i2, i4', i6') :|: i6' <= 3 && -5 <= i6' && static'1 <= static''' + 1 && -4 <= i4' && 0 <= static''' && i4' <= 4 && static''' <= static + 2 && 0 <= static && 0 <= static'1 && -5 <= i4' && -3 <= i6' && -4 <= i6'
iter_IntArithmetic_1567(i639, i471, i628, i632) -{5,5}> iter_LE_1577(i628, i632, i471) :|: 3 * i471 = i640 && 0 <= i641' && i639 + i640 = i641'
iter_LE_1577(i628, i632, i471) -{8,8}> iter_IntArithmetic_1567(i628 - 1 + i632, i471, i628 - 1, i632) :|: i632 < i628 && i628 - 1 = i648' && i648' + i632 = i653'
iter_LE_1584(i632, i471, i628) -{4,4}> iter_Load_1562(i628 + 1, i632 - 2, i471) :|: i471 < i632 && i632 - 2 = i656' && i628 + 1 = i652'
iter_Load_1562(i628, i632, i471) -{5,5}> iter_IntArithmetic_1567(i628 + i632, i471, i628, i632) :|: i628 + i632 = i639'
iter_LE_1584(i632, i471, i628) -{25,25}> iter_Load_1562(i628 + 1, i632 + 1, i471 - 1) :|: i628 + 1 = i665' && i632 + 1 = i672' && i632 <= i471 && i471 - 1 = i676'

(39) koat Proof (EQUIVALENT transformation)

YES(?, 605*ar_0 + 35503)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 3) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_0, i4', i6', arityPad)) [ i6' <= 3 /\ -5 <= i6' /\ static'1 <= static''' + 1 /\ -4 <= i4' /\ 0 <= static''' /\ i4' <= 4 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ -5 <= i4' /\ -3 <= i6' /\ -4 <= i6' ]
(Comp: ?, Cost: 5) iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
(Comp: ?, Cost: 8) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1 - 1, ar_2, ar_0 - 1, ar_1)) [ ar_1 < ar_0 /\ ar_0 - 1 = i648' /\ i648' + ar_1 = i653' ]
(Comp: ?, Cost: 4) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
(Comp: ?, Cost: 5) iter_Load_1562(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1, ar_2, ar_0, ar_1)) [ ar_0 + ar_1 = i639' ]
(Comp: ?, Cost: 25) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(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: ?, Cost: 3) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ ar_0 <= ar_1 ]
(Comp: 1, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_0, i4', i6', arityPad)) [ i6' <= 3 /\ -5 <= i6' /\ static'1 <= static''' + 1 /\ -4 <= i4' /\ 0 <= static''' /\ i4' <= 4 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ -5 <= i4' /\ -3 <= i6' /\ -4 <= i6' ]
(Comp: ?, Cost: 5) iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
(Comp: ?, Cost: 8) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1 - 1, ar_2, ar_0 - 1, ar_1)) [ ar_1 < ar_0 /\ ar_0 - 1 = i648' /\ i648' + ar_1 = i653' ]
(Comp: ?, Cost: 4) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
(Comp: ?, Cost: 5) iter_Load_1562(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1, ar_2, ar_0, ar_1)) [ ar_0 + ar_1 = i639' ]
(Comp: ?, Cost: 25) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
For symbol iter_IntArithmetic_1567: -X_4 + 4 >= 0 /\ X_2 - X_4 + 7 >= 0 /\ -X_2 - X_4 + 7 >= 0 /\ -X_2 + X_4 + 7 >= 0 /\ -X_1 + X_3 + 4 >= 0 /\ -X_2 + 3 >= 0
For symbol iter_LE_1577: -X_3 + 3 >= 0 /\ X_2 - X_3 + 7 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 + 16 >= 0 /\ -X_2 + X_3 + 7 >= 0 /\ X_1 + X_3 + 10 >= 0 /\ -X_2 + 4 >= 0 /\ X_1 - X_2 + 17 >= 0 /\ X_1 + X_2 + 17 >= 0 /\ X_1 + 13 >= 0
For symbol iter_LE_1584: -X_3 + 4 >= 0 /\ X_2 - X_3 + 7 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ X_1 - X_3 >= 0 /\ -X_1 - X_3 + 8 >= 0 /\ X_3 + 13 >= 0 /\ X_2 + X_3 + 10 >= 0 /\ -X_2 + X_3 + 16 >= 0 /\ X_1 + X_3 + 17 >= 0 /\ -X_1 + X_3 + 17 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 + 7 >= 0 /\ -X_1 - X_2 + 7 >= 0 /\ X_2 + 8 >= 0 /\ X_1 + X_2 + 10 >= 0 /\ -X_1 + X_2 + 7 >= 0 /\ -X_1 + 4 >= 0 /\ X_1 + 8 >= 0
For symbol iter_Load_1562: -X_3 + 3 >= 0 /\ X_2 - X_3 + 7 >= 0 /\ -X_2 - X_3 + 7 >= 0 /\ -X_2 + X_3 + 7 >= 0 /\ -X_2 + 4 >= 0

This yielded the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 25) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
(Comp: ?, Cost: 5) iter_Load_1562(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1, ar_2, ar_0, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 + ar_1 = i639' ]
(Comp: ?, Cost: 4) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
(Comp: ?, Cost: 8) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1 - 1, ar_2, ar_0 - 1, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 1 = i648' /\ i648' + ar_1 = i653' ]
(Comp: ?, Cost: 5) iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ -ar_3 + 4 >= 0 /\ ar_1 - ar_3 + 7 >= 0 /\ -ar_1 - ar_3 + 7 >= 0 /\ -ar_1 + ar_3 + 7 >= 0 /\ -ar_0 + ar_2 + 4 >= 0 /\ -ar_1 + 3 >= 0 /\ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
(Comp: 1, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_0, i4', i6', arityPad)) [ i6' <= 3 /\ -5 <= i6' /\ static'1 <= static''' + 1 /\ -4 <= i4' /\ 0 <= static''' /\ i4' <= 4 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ -5 <= i4' /\ -3 <= i6' /\ -4 <= i6' ]
(Comp: ?, Cost: 3) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 11*V_1 + 645
Pol(main_Load_2) = 11*V_1 + 645
Pol(iter_LE_1584) = 8*V_1 + 25*V_2 + 11*V_3 + 534
Pol(iter_Load_1562) = 11*V_1 + 8*V_2 + 25*V_3 + 538
Pol(iter_IntArithmetic_1567) = 25*V_2 + 11*V_3 + 8*V_4 + 538
Pol(iter_LE_1577) = 11*V_1 + 8*V_2 + 25*V_3 + 536
orients all transitions weakly and the transitions
iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 ]
iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ -ar_3 + 4 >= 0 /\ ar_1 - ar_3 + 7 >= 0 /\ -ar_1 - ar_3 + 7 >= 0 /\ -ar_1 + ar_3 + 7 >= 0 /\ -ar_0 + ar_2 + 4 >= 0 /\ -ar_1 + 3 >= 0 /\ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 645, Cost: 25) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
(Comp: ?, Cost: 5) iter_Load_1562(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1, ar_2, ar_0, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 + ar_1 = i639' ]
(Comp: 11*ar_0 + 645, Cost: 4) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
(Comp: ?, Cost: 8) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1 - 1, ar_2, ar_0 - 1, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 1 = i648' /\ i648' + ar_1 = i653' ]
(Comp: 11*ar_0 + 645, Cost: 5) iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ -ar_3 + 4 >= 0 /\ ar_1 - ar_3 + 7 >= 0 /\ -ar_1 - ar_3 + 7 >= 0 /\ -ar_1 + ar_3 + 7 >= 0 /\ -ar_0 + ar_2 + 4 >= 0 /\ -ar_1 + 3 >= 0 /\ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
(Comp: 1, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_0, i4', i6', arityPad)) [ i6' <= 3 /\ -5 <= i6' /\ static'1 <= static''' + 1 /\ -4 <= i4' /\ 0 <= static''' /\ i4' <= 4 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ -5 <= i4' /\ -3 <= i6' /\ -4 <= i6' ]
(Comp: 11*ar_0 + 645, Cost: 3) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 11*ar_0 + 645, Cost: 25) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 + 1, ar_1 - 1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_2 + 1 = i665' /\ ar_0 + 1 = i672' /\ ar_0 <= ar_1 /\ ar_1 - 1 = i676' ]
(Comp: 22*ar_0 + 1291, Cost: 5) iter_Load_1562(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1, ar_2, ar_0, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 + ar_1 = i639' ]
(Comp: 11*ar_0 + 645, Cost: 4) iter_LE_1584(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_2 + 1, ar_0 - 2, ar_1, arityPad)) [ -ar_2 + 4 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 >= 0 /\ -ar_0 - ar_2 + 8 >= 0 /\ ar_2 + 13 >= 0 /\ ar_1 + ar_2 + 10 >= 0 /\ -ar_1 + ar_2 + 16 >= 0 /\ ar_0 + ar_2 + 17 >= 0 /\ -ar_0 + ar_2 + 17 >= 0 /\ -ar_1 + 3 >= 0 /\ ar_0 - ar_1 + 7 >= 0 /\ -ar_0 - ar_1 + 7 >= 0 /\ ar_1 + 8 >= 0 /\ ar_0 + ar_1 + 10 >= 0 /\ -ar_0 + ar_1 + 7 >= 0 /\ -ar_0 + 4 >= 0 /\ ar_0 + 8 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 2 = i656' /\ ar_2 + 1 = i652' ]
(Comp: 11*ar_0 + 645, Cost: 8) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_IntArithmetic_1567(ar_0 + ar_1 - 1, ar_2, ar_0 - 1, ar_1)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_1 < ar_0 /\ ar_0 - 1 = i648' /\ i648' + ar_1 = i653' ]
(Comp: 11*ar_0 + 645, Cost: 5) iter_IntArithmetic_1567(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1577(ar_2, ar_3, ar_1, arityPad)) [ -ar_3 + 4 >= 0 /\ ar_1 - ar_3 + 7 >= 0 /\ -ar_1 - ar_3 + 7 >= 0 /\ -ar_1 + ar_3 + 7 >= 0 /\ -ar_0 + ar_2 + 4 >= 0 /\ -ar_1 + 3 >= 0 /\ 3*ar_1 = i640 /\ 0 <= i641' /\ ar_0 + i640 = i641' ]
(Comp: 1, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_Load_1562(ar_0, i4', i6', arityPad)) [ i6' <= 3 /\ -5 <= i6' /\ static'1 <= static''' + 1 /\ -4 <= i4' /\ 0 <= static''' /\ i4' <= 4 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ -5 <= i4' /\ -3 <= i6' /\ -4 <= i6' ]
(Comp: 11*ar_0 + 645, Cost: 3) iter_LE_1577(ar_0, ar_1, ar_2, ar_3) -> Com_1(iter_LE_1584(ar_1, ar_2, ar_0, arityPad)) [ -ar_2 + 3 >= 0 /\ ar_1 - ar_2 + 7 >= 0 /\ -ar_1 - ar_2 + 7 >= 0 /\ ar_0 - ar_2 + 16 >= 0 /\ -ar_1 + ar_2 + 7 >= 0 /\ ar_0 + ar_2 + 10 >= 0 /\ -ar_1 + 4 >= 0 /\ ar_0 - ar_1 + 17 >= 0 /\ ar_0 + ar_1 + 17 >= 0 /\ ar_0 + 13 >= 0 /\ ar_0 <= ar_1 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 605*ar_0 + 35503

Time: 0.847 sec (SMT: 0.730 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 35503 + 605 * |#0|)