time complexity proof of /tmp/tmpAL4kQu/Take.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 123 + 56 * |#1|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 136 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 61 ms)

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

        ↳19 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)

        ↳20 WeightedIntTrs

↳21 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(50)), 9 ms)

↳22 JBCComplexityEdges

    ↳23 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 162 ms)

    ↳24 WeightedIntTrs

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

    ↳26 WeightedIntTrs

    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 43 ms)

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 494 ms)

    ↳34 BOUNDS(CONSTANT, 73 + 56 * |#1|)

(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(int start, int howMany) {
        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(II)V: Graph of 127 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 76 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 76 jbc graph edges to a weighted ITS with 79 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 79 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(i2, i3, env, static) -{0,0}> main_New_3(i2, i3, env, static) :|: 0 >= 0
main_New_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 >= 0
main_New_48(i2, i3, env, static) -{0,0}> main_New_52(i2, i3, env, static) :|: 0 <= static
main_New_52(i2, i3, env, static) -{0,0}> main_New_53(i2, i3, env, static) :|: 0 >= 0
main_New_53(i2, i3, env, static) -{0,0}> main_New_55(i2, i3, env, static) :|: 0 >= 0
main_New_55(i2, i3, env, static) -{0,0}> main_New_57(i2, i3, env, static) :|: 0 >= 0
main_New_57(i2, i3, env, static) -{1,1}> main_Duplicate_59(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_59(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{1,1}> main_Store_70(i2, i3, o4, env, static) :|: 0 < o4
main_Store_70(i2, i3, o4, env, static) -{1,1}> main_Load_72(i2, i3, o4, env, static) :|: 0 < o4
main_Load_72(i2, i3, o4, env, static) -{1,1}> main_Load_75(i2, i3, o4, env, static) :|: 0 < o4
main_Load_75(i2, i3, o4, env, static) -{1,1}> main_InvokeMethod_76(i2, i3, o4, env, static) :|: 0 < o4
main_InvokeMethod_76(i2, i3, o4, env, static) -{1,1}> take_Load_78(i3, o4, i2, env, static) :|: 0 < o4
take_Load_78(i3, o4, i2, env, static) -{1,1}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
take_ArrayCreate_82(i11, o4, i2, env, static) -{0,0}> take_ArrayCreate_84(i11, o4, i2, env, static) :|: 0 < o4 && i11 <= -1
take_ArrayCreate_82(i12, o4, i2, env, static) -{0,0}> take_ArrayCreate_85(i12, o4, i2, env, static) :|: 0 < o4 && 0 <= i12
take_ArrayCreate_85(i12, o4, i2, env, static) -{1,1}> take_Store_88(a3, i12, o4, i2, env, static) :|: 0 < a3 && a3 = i12 + 2 && 0 < o4 && 0 <= i12
take_Store_88(a3, i12, o4, i2, env, static) -{1,1}> take_ConstantStackPush_91(i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && 0 <= i12
take_ConstantStackPush_91(i12, o4, a3, i2, env, static) -{1,1}> take_Store_92(iconst_0, i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Store_92(iconst_0, i12, o4, a3, i2, env, static) -{1,1}> take_Load_94(i12, o4, a3, iconst_0, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Load_94(i12, o4, a3, iconst_0, i2, env, static) -{0,0}> take_Load_203(i12, o4, a3, iconst_0, i2, i2, env, static) :|: 0 < a3 && 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && 0 <= i12
take_Load_203(i22, o10, a8, i24, i2, i23, env, static) -{0,0}> take_Load_295(i22, o10, a8, i24, i2, i23, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 <= i22 && 0 < o10 && 0 < a8
take_Load_295(i37, o19, a16, i39, i2, i38, env, static) -{0,0}> take_Load_380(i37, o19, a16, i39, i2, i38, env, static) :|: 0 < a16 && 0 <= i39 && 0 < o19 && 0 <= i37 && i39 <= 2
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_382(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_Load_382(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_393(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24 && i52 <= i54
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_394(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_GE_394(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_Load_396(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_Load_396(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) -{1,1}> hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_412(i52, o28, a24, i54, i2, i53, env, static) :|: 0 < iconst_1 && 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_Load_412(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_414(a24, i52, o28, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_414(a24, i52, o28, i54, i2, i53, env, static) -{1,1}> take_Load_416(a24, i54, i52, o28, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_416(a24, i54, i52, o28, i2, i53, env, static) -{1,1}> take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) -{1,1}> next_Load_419(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Load_419(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) -{1,1}> next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) -{1,1}> next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) -{1,1}> next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) :|: 1 <= i52 && i53 + iconst_1 = i61 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_446(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{1,1}> take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && i54 + 1 = i63 && 0 <= i54 && 0 < a24
take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) -{1,1}> take_Load_453(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24
take_Load_453(i52, o28, a24, i63, i2, i61, env, static) -{0,0}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24 && 0 <= i63

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

obtained
main_New_1(i2, i3, env, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
by chaining
main_New_1(i2, i3, env, static) -{0,0}> main_New_3(i2, i3, env, static) :|: 0 >= 0
main_New_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 >= 0
main_New_48(i2, i3, env, static) -{0,0}> main_New_52(i2, i3, env, static) :|: 0 <= static
main_New_52(i2, i3, env, static) -{0,0}> main_New_53(i2, i3, env, static) :|: 0 >= 0
main_New_53(i2, i3, env, static) -{0,0}> main_New_55(i2, i3, env, static) :|: 0 >= 0
main_New_55(i2, i3, env, static) -{0,0}> main_New_57(i2, i3, env, static) :|: 0 >= 0
main_New_57(i2, i3, env, static) -{1,1}> main_Duplicate_59(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_59(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0

obtained
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{6,6}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
by chaining
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{1,1}> main_Store_70(i2, i3, o4, env, static) :|: 0 < o4
main_Store_70(i2, i3, o4, env, static) -{1,1}> main_Load_72(i2, i3, o4, env, static) :|: 0 < o4
main_Load_72(i2, i3, o4, env, static) -{1,1}> main_Load_75(i2, i3, o4, env, static) :|: 0 < o4
main_Load_75(i2, i3, o4, env, static) -{1,1}> main_InvokeMethod_76(i2, i3, o4, env, static) :|: 0 < o4
main_InvokeMethod_76(i2, i3, o4, env, static) -{1,1}> take_Load_78(i3, o4, i2, env, static) :|: 0 < o4
take_Load_78(i3, o4, i2, env, static) -{1,1}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4

obtained
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, a3', 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
by chaining
take_ArrayCreate_82(i12, o4, i2, env, static) -{0,0}> take_ArrayCreate_85(i12, o4, i2, env, static) :|: 0 < o4 && 0 <= i12
take_ArrayCreate_85(i12, o4, i2, env, static) -{1,1}> take_Store_88(a3, i12, o4, i2, env, static) :|: 0 < a3 && a3 = i12 + 2 && 0 < o4 && 0 <= i12
take_Store_88(a3, i12, o4, i2, env, static) -{1,1}> take_ConstantStackPush_91(i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && 0 <= i12
take_ConstantStackPush_91(i12, o4, a3, i2, env, static) -{1,1}> take_Store_92(iconst_0, i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Store_92(iconst_0, i12, o4, a3, i2, env, static) -{1,1}> take_Load_94(i12, o4, a3, iconst_0, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Load_94(i12, o4, a3, iconst_0, i2, env, static) -{0,0}> take_Load_203(i12, o4, a3, iconst_0, i2, i2, env, static) :|: 0 < a3 && 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && 0 <= i12
take_Load_203(i22, o10, a8, i24, i2, i23, env, static) -{0,0}> take_Load_295(i22, o10, a8, i24, i2, i23, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 <= i22 && 0 < o10 && 0 < a8
take_Load_295(i37, o19, a16, i39, i2, i38, env, static) -{0,0}> take_Load_380(i37, o19, a16, i39, i2, i38, env, static) :|: 0 < a16 && 0 <= i39 && 0 < o19 && 0 <= i37 && i39 <= 2

obtained
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{2,2}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < a24 && 0 < o28 && 0 <= i54
by chaining
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_382(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_Load_382(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24

obtained
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'
by chaining
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_394(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_GE_394(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_Load_396(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_Load_396(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) -{1,1}> hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_412(i52, o28, a24, i54, i2, i53, env, static) :|: 0 < iconst_1 && 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_Load_412(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_414(a24, i52, o28, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_414(a24, i52, o28, i54, i2, i53, env, static) -{1,1}> take_Load_416(a24, i54, i52, o28, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_416(a24, i54, i52, o28, i2, i53, env, static) -{1,1}> take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) -{1,1}> next_Load_419(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Load_419(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) -{1,1}> next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) -{1,1}> next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) -{1,1}> next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) :|: 1 <= i52 && i53 + iconst_1 = i61 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24

obtained
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
by chaining
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{1,1}> take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && i54 + 1 = i63 && 0 <= i54 && 0 < a24
take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) -{1,1}> take_Load_453(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24
take_Load_453(i52, o28, a24, i63, i2, i61, env, static) -{0,0}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24 && 0 <= i63

(8) Obligation:

IntTrs with 17 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(i2, i3, env, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{6,6}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
take_ArrayCreate_82(i11, o4, i2, env, static) -{0,0}> take_ArrayCreate_84(i11, o4, i2, env, static) :|: 0 < o4 && i11 <= -1
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, a3', 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{2,2}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < a24 && 0 < o28 && 0 <= i54
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_393(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24 && i52 <= i54
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_446(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

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

Moved arithmethic from constraints to rhss.

take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
was transformed to
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'
was transformed to
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'

take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, a3', 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
was transformed to
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, i12 + 2, 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1

(10) Obligation:

IntTrs with 17 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_393(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24 && i52 <= i54
take_ArrayCreate_82(i11, o4, i2, env, static) -{0,0}> take_ArrayCreate_84(i11, o4, i2, env, static) :|: 0 < o4 && i11 <= -1
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{6,6}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, i12 + 2, 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_446(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{2,2}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < a24 && 0 < o28 && 0 <= i54
main_New_1(i2, i3, env, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0

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

Simplified expressions.

take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && 0 < 1 && i53 + 1 = i61'
was transformed to
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && i53 + 1 = i61'

take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, i12 + 2, 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
was transformed to
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, i12 + 2, 0, i2, i2, env, static) :|: 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3'

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

(12) Obligation:

IntTrs with 17 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_393(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24 && i52 <= i54
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{6,6}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
take_ArrayCreate_82(i11, o4, i2, env, static) -{0,0}> take_ArrayCreate_84(i11, o4, i2, env, static) :|: 0 < o4 && i11 <= -1
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_446(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{16,16}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52, i2, env, static) :|: i54 < i52 && 0 < a24 && 1 <= i52 && 0 <= i54 && 0 < o28 && i53 + 1 = i61'
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{2,2}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < a24 && 0 < o28 && 0 <= i54
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayCreate_82(i12, o4, i2, env, static) -{4,4}> take_Load_380(i12, o4, i12 + 2, 0, i2, i2, env, static) :|: 0 <= i12 && a3' = i12 + 2 && 0 < o4 && 0 < a3'
main_New_1(i2, i3, env, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

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

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

(14) Obligation:

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

(16) Obligation:

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

Moved arithmethic from constraints to rhss.

(18) Obligation:

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

Simplified expressions.

(20) Obligation:

(21) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(50)) transformation)

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

(22) Obligation:

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

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

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 76 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_New_1(i2, i3, env, static) -{0,0}> main_New_3(i2, i3, env, static) :|: 0 >= 0
main_New_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 >= 0
main_New_48(i2, i3, env, static) -{0,0}> main_New_52(i2, i3, env, static) :|: 0 <= static
main_New_52(i2, i3, env, static) -{0,0}> main_New_53(i2, i3, env, static) :|: 0 >= 0
main_New_53(i2, i3, env, static) -{0,0}> main_New_55(i2, i3, env, static) :|: 0 >= 0
main_New_55(i2, i3, env, static) -{0,0}> main_New_57(i2, i3, env, static) :|: 0 >= 0
main_New_57(i2, i3, env, static) -{1,1}> main_Duplicate_59(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_59(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_61(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_62(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_63(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_64(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_65(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{1,1}> main_Store_70(i2, i3, o4, env, static) :|: 0 < o4
main_Store_70(i2, i3, o4, env, static) -{1,1}> main_Load_72(i2, i3, o4, env, static) :|: 0 < o4
main_Load_72(i2, i3, o4, env, static) -{1,1}> main_Load_75(i2, i3, o4, env, static) :|: 0 < o4
main_Load_75(i2, i3, o4, env, static) -{1,1}> main_InvokeMethod_76(i2, i3, o4, env, static) :|: 0 < o4
main_InvokeMethod_76(i2, i3, o4, env, static) -{1,1}> take_Load_78(i3, o4, i2, env, static) :|: 0 < o4
take_Load_78(i3, o4, i2, env, static) -{1,1}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
take_ArrayCreate_82(i12, o4, i2, env, static) -{0,0}> take_ArrayCreate_85(i12, o4, i2, env, static) :|: 0 < o4 && 0 <= i12
take_ArrayCreate_85(i12, o4, i2, env, static) -{1,1}> take_Store_88(a3, i12, o4, i2, env, static) :|: 0 < a3 && a3 = i12 + 2 && 0 < o4 && 0 <= i12
take_Store_88(a3, i12, o4, i2, env, static) -{1,1}> take_ConstantStackPush_91(i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && 0 <= i12
take_ConstantStackPush_91(i12, o4, a3, i2, env, static) -{1,1}> take_Store_92(iconst_0, i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Store_92(iconst_0, i12, o4, a3, i2, env, static) -{1,1}> take_Load_94(i12, o4, a3, iconst_0, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Load_94(i12, o4, a3, iconst_0, i2, env, static) -{0,0}> take_Load_203(i12, o4, a3, iconst_0, i2, i2, env, static) :|: 0 < a3 && 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && 0 <= i12
take_Load_203(i22, o10, a8, i24, i2, i23, env, static) -{0,0}> take_Load_295(i22, o10, a8, i24, i2, i23, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 <= i22 && 0 < o10 && 0 < a8
take_Load_295(i37, o19, a16, i39, i2, i38, env, static) -{0,0}> take_Load_380(i37, o19, a16, i39, i2, i38, env, static) :|: 0 < a16 && 0 <= i39 && 0 < o19 && 0 <= i37 && i39 <= 2
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_382(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_Load_382(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_394(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_GE_394(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_Load_396(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_Load_396(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) -{1,1}> hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_412(i52, o28, a24, i54, i2, i53, env, static) :|: 0 < iconst_1 && 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_Load_412(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_414(a24, i52, o28, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_414(a24, i52, o28, i54, i2, i53, env, static) -{1,1}> take_Load_416(a24, i54, i52, o28, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_416(a24, i54, i52, o28, i2, i53, env, static) -{1,1}> take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) -{1,1}> next_Load_419(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Load_419(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) -{1,1}> next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) -{1,1}> next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) -{1,1}> next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) :|: 1 <= i52 && i53 + iconst_1 = i61 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{1,1}> take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && i54 + 1 = i63 && 0 <= i54 && 0 < a24
take_JMP_451(i52, o28, a24, i63, i2, i61, env, static) -{1,1}> take_Load_453(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24
take_Load_453(i52, o28, a24, i63, i2, i61, env, static) -{0,0}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i52 && 1 <= i63 && 0 < o28 && 0 < a24 && 0 <= i63

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

obtained
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{10,10}> take_Load_380(i3, o4, a3', 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
by chaining
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{1,1}> main_Store_70(i2, i3, o4, env, static) :|: 0 < o4
main_Store_70(i2, i3, o4, env, static) -{1,1}> main_Load_72(i2, i3, o4, env, static) :|: 0 < o4
main_Load_72(i2, i3, o4, env, static) -{1,1}> main_Load_75(i2, i3, o4, env, static) :|: 0 < o4
main_Load_75(i2, i3, o4, env, static) -{1,1}> main_InvokeMethod_76(i2, i3, o4, env, static) :|: 0 < o4
main_InvokeMethod_76(i2, i3, o4, env, static) -{1,1}> take_Load_78(i3, o4, i2, env, static) :|: 0 < o4
take_Load_78(i3, o4, i2, env, static) -{1,1}> take_ArrayCreate_82(i3, o4, i2, env, static) :|: 0 < o4
take_ArrayCreate_82(i12, o4, i2, env, static) -{0,0}> take_ArrayCreate_85(i12, o4, i2, env, static) :|: 0 < o4 && 0 <= i12
take_ArrayCreate_85(i12, o4, i2, env, static) -{1,1}> take_Store_88(a3, i12, o4, i2, env, static) :|: 0 < a3 && a3 = i12 + 2 && 0 < o4 && 0 <= i12
take_Store_88(a3, i12, o4, i2, env, static) -{1,1}> take_ConstantStackPush_91(i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && 0 <= i12
take_ConstantStackPush_91(i12, o4, a3, i2, env, static) -{1,1}> take_Store_92(iconst_0, i12, o4, a3, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Store_92(iconst_0, i12, o4, a3, i2, env, static) -{1,1}> take_Load_94(i12, o4, a3, iconst_0, i2, env, static) :|: 0 < a3 && 0 < o4 && iconst_0 = 0 && 0 <= i12
take_Load_94(i12, o4, a3, iconst_0, i2, env, static) -{0,0}> take_Load_203(i12, o4, a3, iconst_0, i2, i2, env, static) :|: 0 < a3 && 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0 && 0 <= i12
take_Load_203(i22, o10, a8, i24, i2, i23, env, static) -{0,0}> take_Load_295(i22, o10, a8, i24, i2, i23, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2 && 0 <= i22 && 0 < o10 && 0 < a8
take_Load_295(i37, o19, a16, i39, i2, i38, env, static) -{0,0}> take_Load_380(i37, o19, a16, i39, i2, i38, env, static) :|: 0 < a16 && 0 <= i39 && 0 < o19 && 0 <= i37 && i39 <= 2

obtained
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{18,18}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52, i2, env, static) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
by chaining
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_382(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_Load_382(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_GE_391(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && 0 <= i54 && 0 < a24
take_GE_391(i54, i52, o28, a24, i2, i53, env, static) -{0,0}> take_GE_394(i54, i52, o28, a24, i2, i53, env, static) :|: 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_GE_394(i54, i52, o28, a24, i2, i53, env, static) -{1,1}> take_Load_396(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24
take_Load_396(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_398(o28, i52, a24, i54, i2, i53, env, static) -{1,1}> hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
hasNext_ConstantStackPush_402(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
hasNext_Return_408(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_EQ_410(iconst_1, i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_412(i52, o28, a24, i54, i2, i53, env, static) :|: 0 < iconst_1 && 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
take_Load_412(i52, o28, a24, i54, i2, i53, env, static) -{1,1}> take_Load_414(a24, i52, o28, i54, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_414(a24, i52, o28, i54, i2, i53, env, static) -{1,1}> take_Load_416(a24, i54, i52, o28, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_Load_416(a24, i54, i52, o28, i2, i53, env, static) -{1,1}> take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_InvokeMethod_417(a24, i54, o28, i52, i2, i53, env, static) -{1,1}> next_Load_419(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Load_419(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_420(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_FieldAccess_422(o28, a24, i54, i52, i2, i53, env, static) -{1,1}> next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_Duplicate_435(o28, i53, a24, i54, i52, i2, env, static) -{1,1}> next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
next_ConstantStackPush_438(i53, o28, a24, i54, i52, i2, env, static) -{1,1}> next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) :|: 1 <= i52 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24
next_IntArithmetic_440(i53, o28, iconst_1, a24, i54, i52, i2, env, static) -{1,1}> next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) :|: 1 <= i52 && i53 + iconst_1 = i61 && 0 < o28 && iconst_1 = 1 && 0 <= i54 && 0 < a24

obtained
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 0 < a24 && 0 <= i54 && 1 <= i52 && 0 < o28
by chaining
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24
take_ArrayAccess_444(a24, i54, i53, i52, o28, i2, i61, env, static) -{0,0}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 1 <= i52 && 0 < o28 && 0 <= i54 && 0 < a24

(26) Obligation:

IntTrs with 11 rules
Start term: main_New_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_New_1(i2, i3, env, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4, env, static) -{10,10}> take_Load_380(i3, o4, a3', 0, i2, i2, env, static) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
take_Load_380(i52, o28, a24, i54, i2, i53, env, static) -{18,18}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52, i2, env, static) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52, i2, env, static) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i2, i61, env, static) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
next_Return_443(i53, a24, i54, i52, o28, i2, i61, env, static) -{1,1}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) :|: 0 < a24 && 0 <= i54 && 1 <= i52 && 0 < o28
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_ArrayAccess_445(a24, i54, i53, i52, o28, i2, i61, env, static) -{1,1}> take_Inc_449(i52, o28, a24', i54, i2, i61, env, static) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_Inc_449(i52, o28, a24, i54, i2, i61, env, static) -{2,2}> take_Load_380(i52, o28, a24, i63, i2, i61, env, static) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

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

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

main_New_1(x1, x2, x3, x4) → main_New_1(x1, x2, x4)
langle_init_rangle_FieldAccess_66(x1, x2, x3, x4, x5, x6) → langle_init_rangle_FieldAccess_66(x1, x2, x3, x4)
langle_init_rangle_Return_68(x1, x2, x3, x4, x5) → langle_init_rangle_Return_68(x1, x2, x3)
take_Load_380(x1, x2, x3, x4, x5, x6, x7, x8) → take_Load_380(x1, x2, x3, x4, x6)
next_FieldAccess_442(x1, x2, x3, x4, x5, x6, x7, x8, x9) → next_FieldAccess_442(x1, x2, x3, x4, x5, x6)
next_Return_443(x1, x2, x3, x4, x5, x6, x7, x8, x9) → next_Return_443(x1, x2, x3, x4, x5, x7)
take_ArrayAccess_445(x1, x2, x3, x4, x5, x6, x7, x8, x9) → take_ArrayAccess_445(x1, x2, x3, x4, x5, x7)
take_Inc_449(x1, x2, x3, x4, x5, x6, x7, x8) → take_Inc_449(x1, x2, x3, x4, x6)

(28) Obligation:

IntTrs with 11 rules
Start term: main_New_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_New_1(i2, i3, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, a3', 0, i2) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
next_Return_443(i53, a24, i54, i52, o28, i61) -{1,1}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) :|: 0 < a24 && 0 <= i54 && 1 <= i52 && 0 < o28
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
take_Inc_449(i52, o28, a24, i54, i61) -{2,2}> take_Load_380(i52, o28, a24, i63, i61) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

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

Moved arithmethic from constraints to rhss.

take_Inc_449(i52, o28, a24, i54, i61) -{2,2}> take_Load_380(i52, o28, a24, i63, i61) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
was transformed to
take_Inc_449(i52, o28, a24, i54, i61) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i61) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54

take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i61', a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
was transformed to
take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'

langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, a3', 0, i2) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
was transformed to
langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, i3 + 2, 0, i2) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1

(30) Obligation:

IntTrs with 11 rules
Start term: main_New_1(#0, #1, static)
Considered paths: all paths from start
Rules:
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
main_New_1(i2, i3, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0) :|: static'1 <= static''' + 1 && 0 < 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 < 2 && 0 <= static'1
take_Inc_449(i52, o28, a24, i54, i61) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i61) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
next_Return_443(i53, a24, i54, i52, o28, i61) -{1,1}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) :|: 0 < a24 && 0 <= i54 && 1 <= i52 && 0 < o28
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, i3 + 2, 0, i2) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1

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

Simplified expressions.

langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, i3 + 2, 0, i2) :|: 0 <= 2 && 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3' && 0 <= 0 && 0 <= 1
was transformed to
langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, i3 + 2, 0, i2) :|: 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3'

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

take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && 0 < 1 && i53 + 1 = i61'
was transformed to
take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && i53 + 1 = i61'

(32) Obligation:

IntTrs with 11 rules
Start term: main_New_1(#0, #1, static)
Considered paths: all paths from start
Rules:
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: o28' <= o28 + i61 && 1 <= i52 && 0 < o28 && 0 < o28' && 0 < i61 && 0 <= i54 && 0 < a24
take_Inc_449(i52, o28, a24, i54, i61) -{2,2}> take_Load_380(i52, o28, a24, i54 + 1, i61) :|: 1 <= i63 && 0 <= i63 && 1 <= i52 && 0 < a24 && i54 + 1 = i63 && 0 < o28 && 0 <= i54
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && 0 < i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && a24' <= a24 + i53
take_Load_380(i52, o28, a24, i54, i53) -{18,18}> next_FieldAccess_442(i53, o28, i53 + 1, a24, i54, i52) :|: 0 < o28 && 0 < a24 && 1 <= i52 && 0 <= i54 && i54 < i52 && i53 + 1 = i61'
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
next_Return_443(i53, a24, i54, i52, o28, i61) -{1,1}> take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) :|: 0 < a24 && 0 <= i54 && 1 <= i52 && 0 < o28
main_New_1(i2, i3, static) -{23,23}> langle_init_rangle_FieldAccess_66(1, i2, i3, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
langle_init_rangle_Return_68(i2, i3, o4) -{10,10}> take_Load_380(i3, o4, i3 + 2, 0, i2) :|: 0 <= i3 && a3' = i3 + 2 && 0 < o4 && 0 < a3'
next_FieldAccess_442(i53, o28, i61, a24, i54, i52) -{1,1}> next_Return_443(i53, a24, i54, i52, o28', i61) :|: 1 <= i52 && o28' <= o28 + -1 * i61 && 0 < o28 && 0 < o28' && 0 <= i54 && 0 < a24 && i61 <= 0
take_ArrayAccess_445(a24, i54, i53, i52, o28, i61) -{1,1}> take_Inc_449(i52, o28, a24', i54, i61) :|: 1 <= i52 && a24' <= a24 + -1 * i53 && 0 < o28 && i54 < i52 && 0 <= i54 && 0 < a24 && 0 < a24' && i53 <= 0
langle_init_rangle_FieldAccess_66(o4, i2, i3, iconst_0) -{1,1}> langle_init_rangle_Return_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'

(33) koat Proof (EQUIVALENT transformation)

YES(?, 56*ar_1 + 73)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ o28' <= ar_1 + ar_2 /\ 1 <= ar_5 /\ 0 < ar_1 /\ 0 < o28' /\ 0 < ar_2 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 2) take_Inc_449(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_0, ar_1, ar_2, ar_3 + 1, ar_4, arityPad)) [ 1 <= i63 /\ 0 <= i63 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_3 + 1 = i63 /\ 0 < ar_1 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ a24' <= ar_0 + ar_2 ]
(Comp: ?, Cost: 18) take_Load_380(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_FieldAccess_442(ar_4, ar_1, ar_4 + 1, ar_2, ar_3, ar_0)) [ 0 < ar_1 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 <= ar_3 /\ ar_3 < ar_0 /\ ar_4 + 1 = i61' ]
(Comp: ?, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ ar_1 <= 0 /\ o4' <= ar_0 - ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: ?, Cost: 1) next_Return_443(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_ArrayAccess_445(ar_1, ar_2, ar_0, ar_3, ar_4, ar_5)) [ 0 < ar_1 /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_4 ]
(Comp: ?, Cost: 23) main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_FieldAccess_66(1, ar_0, ar_1, 0, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 10) langle_init_rangle_Return_68(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_1, ar_2, ar_1 + 2, 0, ar_0, arityPad)) [ 0 <= ar_1 /\ a3' = ar_1 + 2 /\ 0 < ar_2 /\ 0 < a3' ]
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ 1 <= ar_5 /\ o28' <= ar_1 - ar_2 /\ 0 < ar_1 /\ 0 < o28' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ a24' <= ar_0 - ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ ar_2 <= 0 ]
(Comp: ?, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ o4' <= ar_0 + ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < ar_1 /\ 0 < o4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ o28' <= ar_1 + ar_2 /\ 1 <= ar_5 /\ 0 < ar_1 /\ 0 < o28' /\ 0 < ar_2 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 2) take_Inc_449(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_0, ar_1, ar_2, ar_3 + 1, ar_4, arityPad)) [ 1 <= i63 /\ 0 <= i63 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_3 + 1 = i63 /\ 0 < ar_1 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ a24' <= ar_0 + ar_2 ]
(Comp: ?, Cost: 18) take_Load_380(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_FieldAccess_442(ar_4, ar_1, ar_4 + 1, ar_2, ar_3, ar_0)) [ 0 < ar_1 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 <= ar_3 /\ ar_3 < ar_0 /\ ar_4 + 1 = i61' ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ ar_1 <= 0 /\ o4' <= ar_0 - ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: ?, Cost: 1) next_Return_443(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_ArrayAccess_445(ar_1, ar_2, ar_0, ar_3, ar_4, ar_5)) [ 0 < ar_1 /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_4 ]
(Comp: 1, Cost: 23) main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_FieldAccess_66(1, ar_0, ar_1, 0, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 2, Cost: 10) langle_init_rangle_Return_68(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_1, ar_2, ar_1 + 2, 0, ar_0, arityPad)) [ 0 <= ar_1 /\ a3' = ar_1 + 2 /\ 0 < ar_2 /\ 0 < a3' ]
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ 1 <= ar_5 /\ o28' <= ar_1 - ar_2 /\ 0 < ar_1 /\ 0 < o28' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 <= 0 ]
(Comp: ?, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ a24' <= ar_0 - ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ ar_2 <= 0 ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ o4' <= ar_0 + ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < ar_1 /\ 0 < o4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(next_FieldAccess_442) = -2*V_5 + 2*V_6
Pol(next_Return_443) = -2*V_3 + 2*V_4
Pol(take_Inc_449) = 2*V_1 - 2*V_4 - 1
Pol(take_Load_380) = 2*V_1 - 2*V_4 + 1
Pol(take_ArrayAccess_445) = -2*V_2 + 2*V_4
Pol(langle_init_rangle_FieldAccess_66) = 2*V_3 + 1
Pol(langle_init_rangle_Return_68) = 2*V_2 + 1
Pol(main_New_1) = 2*V_2 + 1
Pol(koat_start) = 2*V_2 + 1
orients all transitions weakly and the transitions
take_Load_380(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_FieldAccess_442(ar_4, ar_1, ar_4 + 1, ar_2, ar_3, ar_0)) [ 0 < ar_1 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 <= ar_3 /\ ar_3 < ar_0 /\ ar_4 + 1 = i61' ]
take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ a24' <= ar_0 + ar_2 ]
take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ a24' <= ar_0 - ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ ar_2 <= 0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ o28' <= ar_1 + ar_2 /\ 1 <= ar_5 /\ 0 < ar_1 /\ 0 < o28' /\ 0 < ar_2 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: ?, Cost: 2) take_Inc_449(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_0, ar_1, ar_2, ar_3 + 1, ar_4, arityPad)) [ 1 <= i63 /\ 0 <= i63 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_3 + 1 = i63 /\ 0 < ar_1 /\ 0 <= ar_3 ]
(Comp: 2*ar_1 + 1, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ a24' <= ar_0 + ar_2 ]
(Comp: 2*ar_1 + 1, Cost: 18) take_Load_380(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_FieldAccess_442(ar_4, ar_1, ar_4 + 1, ar_2, ar_3, ar_0)) [ 0 < ar_1 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 <= ar_3 /\ ar_3 < ar_0 /\ ar_4 + 1 = i61' ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ ar_1 <= 0 /\ o4' <= ar_0 - ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: ?, Cost: 1) next_Return_443(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_ArrayAccess_445(ar_1, ar_2, ar_0, ar_3, ar_4, ar_5)) [ 0 < ar_1 /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_4 ]
(Comp: 1, Cost: 23) main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_FieldAccess_66(1, ar_0, ar_1, 0, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 2, Cost: 10) langle_init_rangle_Return_68(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_1, ar_2, ar_1 + 2, 0, ar_0, arityPad)) [ 0 <= ar_1 /\ a3' = ar_1 + 2 /\ 0 < ar_2 /\ 0 < a3' ]
(Comp: ?, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ 1 <= ar_5 /\ o28' <= ar_1 - ar_2 /\ 0 < ar_1 /\ 0 < o28' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 <= 0 ]
(Comp: 2*ar_1 + 1, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ a24' <= ar_0 - ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ ar_2 <= 0 ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ o4' <= ar_0 + ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < ar_1 /\ 0 < o4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4: T:
(Comp: 2*ar_1 + 1, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ o28' <= ar_1 + ar_2 /\ 1 <= ar_5 /\ 0 < ar_1 /\ 0 < o28' /\ 0 < ar_2 /\ 0 <= ar_4 /\ 0 < ar_3 ]
(Comp: 4*ar_1 + 2, Cost: 2) take_Inc_449(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_0, ar_1, ar_2, ar_3 + 1, ar_4, arityPad)) [ 1 <= i63 /\ 0 <= i63 /\ 1 <= ar_0 /\ 0 < ar_2 /\ ar_3 + 1 = i63 /\ 0 < ar_1 /\ 0 <= ar_3 ]
(Comp: 2*ar_1 + 1, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ a24' <= ar_0 + ar_2 ]
(Comp: 2*ar_1 + 1, Cost: 18) take_Load_380(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_FieldAccess_442(ar_4, ar_1, ar_4 + 1, ar_2, ar_3, ar_0)) [ 0 < ar_1 /\ 0 < ar_2 /\ 1 <= ar_0 /\ 0 <= ar_3 /\ ar_3 < ar_0 /\ ar_4 + 1 = i61' ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ ar_1 <= 0 /\ o4' <= ar_0 - ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: 4*ar_1 + 2, Cost: 1) next_Return_443(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_ArrayAccess_445(ar_1, ar_2, ar_0, ar_3, ar_4, ar_5)) [ 0 < ar_1 /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_4 ]
(Comp: 1, Cost: 23) main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_FieldAccess_66(1, ar_0, ar_1, 0, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 2, Cost: 10) langle_init_rangle_Return_68(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Load_380(ar_1, ar_2, ar_1 + 2, 0, ar_0, arityPad)) [ 0 <= ar_1 /\ a3' = ar_1 + 2 /\ 0 < ar_2 /\ 0 < a3' ]
(Comp: 2*ar_1 + 1, Cost: 1) next_FieldAccess_442(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(next_Return_443(ar_0, ar_3, ar_4, ar_5, o28', ar_2)) [ 1 <= ar_5 /\ o28' <= ar_1 - ar_2 /\ 0 < ar_1 /\ 0 < o28' /\ 0 <= ar_4 /\ 0 < ar_3 /\ ar_2 <= 0 ]
(Comp: 2*ar_1 + 1, Cost: 1) take_ArrayAccess_445(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(take_Inc_449(ar_3, ar_4, a24', ar_1, ar_5, arityPad)) [ 1 <= ar_3 /\ a24' <= ar_0 - ar_2 /\ 0 < ar_4 /\ ar_1 < ar_3 /\ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < a24' /\ ar_2 <= 0 ]
(Comp: 1, Cost: 1) langle_init_rangle_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(langle_init_rangle_Return_68(ar_1, ar_2, o4', arityPad, arityPad, arityPad)) [ o4' <= ar_0 + ar_1 /\ 0 < ar_0 /\ ar_3 = 0 /\ 0 < ar_1 /\ 0 < o4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_New_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 56*ar_1 + 73

Time: 0.523 sec (SMT: 0.440 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

(21) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(50)) transformation)

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 73 + 56 * |#1|)