time complexity proof of /tmp/tmp_yhVg

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 159 + 23 * |args|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 16 ms)

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(115)), 8 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 219 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 75 ms)

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 5 ms)

    ↳40 WeightedIntTrs

    ↳41 koat Proof (⇔, 333 ms)

    ↳42 BOUNDS(CONSTANT, 44 + 23 * |args|)

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Java can do infinite data objects, too.
 * Here we take the first n elements from an
 * ascending infinite list of integer numbers.
 *
 * @author Carsten Fuhs
 */
public class Take {

    public static int[] take(int n, MyIterator f) {
        int[] result = new int[n];
        for (int i = 0; i < n; ++i) {
            if (f.hasNext()) {
                result[i] = f.next();
            }
            else {
                break;
            }
        }
        return result;
    }

    public static void main(String args[]) {
        int start = args[0].length();
        int howMany = args[1].length();
        From f = new From(start);
        int[] firstHowMany = take(howMany, f);
    }
}

interface MyIterator {
    boolean hasNext();
    int next();
}

class From implements MyIterator {

    private int current;

    public From(int start) {
        this.current = start;
    }

    public boolean hasNext() {
        return true;
    }

    public int next() {
        return current++;
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- From: [current]

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 93 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_20(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_24(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_28(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_36(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_36(o2, env, static) -{1,1}> main_Load_38(o2, env, static) :|: 0 < o2
main_Load_38(o2, env, static) -{0,0}> main_Load_39(o2, env, static) :|: 0 < o2
main_Load_39(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_47(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{1,1}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_54(a6, iconst_0, i4, env, static) :|: 0 <= i4 && iconst_0 = 0 && 0 < a6 && i4 < a6
main_ArrayAccess_54(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_55(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_54(a6, iconst_0, i5, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: iconst_0 = 0 && 0 < a6 && 0 <= i5 && 1 <= i5
main_ArrayAccess_57(a6, iconst_0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i5, env, static) :|: 0 <= o8 && o8 < a6 && iconst_0 = 0 && iconst_0 < i5 && 0 < a6 && 1 <= i5
main_InvokeMethod_64(a6, o12, i5, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i5, env, static) :|: 0 <= o12 && 0 < o12 && 0 < a6 && 1 <= i5
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
main_InvokeMethod_66(a6, o12, i5, env, static) -{1,1}> main_Store_70(a6, i8, i5, env, static) :|: i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8 && 1 <= i5
main_Store_70(a6, i8, i5, env, static) -{1,1}> main_Load_76(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_Load_76(a6, i8, i5, env, static) -{1,1}> main_ConstantStackPush_80(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_ConstantStackPush_80(a6, i8, i5, env, static) -{1,1}> main_ArrayAccess_86(a6, iconst_1, i8, i5, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i5
main_ArrayAccess_86(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_86(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18, i8, i12, env, static) :|: 2 <= i12 && 0 <= o18 && iconst_1 = 1 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o18 < a6
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{0,0}> main_InvokeMethod_100(a6, o21, i8, i12, env, static) :|: 2 <= i12 && 0 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_100(a6, o21, i8, i12, env, static) -{1,1}> main_Store_106(a6, i13, i8, i12, env, static) :|: 2 <= i12 && i13 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_106(a6, i13, i8, i12, env, static) -{1,1}> main_New_113(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_113(a6, i8, i13, i12, env, static) -{0,0}> main_New_118(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_118(a6, i8, i13, i12, env, static) -{1,1}> main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && o30 = 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Return_256(a6, o30', i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && o30' <= o30 + i8 && 0 < a6 && o30 <= o30' && 0 <= i8 && 0 < o30' && 0 <= i13
langle_init_rangle_Return_256(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Store_261(a6, o30, i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_261(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Load_266(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_266(a6, i13, o30, i12, i8, env, static) -{1,1}> main_Load_271(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_271(a6, i13, o30, i12, i8, env, static) -{1,1}> main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) -{1,1}> take_Load_281(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_281(i13, o30, a6, i8, i12, env, static) -{1,1}> take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) -{1,1}> take_Store_291(a75, i13, o30, a6, i8, i12, env, static) :|: 0 < a75 && a75 = i13 + 2 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_291(a75, i13, o30, a6, i8, i12, env, static) -{1,1}> take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) -{0,0}> take_Load_394(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 0 <= iconst_0 && 2 <= i12 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_394(i22, o129, a90, i24, a91, i23, i12, env, static) -{0,0}> take_Load_500(i22, o129, a90, i24, a91, i23, i12, env, static) :|: 0 <= i24 && i24 <= 1 && 0 < a91 && 2 <= i12 && i24 <= 2 && 0 < a90 && 0 <= i22 && 0 < o129 && 0 <= i23
take_Load_500(i40, o138, a100, i42, a101, i41, i12, env, static) -{0,0}> take_Load_645(i40, o138, a100, i42, a101, i41, i12, env, static) :|: 0 < o138 && i42 <= 2 && 0 <= i41 && 2 <= i12 && 0 <= i40 && 0 < a100 && 0 <= i42 && 0 < a101
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i60 < i58 && 0 < a111
take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 1 <= i58 && i60 < i58 && 0 < a111
take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < iconst_1 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) -{1,1}> take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) -{1,1}> next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) -{1,1}> next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) -{1,1}> next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) -{1,1}> next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) :|: i59 + iconst_1 = i68 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) -{1,1}> next_Return_690(i59, a110, i60, i58, o147', a111, i68, i12, env, static) :|: 0 < a110 && o147 < o147' && 0 <= i59 && 2 <= i12 && 0 < o147' && o147' <= o147 + i68 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_Return_690(i59, a110, i60, i58, o147, a111, i68, i12, env, static) -{1,1}> take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{1,1}> take_Inc_696(i58, o147, a110', i60, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && a110' <= a110 + i59 && 0 < o147 && 0 <= i60 && 1 <= i58 && i60 < i58 && 1 <= i68 && 0 < a110' && 0 < a111
take_Inc_696(i58, o147, a110, i60, a111, i68, i12, env, static) -{1,1}> take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 1 <= i70 && i60 + 1 = i70 && 0 < a111
take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) -{1,1}> take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111
take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) -{0,0}> take_Load_645(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 <= i70 && 0 < o147 && 0 <= i58 && 0 <= i68 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111

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

obtained
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_20(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_24(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_28(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_36(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_36(o2, env, static) -{1,1}> main_Load_38(o2, env, static) :|: 0 < o2
main_Load_38(o2, env, static) -{0,0}> main_Load_39(o2, env, static) :|: 0 < o2
main_Load_39(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_47(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{1,1}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_54(a6, iconst_0, i4, env, static) :|: 0 <= i4 && iconst_0 = 0 && 0 < a6 && i4 < a6

obtained
main_ArrayAccess_54(a6, 0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6
by chaining
main_ArrayAccess_54(a6, iconst_0, i5, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: iconst_0 = 0 && 0 < a6 && 0 <= i5 && 1 <= i5
main_ArrayAccess_57(a6, iconst_0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i5, env, static) :|: 0 <= o8 && o8 < a6 && iconst_0 = 0 && iconst_0 < i5 && 0 < a6 && 1 <= i5

obtained
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
by chaining
main_InvokeMethod_64(a6, o12, i5, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i5, env, static) :|: 0 <= o12 && 0 < o12 && 0 < a6 && 1 <= i5
main_InvokeMethod_66(a6, o12, i5, env, static) -{1,1}> main_Store_70(a6, i8, i5, env, static) :|: i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8 && 1 <= i5
main_Store_70(a6, i8, i5, env, static) -{1,1}> main_Load_76(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_Load_76(a6, i8, i5, env, static) -{1,1}> main_ConstantStackPush_80(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_ConstantStackPush_80(a6, i8, i5, env, static) -{1,1}> main_ArrayAccess_86(a6, iconst_1, i8, i5, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i5

obtained
main_ArrayAccess_86(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18'
by chaining
main_ArrayAccess_86(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18, i8, i12, env, static) :|: 2 <= i12 && 0 <= o18 && iconst_1 = 1 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o18 < a6

obtained
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', a75', 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
by chaining
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{0,0}> main_InvokeMethod_100(a6, o21, i8, i12, env, static) :|: 2 <= i12 && 0 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8
main_InvokeMethod_100(a6, o21, i8, i12, env, static) -{1,1}> main_Store_106(a6, i13, i8, i12, env, static) :|: 2 <= i12 && i13 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_106(a6, i13, i8, i12, env, static) -{1,1}> main_New_113(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_113(a6, i8, i13, i12, env, static) -{0,0}> main_New_118(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_118(a6, i8, i13, i12, env, static) -{1,1}> main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && o30 = 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Return_256(a6, o30', i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && o30' <= o30 + i8 && 0 < a6 && o30 <= o30' && 0 <= i8 && 0 < o30' && 0 <= i13
langle_init_rangle_Return_256(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Store_261(a6, o30, i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_261(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Load_266(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_266(a6, i13, o30, i12, i8, env, static) -{1,1}> main_Load_271(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_271(a6, i13, o30, i12, i8, env, static) -{1,1}> main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) -{1,1}> take_Load_281(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_281(i13, o30, a6, i8, i12, env, static) -{1,1}> take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) -{1,1}> take_Store_291(a75, i13, o30, a6, i8, i12, env, static) :|: 0 < a75 && a75 = i13 + 2 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_291(a75, i13, o30, a6, i8, i12, env, static) -{1,1}> take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) -{0,0}> take_Load_394(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 0 <= iconst_0 && 2 <= i12 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_394(i22, o129, a90, i24, a91, i23, i12, env, static) -{0,0}> take_Load_500(i22, o129, a90, i24, a91, i23, i12, env, static) :|: 0 <= i24 && i24 <= 1 && 0 < a91 && 2 <= i12 && i24 <= 2 && 0 < a90 && 0 <= i22 && 0 < o129 && 0 <= i23
take_Load_500(i40, o138, a100, i42, a101, i41, i12, env, static) -{0,0}> take_Load_645(i40, o138, a100, i42, a101, i41, i12, env, static) :|: 0 < o138 && i42 <= 2 && 0 <= i41 && 2 <= i12 && 0 <= i40 && 0 < a100 && 0 <= i42 && 0 < a101

obtained
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
by chaining
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111

obtained
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i68', i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
by chaining
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i60 < i58 && 0 < a111
take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 1 <= i58 && i60 < i58 && 0 < a111
take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < iconst_1 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) -{1,1}> take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) -{1,1}> next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) -{1,1}> next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) -{1,1}> next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) -{1,1}> next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) :|: i59 + iconst_1 = i68 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) -{1,1}> next_Return_690(i59, a110, i60, i58, o147', a111, i68, i12, env, static) :|: 0 < a110 && o147 < o147' && 0 <= i59 && 2 <= i12 && 0 < o147' && o147' <= o147 + i68 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_Return_690(i59, a110, i60, i58, o147, a111, i68, i12, env, static) -{1,1}> take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111

obtained
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i70', a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
by chaining
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{1,1}> take_Inc_696(i58, o147, a110', i60, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && a110' <= a110 + i59 && 0 < o147 && 0 <= i60 && 1 <= i58 && i60 < i58 && 1 <= i68 && 0 < a110' && 0 < a111
take_Inc_696(i58, o147, a110, i60, a111, i68, i12, env, static) -{1,1}> take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 1 <= i70 && i60 + 1 = i70 && 0 < a111
take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) -{1,1}> take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111
take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) -{0,0}> take_Load_645(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 <= i70 && 0 < o147 && 0 <= i58 && 0 <= i68 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111

(8) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_54(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_55(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_54(a6, 0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
main_ArrayAccess_86(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_86(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18'
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', a75', 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i68', i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i70', a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60

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

Moved arithmethic from lhss to constraints.

main_ArrayAccess_86(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18'
was transformed to
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1

main_ArrayAccess_54(a6, 0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6
was transformed to
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0

(10) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_86(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i68', i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i70', a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', a75', 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
main_ArrayAccess_54(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_55(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0

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

Linearized lhss.

main_ArrayAccess_86(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
was transformed to
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

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

(12) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i68', i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i70', a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', a75', 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
main_ArrayAccess_54(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_55(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

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

Moved arithmethic from constraints to rhss.

main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
was transformed to
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5

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

take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i68', i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
was transformed to
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'

take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i70', a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
was transformed to
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i60 + 1, a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60

main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
was transformed to
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8

main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', a75', 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
was transformed to
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21

main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
was transformed to
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

(14) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
main_ArrayAccess_54(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_55(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i60 + 1, a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

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

Simplified expressions.

main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
was transformed to
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1

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

main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0
was transformed to
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0

take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
was transformed to
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && i59 + 1 = i68'

main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
was transformed to
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6

main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
was transformed to
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= i8 && 0 < o30''' && a75' = i13' + 2 && i13' <= o21

(16) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i60 + 1, a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && i59 + 1 = i68'
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= i8 && 0 < o30''' && a75' = i13' + 2 && i13' <= o21
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
main_ArrayAccess_54(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_55(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

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

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

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Linearized lhss.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_86(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18', i8, i12, env, static) :|: 1 <= i12 && o18' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o18' && x = 1
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_54(o2, 0, i4', env, static'1) :|: static'1 <= static''' + 1 && i4' < o2 && 0 <= 2 && 0 < o2 && static''' <= static + 2 && 0 <= i4' && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_648(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i58 <= i60 && 0 < a111
main_ArrayAccess_54(a6, x, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i5, env, static) :|: 1 <= i5 && 0 <= i5 && 0 < a6 && 0 < i5 && 0 <= o8' && o8' < a6 && x = 0
main_InvokeMethod_64(a6, NULL, i5, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i5, env, static) :|: NULL = 0 && 0 <= NULL && 0 < a6 && 1 <= i5
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{2,2}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a111 && 0 <= i60 && 0 <= i58 && 0 < o147 && 2 <= i12 && 0 < a110 && 0 <= i59
main_ArrayAccess_54(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_55(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{18,18}> take_ArrayAccess_692(a110, i60, i59, i58, o147''', a111, i59 + 1, i12, env, static) :|: o147 < o147''' && 0 < a111 && 0 < a110 && 1 <= i68' && 0 <= i59 && 1 <= i58 && 2 <= i12 && 0 <= i60 && 0 < o147''' && o147''' <= o147 + i68' && 0 < o147 && 0 <= i58 && i60 < i58 && 0 < 1 && i59 + 1 = i68'
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{3,3}> take_Load_645(i58, o147, a110''', i60 + 1, a111, i68, i12, env, static) :|: a110''' <= a110 + i59 && 0 < a111 && 0 <= i59 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68 && 0 < a110 && 1 <= i58 && 2 <= i12 && 0 <= i68 && 0 < o147 && 0 <= i58 && 0 <= i70' && i60 < i58 && 0 < a110''' && 0 <= i60
main_InvokeMethod_98(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_101(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{21,21}> take_Load_645(i13', o30''', i13' + 2, 0, a6, i8, i12, env, static) :|: 0 < o21 && 0 < a6 && o30''' <= 1 + i8 && 0 <= 0 && 0 < 1 && 0 < a75' && 1 <= o30''' && 0 <= i13' && 2 <= i12 && 0 <= 1 && 0 <= i8 && 0 < o30''' && 0 <= 2 && a75' = i13' + 2 && 0 <= o21 && i13' <= o21
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_695(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
main_InvokeMethod_64(a6, o12, i5, env, static) -{4,4}> main_ArrayAccess_86(a6, 1, i8', i5, env, static) :|: i8' <= o12 && 1 <= i5 && 0 < o12 && 0 <= i8' && 0 < a6 && 0 <= o12
main_ArrayAccess_86(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_93(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

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

Simplified expressions.

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(115)) transformation)

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

(30) Obligation:

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

Used field analysis yielded the following read fields:
- From: [current]

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 87 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_20(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_24(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_28(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_36(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_36(o2, env, static) -{1,1}> main_Load_38(o2, env, static) :|: 0 < o2
main_Load_38(o2, env, static) -{0,0}> main_Load_39(o2, env, static) :|: 0 < o2
main_Load_39(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_47(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{1,1}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_54(a6, iconst_0, i4, env, static) :|: 0 <= i4 && iconst_0 = 0 && 0 < a6 && i4 < a6
main_ArrayAccess_54(a6, iconst_0, i5, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: iconst_0 = 0 && 0 < a6 && 0 <= i5 && 1 <= i5
main_ArrayAccess_57(a6, iconst_0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i5, env, static) :|: 0 <= o8 && o8 < a6 && iconst_0 = 0 && iconst_0 < i5 && 0 < a6 && 1 <= i5
main_InvokeMethod_64(a6, o12, i5, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i5, env, static) :|: 0 <= o12 && 0 < o12 && 0 < a6 && 1 <= i5
main_InvokeMethod_66(a6, o12, i5, env, static) -{1,1}> main_Store_70(a6, i8, i5, env, static) :|: i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8 && 1 <= i5
main_Store_70(a6, i8, i5, env, static) -{1,1}> main_Load_76(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_Load_76(a6, i8, i5, env, static) -{1,1}> main_ConstantStackPush_80(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_ConstantStackPush_80(a6, i8, i5, env, static) -{1,1}> main_ArrayAccess_86(a6, iconst_1, i8, i5, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i5
main_ArrayAccess_86(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18, i8, i12, env, static) :|: 2 <= i12 && 0 <= o18 && iconst_1 = 1 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o18 < a6
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{0,0}> main_InvokeMethod_100(a6, o21, i8, i12, env, static) :|: 2 <= i12 && 0 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8
main_InvokeMethod_100(a6, o21, i8, i12, env, static) -{1,1}> main_Store_106(a6, i13, i8, i12, env, static) :|: 2 <= i12 && i13 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_106(a6, i13, i8, i12, env, static) -{1,1}> main_New_113(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_113(a6, i8, i13, i12, env, static) -{0,0}> main_New_118(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_118(a6, i8, i13, i12, env, static) -{1,1}> main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && o30 = 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Return_256(a6, o30', i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && o30' <= o30 + i8 && 0 < a6 && o30 <= o30' && 0 <= i8 && 0 < o30' && 0 <= i13
langle_init_rangle_Return_256(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Store_261(a6, o30, i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_261(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Load_266(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_266(a6, i13, o30, i12, i8, env, static) -{1,1}> main_Load_271(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_271(a6, i13, o30, i12, i8, env, static) -{1,1}> main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) -{1,1}> take_Load_281(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_281(i13, o30, a6, i8, i12, env, static) -{1,1}> take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) -{1,1}> take_Store_291(a75, i13, o30, a6, i8, i12, env, static) :|: 0 < a75 && a75 = i13 + 2 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_291(a75, i13, o30, a6, i8, i12, env, static) -{1,1}> take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) -{0,0}> take_Load_394(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 0 <= iconst_0 && 2 <= i12 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_394(i22, o129, a90, i24, a91, i23, i12, env, static) -{0,0}> take_Load_500(i22, o129, a90, i24, a91, i23, i12, env, static) :|: 0 <= i24 && i24 <= 1 && 0 < a91 && 2 <= i12 && i24 <= 2 && 0 < a90 && 0 <= i22 && 0 < o129 && 0 <= i23
take_Load_500(i40, o138, a100, i42, a101, i41, i12, env, static) -{0,0}> take_Load_645(i40, o138, a100, i42, a101, i41, i12, env, static) :|: 0 < o138 && i42 <= 2 && 0 <= i41 && 2 <= i12 && 0 <= i40 && 0 < a100 && 0 <= i42 && 0 < a101
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i60 < i58 && 0 < a111
take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 1 <= i58 && i60 < i58 && 0 < a111
take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < iconst_1 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) -{1,1}> take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) -{1,1}> next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) -{1,1}> next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) -{1,1}> next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) -{1,1}> next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) :|: i59 + iconst_1 = i68 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) -{1,1}> next_Return_690(i59, a110, i60, i58, o147', a111, i68, i12, env, static) :|: 0 < a110 && o147 < o147' && 0 <= i59 && 2 <= i12 && 0 < o147' && o147' <= o147 + i68 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_Return_690(i59, a110, i60, i58, o147, a111, i68, i12, env, static) -{1,1}> take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{1,1}> take_Inc_696(i58, o147, a110', i60, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && a110' <= a110 + i59 && 0 < o147 && 0 <= i60 && 1 <= i58 && i60 < i58 && 1 <= i68 && 0 < a110' && 0 < a111
take_Inc_696(i58, o147, a110, i60, a111, i68, i12, env, static) -{1,1}> take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 1 <= i70 && i60 + 1 = i70 && 0 < a111
take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) -{1,1}> take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111
take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) -{0,0}> take_Load_645(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 <= i70 && 0 < o147 && 0 <= i58 && 0 <= i68 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111

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

obtained
main_Load_2(o2, env, static) -{44,44}> take_Load_645(i13', o30''', a75', 0, o2, i8', i4', env, static'1) :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
by chaining
main_Load_2(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_20(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_23(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_24(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_24(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_28(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_33(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_36(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_36(o2, env, static) -{1,1}> main_Load_38(o2, env, static) :|: 0 < o2
main_Load_38(o2, env, static) -{0,0}> main_Load_39(o2, env, static) :|: 0 < o2
main_Load_39(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_47(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{1,1}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_54(a6, iconst_0, i4, env, static) :|: 0 <= i4 && iconst_0 = 0 && 0 < a6 && i4 < a6
main_ArrayAccess_54(a6, iconst_0, i5, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: iconst_0 = 0 && 0 < a6 && 0 <= i5 && 1 <= i5
main_ArrayAccess_57(a6, iconst_0, i5, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i5, env, static) :|: 0 <= o8 && o8 < a6 && iconst_0 = 0 && iconst_0 < i5 && 0 < a6 && 1 <= i5
main_InvokeMethod_64(a6, o12, i5, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i5, env, static) :|: 0 <= o12 && 0 < o12 && 0 < a6 && 1 <= i5
main_InvokeMethod_66(a6, o12, i5, env, static) -{1,1}> main_Store_70(a6, i8, i5, env, static) :|: i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8 && 1 <= i5
main_Store_70(a6, i8, i5, env, static) -{1,1}> main_Load_76(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_Load_76(a6, i8, i5, env, static) -{1,1}> main_ConstantStackPush_80(a6, i8, i5, env, static) :|: 0 < a6 && 0 <= i8 && 1 <= i5
main_ConstantStackPush_80(a6, i8, i5, env, static) -{1,1}> main_ArrayAccess_86(a6, iconst_1, i8, i5, env, static) :|: iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i5
main_ArrayAccess_86(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_94(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_98(a6, o18, i8, i12, env, static) :|: 2 <= i12 && 0 <= o18 && iconst_1 = 1 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o18 < a6
main_InvokeMethod_98(a6, o21, i8, i12, env, static) -{0,0}> main_InvokeMethod_100(a6, o21, i8, i12, env, static) :|: 2 <= i12 && 0 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8
main_InvokeMethod_100(a6, o21, i8, i12, env, static) -{1,1}> main_Store_106(a6, i13, i8, i12, env, static) :|: 2 <= i12 && i13 <= o21 && 0 < o21 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_106(a6, i13, i8, i12, env, static) -{1,1}> main_New_113(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_113(a6, i8, i13, i12, env, static) -{0,0}> main_New_118(a6, i8, i13, i12, env, static) :|: 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_New_118(a6, i8, i13, i12, env, static) -{1,1}> main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && o30 = 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Duplicate_127(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_137(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_144(a6, o30, i8, i13, i12, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_150(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_InvokeMethod_164(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_192(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_Load_248(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
langle_init_rangle_FieldAccess_252(o30, i8, a6, i13, iconst_0, i12, env, static) -{1,1}> langle_init_rangle_Return_256(a6, o30', i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && iconst_0 = 0 && o30' <= o30 + i8 && 0 < a6 && o30 <= o30' && 0 <= i8 && 0 < o30' && 0 <= i13
langle_init_rangle_Return_256(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Store_261(a6, o30, i13, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Store_261(a6, o30, i13, i12, i8, env, static) -{1,1}> main_Load_266(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_266(a6, i13, o30, i12, i8, env, static) -{1,1}> main_Load_271(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_Load_271(a6, i13, o30, i12, i8, env, static) -{1,1}> main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
main_InvokeMethod_276(a6, i13, o30, i12, i8, env, static) -{1,1}> take_Load_281(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_281(i13, o30, a6, i8, i12, env, static) -{1,1}> take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) :|: 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ArrayCreate_288(i13, o30, a6, i8, i12, env, static) -{1,1}> take_Store_291(a75, i13, o30, a6, i8, i12, env, static) :|: 0 < a75 && a75 = i13 + 2 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_291(a75, i13, o30, a6, i8, i12, env, static) -{1,1}> take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= i13
take_ConstantStackPush_294(i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Store_297(iconst_0, i13, o30, a75, a6, i8, i12, env, static) -{1,1}> take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 2 <= i12 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_300(i13, o30, a75, iconst_0, a6, i8, i12, env, static) -{0,0}> take_Load_394(i13, o30, a75, iconst_0, a6, i8, i12, env, static) :|: 0 < a75 && 0 < o30 && 0 <= iconst_0 && 2 <= i12 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 0 <= i8 && 0 <= i13
take_Load_394(i22, o129, a90, i24, a91, i23, i12, env, static) -{0,0}> take_Load_500(i22, o129, a90, i24, a91, i23, i12, env, static) :|: 0 <= i24 && i24 <= 1 && 0 < a91 && 2 <= i12 && i24 <= 2 && 0 < a90 && 0 <= i22 && 0 < o129 && 0 <= i23
take_Load_500(i40, o138, a100, i42, a101, i41, i12, env, static) -{0,0}> take_Load_645(i40, o138, a100, i42, a101, i41, i12, env, static) :|: 0 < o138 && i42 <= 2 && 0 <= i41 && 2 <= i12 && 0 <= i40 && 0 < a100 && 0 <= i42 && 0 < a101

obtained
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{23,23}> take_Load_645(i58, o147''', a110''', i70', a111, i68', i12, env, static) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''
by chaining
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_Load_646(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 0 < a111
take_GE_647(i60, i58, o147, a110, a111, i59, i12, env, static) -{0,0}> take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && i60 < i58 && 0 < a111
take_GE_649(i60, i58, o147, a110, a111, i59, i12, env, static) -{1,1}> take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i58 && 0 <= i60 && 1 <= i58 && i60 < i58 && 0 < a111
take_Load_652(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_654(o147, i58, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_ConstantStackPush_656(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
hasNext_Return_661(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_EQ_663(iconst_1, i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) :|: 0 < iconst_1 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_665(i58, o147, a110, i60, a111, i59, i12, env, static) -{1,1}> take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_667(a110, i58, o147, i60, a111, i59, i12, env, static) -{1,1}> take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_Load_670(a110, i60, i58, o147, a111, i59, i12, env, static) -{1,1}> take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
take_InvokeMethod_672(a110, i60, o147, i58, a111, i59, i12, env, static) -{1,1}> next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Load_674(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_676(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_FieldAccess_678(o147, a110, i60, i58, a111, i59, i12, env, static) -{1,1}> next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_Duplicate_680(o147, i59, a110, i60, i58, a111, i12, env, static) -{1,1}> next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_ConstantStackPush_682(i59, o147, a110, i60, i58, a111, i12, env, static) -{1,1}> next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 0 < a111
next_IntArithmetic_684(i59, o147, iconst_1, a110, i60, i58, a111, i12, env, static) -{1,1}> next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) :|: i59 + iconst_1 = i68 && 0 < a110 && 0 <= i59 && 2 <= i12 && iconst_1 = 1 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_FieldAccess_687(i59, o147, i68, a110, i60, i58, a111, i12, env, static) -{1,1}> next_Return_690(i59, a110, i60, i58, o147', a111, i68, i12, env, static) :|: 0 < a110 && o147 < o147' && 0 <= i59 && 2 <= i12 && 0 < o147' && o147' <= o147 + i68 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
next_Return_690(i59, a110, i60, i58, o147, a111, i68, i12, env, static) -{1,1}> take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_692(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{0,0}> take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 0 < a111
take_ArrayAccess_694(a110, i60, i59, i58, o147, a111, i68, i12, env, static) -{1,1}> take_Inc_696(i58, o147, a110', i60, a111, i68, i12, env, static) :|: 0 < a110 && 0 <= i59 && 2 <= i12 && a110' <= a110 + i59 && 0 < o147 && 0 <= i60 && 1 <= i58 && i60 < i58 && 1 <= i68 && 0 < a110' && 0 < a111
take_Inc_696(i58, o147, a110, i60, a111, i68, i12, env, static) -{1,1}> take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 0 <= i60 && 1 <= i58 && 1 <= i68 && 1 <= i70 && i60 + 1 = i70 && 0 < a111
take_JMP_698(i58, o147, a110, i70, a111, i68, i12, env, static) -{1,1}> take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 < o147 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111
take_Load_699(i58, o147, a110, i70, a111, i68, i12, env, static) -{0,0}> take_Load_645(i58, o147, a110, i70, a111, i68, i12, env, static) :|: 0 < a110 && 2 <= i12 && 0 <= i70 && 0 < o147 && 0 <= i58 && 0 <= i68 && 1 <= i58 && 1 <= i68 && 1 <= i70 && 0 < a111

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{44,44}> take_Load_645(i13', o30''', a75', 0, o2, i8', i4', env, static'1) :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
take_Load_645(i58, o147, a110, i60, a111, i59, i12, env, static) -{23,23}> take_Load_645(i58, o147''', a110''', i70', a111, i68', i12, env, static) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''

(35) 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)
take_Load_645(x1, x2, x3, x4, x5, x6, x7, x8, x9) → take_Load_645(x1, x2, x3, x4, x5, x6, x7)

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', a75', 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i70', a111, i68', i12) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''

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

Moved arithmethic from constraints to rhss.

main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', a75', 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
was transformed to
main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', i13' + 2, 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'

take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i70', a111, i68', i12) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''
was transformed to
take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i60 + 1, a111, i59 + 1, i12) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''

(38) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', i13' + 2, 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i60 + 1, a111, i59 + 1, i12) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''

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

Simplified expressions.

main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', i13' + 2, 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 < a75' && 0 <= i4' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= o8' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && 0 <= 2 && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 < o8' && i8' <= o8' && 0 <= 1 && o30''' <= 1 + i8' && 0 < i4' && 0 <= o18' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2 && 1 <= i4'
was transformed to
main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', i13' + 2, 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 <= static'1 && 0 < a75' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < o8' && i8' <= o8' && o30''' <= 1 + i8' && 0 < i4' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2

take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i60 + 1, a111, i59 + 1, i12) :|: i59 + 1 = i68' && 0 < a111 && 0 < 1 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''
was transformed to
take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i60 + 1, a111, i59 + 1, i12) :|: i59 + 1 = i68' && 0 < a111 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''

(40) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
take_Load_645(i58, o147, a110, i60, a111, i59, i12) -{23,23}> take_Load_645(i58, o147''', a110''', i60 + 1, a111, i59 + 1, i12) :|: i59 + 1 = i68' && 0 < a111 && 1 <= i70' && i60 + 1 = i70' && 1 <= i68' && 0 <= i58 && 1 <= i58 && a110''' <= a110 + i59 && 0 <= i68' && 0 < o147 && 0 <= i60 && 0 < o147''' && 0 < a110''' && 0 <= i70' && 2 <= i12 && o147''' <= o147 + i68' && i60 < i58 && 0 < a110 && 0 <= i59 && o147 < o147'''
main_Load_2(o2, static) -{44,44}> take_Load_645(i13', o30''', i13' + 2, 0, o2, i8', i4') :|: o18' < o2 && 0 < o2 && 0 <= static'1 && 0 < a75' && 0 <= i13' && 0 < o18' && 2 <= i4' && 0 <= i8' && a75' = i13' + 2 && 0 < o30''' && i13' <= o18' && 1 < i4' && 0 <= static && o8' < o2 && 0 <= static''' && static''' <= static + 2 && 0 < o8' && i8' <= o8' && o30''' <= 1 + i8' && 0 < i4' && 1 <= o30''' && static'1 <= static''' + 1 && i4' < o2

(41) koat Proof (EQUIVALENT transformation)

YES(?, 23*ar_0 + 44)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 23) take_Load_645(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(ar_0, o147''', a110''', ar_3 + 1, ar_4, ar_5 + 1, ar_6)) [ ar_5 + 1 = i68' /\ 0 < ar_4 /\ 1 <= i70' /\ ar_3 + 1 = i70' /\ 1 <= i68' /\ 0 <= ar_0 /\ 1 <= ar_0 /\ a110''' <= ar_2 + ar_5 /\ 0 <= i68' /\ 0 < ar_1 /\ 0 <= ar_3 /\ 0 < o147''' /\ 0 < a110''' /\ 0 <= i70' /\ 2 <= ar_6 /\ o147''' <= ar_1 + i68' /\ ar_3 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_5 /\ ar_1 < o147''' ]
(Comp: ?, Cost: 44) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(i13', o30''', i13' + 2, 0, ar_0, i8', i4')) [ o18' < ar_0 /\ 0 < ar_0 /\ 0 <= static'1 /\ 0 < a75' /\ 0 <= i13' /\ 0 < o18' /\ 2 <= i4' /\ 0 <= i8' /\ a75' = i13' + 2 /\ 0 < o30''' /\ i13' <= o18' /\ 1 < i4' /\ 0 <= ar_1 /\ o8' < ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 < o8' /\ i8' <= o8' /\ o30''' <= i8' + 1 /\ 0 < i4' /\ 1 <= o30''' /\ static'1 <= static''' + 1 /\ i4' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 23) take_Load_645(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(ar_0, o147''', a110''', ar_3 + 1, ar_4, ar_5 + 1, ar_6)) [ ar_5 + 1 = i68' /\ 0 < ar_4 /\ 1 <= i70' /\ ar_3 + 1 = i70' /\ 1 <= i68' /\ 0 <= ar_0 /\ 1 <= ar_0 /\ a110''' <= ar_2 + ar_5 /\ 0 <= i68' /\ 0 < ar_1 /\ 0 <= ar_3 /\ 0 < o147''' /\ 0 < a110''' /\ 0 <= i70' /\ 2 <= ar_6 /\ o147''' <= ar_1 + i68' /\ ar_3 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_5 /\ ar_1 < o147''' ]
(Comp: 1, Cost: 44) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(i13', o30''', i13' + 2, 0, ar_0, i8', i4')) [ o18' < ar_0 /\ 0 < ar_0 /\ 0 <= static'1 /\ 0 < a75' /\ 0 <= i13' /\ 0 < o18' /\ 2 <= i4' /\ 0 <= i8' /\ a75' = i13' + 2 /\ 0 < o30''' /\ i13' <= o18' /\ 1 < i4' /\ 0 <= ar_1 /\ o8' < ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 < o8' /\ i8' <= o8' /\ o30''' <= i8' + 1 /\ 0 < i4' /\ 1 <= o30''' /\ static'1 <= static''' + 1 /\ i4' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(take_Load_645) = V_1 - V_4
Pol(main_Load_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
take_Load_645(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(ar_0, o147''', a110''', ar_3 + 1, ar_4, ar_5 + 1, ar_6)) [ ar_5 + 1 = i68' /\ 0 < ar_4 /\ 1 <= i70' /\ ar_3 + 1 = i70' /\ 1 <= i68' /\ 0 <= ar_0 /\ 1 <= ar_0 /\ a110''' <= ar_2 + ar_5 /\ 0 <= i68' /\ 0 < ar_1 /\ 0 <= ar_3 /\ 0 < o147''' /\ 0 < a110''' /\ 0 <= i70' /\ 2 <= ar_6 /\ o147''' <= ar_1 + i68' /\ ar_3 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_5 /\ ar_1 < o147''' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0, Cost: 23) take_Load_645(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(ar_0, o147''', a110''', ar_3 + 1, ar_4, ar_5 + 1, ar_6)) [ ar_5 + 1 = i68' /\ 0 < ar_4 /\ 1 <= i70' /\ ar_3 + 1 = i70' /\ 1 <= i68' /\ 0 <= ar_0 /\ 1 <= ar_0 /\ a110''' <= ar_2 + ar_5 /\ 0 <= i68' /\ 0 < ar_1 /\ 0 <= ar_3 /\ 0 < o147''' /\ 0 < a110''' /\ 0 <= i70' /\ 2 <= ar_6 /\ o147''' <= ar_1 + i68' /\ ar_3 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_5 /\ ar_1 < o147''' ]
(Comp: 1, Cost: 44) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(take_Load_645(i13', o30''', i13' + 2, 0, ar_0, i8', i4')) [ o18' < ar_0 /\ 0 < ar_0 /\ 0 <= static'1 /\ 0 < a75' /\ 0 <= i13' /\ 0 < o18' /\ 2 <= i4' /\ 0 <= i8' /\ a75' = i13' + 2 /\ 0 < o30''' /\ i13' <= o18' /\ 1 < i4' /\ 0 <= ar_1 /\ o8' < ar_0 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 < o8' /\ i8' <= o8' /\ o30''' <= i8' + 1 /\ 0 < i4' /\ 1 <= o30''' /\ static'1 <= static''' + 1 /\ i4' < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 23*ar_0 + 44

Time: 0.626 sec (SMT: 0.577 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(115)) 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) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, 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) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(115)) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

(41) koat Proof (EQUIVALENT transformation)

(42) BOUNDS(CONSTANT, 44 + 23 * |args|)