time complexity proof of /tmp/tmp1C6xiS/PastaC9.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 31 + 18 * |#0| + 24 * |#0| * |#2| + 24 * |#1|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

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

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 113 ms)

    ↳16 BOUNDS(CONSTANT, 28 + 18 * |#0| + 24 * |#0| * |#2| + 24 * |#1|)

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

↳18 JBCComplexityEdges

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

    ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

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

        ↳36 WeightedIntTrs

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

        ↳38 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaC9 {
    public static void main(int x, int y, int z) {
        while (x > 0 && y > 0) {
            if (new Object().hashCode() < 42) {
                x--;
                y = z;
            } else {
                y--;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaC9.main(III)V: Graph of 54 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 50 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, i6, env, static) -{0,0}> main_Load_3(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, i6, env, static) -{1,1}> main_Load_45(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i6, env, static) -{0,0}> main_Load_46(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i3, i6, env, static) -{0,0}> main_Load_49(i1, i3, i6, env, static) :|: 0 <= static
main_Load_49(i1, i3, i6, env, static) -{0,0}> main_Load_50(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i3, i6, env, static) -{0,0}> main_Load_51(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i3, i6, env, static) -{1,1}> main_LE_52(i1, i3, i6, env, static) :|: 0 >= 0
main_LE_52(i1, i3, i6, env, static) -{0,0}> main_LE_96(i1, i3, i6, i3, env, static) :|: 0 >= 0
main_LE_96(i38, i39, i6, i40, env, static) -{0,0}> main_LE_400(i38, i39, i6, i38, i40, env, static) :|: 0 >= 0
main_LE_400(i246, i39, i247, i265, i249, env, static) -{0,0}> main_LE_405(i246, i39, i247, i265, i249, env, static) :|: 1 <= i265
main_LE_405(i246, i39, i247, i265, i249, env, static) -{1,1}> main_Load_409(i246, i39, i247, i265, i249, env, static) :|: 0 < i265 && 1 <= i265
main_Load_409(i246, i39, i247, i265, i249, env, static) -{1,1}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265
main_LE_414(i246, i39, i247, i271, i265, env, static) -{0,0}> main_LE_417(i246, i39, i247, i271, i265, env, static) :|: 1 <= i271 && 1 <= i265
main_LE_417(i246, i39, i247, i271, i265, env, static) -{1,1}> main_New_423(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && 0 < i271 && 1 <= i265
main_New_423(i246, i39, i247, i265, i271, env, static) -{1,1}> main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && o78 = 1 && 0 < o78 && 1 <= i265
main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) -{1,1}> main_GE_437(i246, i39, i247, i274, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 1 <= i265
main_GE_437(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{0,0}> main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && 1 <= i265
main_GE_437(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{0,0}> main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && 1 <= i265
main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_441(i246, i39, i247, i265, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && i282 < iconst_42 && 1 <= i265
main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_443(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && iconst_42 <= i283 && 1 <= i265
main_Inc_441(i246, i39, i247, i265, env, static) -{1,1}> main_Load_444(i246, i39, i247, i284, env, static) :|: i265 + -1 = i284 && 0 <= i284 && 1 <= i265
main_Inc_443(i246, i39, i247, i265, i271, env, static) -{1,1}> main_JMP_445(i246, i39, i247, i265, i285, env, static) :|: 1 <= i271 && i271 + -1 = i285 && 1 <= i265 && 0 <= i285
main_Load_444(i246, i39, i247, i284, env, static) -{1,1}> main_Store_446(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_JMP_445(i246, i39, i247, i265, i285, env, static) -{1,1}> main_Load_457(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_Store_446(i246, i39, i247, i284, env, static) -{1,1}> main_JMP_459(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_Load_457(i246, i39, i247, i265, i285, env, static) -{1,1}> main_LE_462(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_JMP_459(i246, i39, i247, i284, env, static) -{1,1}> main_Load_463(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_LE_462(i246, i39, i247, i265, i285, env, static) -{0,0}> main_LE_400(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_Load_463(i246, i39, i247, i284, env, static) -{1,1}> main_LE_467(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_LE_467(i246, i39, i247, i284, env, static) -{0,0}> main_LE_400(i246, i39, i247, i284, i247, env, static) :|: 0 <= i284

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

obtained
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(i1, i3, i6, env, static) -{0,0}> main_Load_3(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, i6, env, static) -{1,1}> main_Load_45(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i6, env, static) -{0,0}> main_Load_46(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i3, i6, env, static) -{0,0}> main_Load_49(i1, i3, i6, env, static) :|: 0 <= static
main_Load_49(i1, i3, i6, env, static) -{0,0}> main_Load_50(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i3, i6, env, static) -{0,0}> main_Load_51(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i3, i6, env, static) -{1,1}> main_LE_52(i1, i3, i6, env, static) :|: 0 >= 0
main_LE_52(i1, i3, i6, env, static) -{0,0}> main_LE_96(i1, i3, i6, i3, env, static) :|: 0 >= 0
main_LE_96(i38, i39, i6, i40, env, static) -{0,0}> main_LE_400(i38, i39, i6, i38, i40, env, static) :|: 0 >= 0

obtained
main_LE_400(i246, i39, i247, i265, i249, env, static) -{8,8}> main_GE_437(i246, i39, i247, i274', 42, i265, i249, env, static) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249 && 0 < 1
by chaining
main_LE_400(i246, i39, i247, i265, i249, env, static) -{0,0}> main_LE_405(i246, i39, i247, i265, i249, env, static) :|: 1 <= i265
main_LE_405(i246, i39, i247, i265, i249, env, static) -{1,1}> main_Load_409(i246, i39, i247, i265, i249, env, static) :|: 0 < i265 && 1 <= i265
main_Load_409(i246, i39, i247, i265, i249, env, static) -{1,1}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265
main_LE_414(i246, i39, i247, i271, i265, env, static) -{0,0}> main_LE_417(i246, i39, i247, i271, i265, env, static) :|: 1 <= i271 && 1 <= i265
main_LE_417(i246, i39, i247, i271, i265, env, static) -{1,1}> main_New_423(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && 0 < i271 && 1 <= i265
main_New_423(i246, i39, i247, i265, i271, env, static) -{1,1}> main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && o78 = 1 && 0 < o78 && 1 <= i265
main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) -{1,1}> main_GE_437(i246, i39, i247, i274, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 1 <= i265

obtained
main_GE_437(i246, i39, i247, i283, 42, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
by chaining
main_GE_437(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{0,0}> main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && 1 <= i265
main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_443(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && iconst_42 <= i283 && 1 <= i265
main_Inc_443(i246, i39, i247, i265, i271, env, static) -{1,1}> main_JMP_445(i246, i39, i247, i265, i285, env, static) :|: 1 <= i271 && i271 + -1 = i285 && 1 <= i265 && 0 <= i285
main_JMP_445(i246, i39, i247, i265, i285, env, static) -{1,1}> main_Load_457(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_Load_457(i246, i39, i247, i265, i285, env, static) -{1,1}> main_LE_462(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_LE_462(i246, i39, i247, i265, i285, env, static) -{0,0}> main_LE_400(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285

obtained
main_GE_437(i246, i39, i247, i282, 42, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265
by chaining
main_GE_437(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{0,0}> main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && 1 <= i265
main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_441(i246, i39, i247, i265, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && i282 < iconst_42 && 1 <= i265
main_Inc_441(i246, i39, i247, i265, env, static) -{1,1}> main_Load_444(i246, i39, i247, i284, env, static) :|: i265 + -1 = i284 && 0 <= i284 && 1 <= i265
main_Load_444(i246, i39, i247, i284, env, static) -{1,1}> main_Store_446(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_Store_446(i246, i39, i247, i284, env, static) -{1,1}> main_JMP_459(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_JMP_459(i246, i39, i247, i284, env, static) -{1,1}> main_Load_463(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_Load_463(i246, i39, i247, i284, env, static) -{1,1}> main_LE_467(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_LE_467(i246, i39, i247, i284, env, static) -{0,0}> main_LE_400(i246, i39, i247, i284, i247, env, static) :|: 0 <= i284

(8) Obligation:

IntTrs with 4 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i246, i39, i247, i265, i249, env, static) -{8,8}> main_GE_437(i246, i39, i247, i274', 42, i265, i249, env, static) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249 && 0 < 1
main_GE_437(i246, i39, i247, i283, 42, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
main_GE_437(i246, i39, i247, i282, 42, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

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

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

main_Load_2(x1, x2, x3, x4, x5) → main_Load_2(x1, x2, x3, x5)
main_LE_400(x1, x2, x3, x4, x5, x6, x7) → main_LE_400(x3, x4, x5)
main_GE_437(x1, x2, x3, x4, x5, x6, x7, x8, x9) → main_GE_437(x3, x4, x6, x7)

(10) Obligation:

IntTrs with 4 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, i6, static) -{16,16}> main_LE_400(i6, i1, i3) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i247, i265, i249) -{8,8}> main_GE_437(i247, i274', i265, i249) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249 && 0 < 1
main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i285') :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i284', i247) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

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

Moved arithmethic from constraints to rhss.

main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i285') :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
was transformed to
main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i271 + -1) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271

main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i284', i247) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265
was transformed to
main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i265 + -1, i247) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

(12) Obligation:

IntTrs with 4 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i271 + -1) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
main_Load_2(i1, i3, i6, static) -{16,16}> main_LE_400(i6, i1, i3) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i247, i265, i249) -{8,8}> main_GE_437(i247, i274', i265, i249) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249 && 0 < 1
main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i265 + -1, i247) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

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

Simplified expressions.

main_Load_2(i1, i3, i6, static) -{16,16}> main_LE_400(i6, i1, i3) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(i1, i3, i6, static) -{16,16}> main_LE_400(i6, i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_400(i247, i265, i249) -{8,8}> main_GE_437(i247, i274', i265, i249) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249 && 0 < 1
was transformed to
main_LE_400(i247, i265, i249) -{8,8}> main_GE_437(i247, i274', i265, i249) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249

main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i271 + -1) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
was transformed to
main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i271 - 1) :|: i271 - 1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271

main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i265 + -1, i247) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265
was transformed to
main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i265 - 1, i247) :|: 0 <= i284' && i282 < 42 && i265 - 1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

(14) Obligation:

IntTrs with 4 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_LE_400(i247, i265, i249) -{8,8}> main_GE_437(i247, i274', i265, i249) :|: 0 < i249 && 1 <= i265 && 0 < i265 && 1 <= i249
main_GE_437(i247, i282, i265, i271) -{6,6}> main_LE_400(i247, i265 - 1, i247) :|: 0 <= i284' && i282 < 42 && i265 - 1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265
main_GE_437(i247, i283, i265, i271) -{4,4}> main_LE_400(i247, i265, i271 - 1) :|: i271 - 1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
main_Load_2(i1, i3, i6, static) -{16,16}> main_LE_400(i6, i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(15) koat Proof (EQUIVALENT transformation)

YES(?, 24*ar_1 + 24*ar_0*ar_2 + 18*ar_0 + 28)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 6) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\ ar_1 < 42 /\ ar_2 - 1 = i284' /\ 1 <= ar_3 /\ ar_1 <= 41 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 4) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 8) main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 6) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\ ar_1 < 42 /\ ar_2 - 1 = i284' /\ 1 <= ar_3 /\ ar_1 <= 41 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 4) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_400) = V_2
Pol(main_GE_437) = V_3
Pol(main_Load_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\ ar_1 < 42 /\ ar_2 - 1 = i284' /\ 1 <= ar_3 /\ ar_1 <= 41 /\ 1 <= ar_2 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 8) main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
(Comp: ar_0, Cost: 6) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\ ar_1 < 42 /\ ar_2 - 1 = i284' /\ 1 <= ar_3 /\ ar_1 <= 41 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 4) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_400) = 2*V_3 + 1
Pol(main_GE_437) = 2*V_4
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-3) = ar_3
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_3 + 2 /\\ 0 <= ar_3 /\\ 0 <= static'1 ]", 0-0) = ar_2
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_3 + 2 /\\ 0 <= ar_3 /\\ 0 <= static'1 ]", 0-1) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_3 + 2 /\\ 0 <= ar_3 /\\ 0 <= static'1 ]", 0-2) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_3 + 2 /\\ 0 <= ar_3 /\\ 0 <= static'1 ]", 0-3) = ?
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\\ 1 <= ar_2 /\\ 0 <= i285' /\\ 42 <= ar_1 /\\ 1 <= ar_3 ]", 0-0) = ar_2
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\\ 1 <= ar_2 /\\ 0 <= i285' /\\ 42 <= ar_1 /\\ 1 <= ar_3 ]", 0-1) = ar_0
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\\ 1 <= ar_2 /\\ 0 <= i285' /\\ 42 <= ar_1 /\\ 1 <= ar_3 ]", 0-2) = ar_1 + ar_2
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\\ 1 <= ar_2 /\\ 0 <= i285' /\\ 42 <= ar_1 /\\ 1 <= ar_3 ]", 0-3) = ?
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\\ ar_1 < 42 /\\ ar_2 - 1 = i284' /\\ 1 <= ar_3 /\\ ar_1 <= 41 /\\ 1 <= ar_2 ]", 0-0) = ar_2
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\\ ar_1 < 42 /\\ ar_2 - 1 = i284' /\\ 1 <= ar_3 /\\ ar_1 <= 41 /\\ 1 <= ar_2 ]", 0-1) = ar_0
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\\ ar_1 < 42 /\\ ar_2 - 1 = i284' /\\ 1 <= ar_3 /\\ ar_1 <= 41 /\\ 1 <= ar_2 ]", 0-2) = ar_2
S("main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\\ ar_1 < 42 /\\ ar_2 - 1 = i284' /\\ 1 <= ar_3 /\\ ar_1 <= 41 /\\ 1 <= ar_2 ]", 0-3) = ?
S("main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_2 ]", 0-0) = ar_2
S("main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_2 ]", 0-1) = ?
S("main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_2 ]", 0-2) = ar_0
S("main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\\ 1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_2 ]", 0-3) = ar_1 + ar_2
orients the transitions
main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
weakly and the transitions
main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
strictly and produces the following problem:
4: T:
(Comp: 2*ar_1 + 2*ar_0*ar_2 + ar_0 + 1, Cost: 8) main_LE_400(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_437(ar_0, i274', ar_1, ar_2)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_2 ]
(Comp: ar_0, Cost: 6) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2 - 1, ar_0, arityPad)) [ 0 <= i284' /\ ar_1 < 42 /\ ar_2 - 1 = i284' /\ 1 <= ar_3 /\ ar_1 <= 41 /\ 1 <= ar_2 ]
(Comp: 2*ar_1 + 2*ar_0*ar_2 + ar_0 + 1, Cost: 4) main_GE_437(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_0, ar_2, ar_3 - 1, arityPad)) [ ar_3 - 1 = i285' /\ 1 <= ar_2 /\ 0 <= i285' /\ 42 <= ar_1 /\ 1 <= ar_3 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_400(ar_2, ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 24*ar_1 + 24*ar_0*ar_2 + 18*ar_0 + 28

Time: 0.314 sec (SMT: 0.286 sec)

(16) BOUNDS(CONSTANT, 28 + 18 * |#0| + 24 * |#0| * |#2| + 24 * |#1|)

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

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

(18) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(20) Obligation:

IntTrs with 52 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i3, i6, env, static) -{0,0}> main_Load_3(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i3, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i3, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i3, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i3, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i3, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, i6, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, i6, env, static) -{1,1}> main_Load_45(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i3, i6, env, static) -{0,0}> main_Load_46(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i3, i6, env, static) -{0,0}> main_Load_49(i1, i3, i6, env, static) :|: 0 <= static
main_Load_49(i1, i3, i6, env, static) -{0,0}> main_Load_50(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i3, i6, env, static) -{0,0}> main_Load_51(i1, i3, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i3, i6, env, static) -{1,1}> main_LE_52(i1, i3, i6, env, static) :|: 0 >= 0
main_LE_52(i1, i3, i6, env, static) -{0,0}> main_LE_96(i1, i3, i6, i3, env, static) :|: 0 >= 0
main_LE_96(i38, i39, i6, i40, env, static) -{0,0}> main_LE_400(i38, i39, i6, i38, i40, env, static) :|: 0 >= 0
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_LE_400(i246, i39, i247, i265, i249, env, static) -{0,0}> main_LE_405(i246, i39, i247, i265, i249, env, static) :|: 1 <= i265
main_LE_405(i246, i39, i247, i265, i249, env, static) -{1,1}> main_Load_409(i246, i39, i247, i265, i249, env, static) :|: 0 < i265 && 1 <= i265
main_Load_409(i246, i39, i247, i265, i249, env, static) -{1,1}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_LE_414(i246, i39, i247, i271, i265, env, static) -{0,0}> main_LE_417(i246, i39, i247, i271, i265, env, static) :|: 1 <= i271 && 1 <= i265
main_LE_417(i246, i39, i247, i271, i265, env, static) -{1,1}> main_New_423(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && 0 < i271 && 1 <= i265
main_New_423(i246, i39, i247, i265, i271, env, static) -{1,1}> main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && o78 = 1 && 0 < o78 && 1 <= i265
main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) -{1,1}> main_GE_437(i246, i39, i247, i274, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 1 <= i265
main_GE_437(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{0,0}> main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && 1 <= i265
main_GE_437(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{0,0}> main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && 1 <= i265
main_GE_439(i246, i39, i247, i282, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_441(i246, i39, i247, i265, env, static) :|: 1 <= i271 && i282 <= 41 && iconst_42 = 42 && i282 < iconst_42 && 1 <= i265
main_GE_440(i246, i39, i247, i283, iconst_42, i265, i271, env, static) -{1,1}> main_Inc_443(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 42 <= i283 && iconst_42 <= i283 && 1 <= i265
main_Inc_441(i246, i39, i247, i265, env, static) -{1,1}> main_Load_444(i246, i39, i247, i284, env, static) :|: i265 + -1 = i284 && 0 <= i284 && 1 <= i265
main_Inc_443(i246, i39, i247, i265, i271, env, static) -{1,1}> main_JMP_445(i246, i39, i247, i265, i285, env, static) :|: 1 <= i271 && i271 + -1 = i285 && 1 <= i265 && 0 <= i285
main_Load_444(i246, i39, i247, i284, env, static) -{1,1}> main_Store_446(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_JMP_445(i246, i39, i247, i265, i285, env, static) -{1,1}> main_Load_457(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_Store_446(i246, i39, i247, i284, env, static) -{1,1}> main_JMP_459(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_Load_457(i246, i39, i247, i265, i285, env, static) -{1,1}> main_LE_462(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_JMP_459(i246, i39, i247, i284, env, static) -{1,1}> main_Load_463(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_LE_462(i246, i39, i247, i265, i285, env, static) -{0,0}> main_LE_400(i246, i39, i247, i265, i285, env, static) :|: 1 <= i265 && 0 <= i285
main_Load_463(i246, i39, i247, i284, env, static) -{1,1}> main_LE_467(i246, i39, i247, i284, env, static) :|: 0 <= i284
main_LE_467(i246, i39, i247, i284, env, static) -{0,0}> main_LE_400(i246, i39, i247, i284, i247, env, static) :|: 0 <= i284

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

obtained
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
by chaining
main_LE_400(i246, i39, i247, i265, i249, env, static) -{0,0}> main_LE_405(i246, i39, i247, i265, i249, env, static) :|: 1 <= i265
main_LE_405(i246, i39, i247, i265, i249, env, static) -{1,1}> main_Load_409(i246, i39, i247, i265, i249, env, static) :|: 0 < i265 && 1 <= i265
main_Load_409(i246, i39, i247, i265, i249, env, static) -{1,1}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265

obtained
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
by chaining
main_LE_414(i246, i39, i247, i271, i265, env, static) -{0,0}> main_LE_417(i246, i39, i247, i271, i265, env, static) :|: 1 <= i271 && 1 <= i265
main_LE_417(i246, i39, i247, i271, i265, env, static) -{1,1}> main_New_423(i246, i39, i247, i265, i271, env, static) :|: 1 <= i271 && 0 < i271 && 1 <= i265
main_New_423(i246, i39, i247, i265, i271, env, static) -{1,1}> main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && o78 = 1 && 0 < o78 && 1 <= i265
main_Duplicate_425(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_426(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_InvokeMethod_427(i246, i39, i247, o78, i265, i271, env, static) -{1,1}> main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) :|: 1 <= i271 && 0 < o78 && 1 <= i265
main_ConstantStackPush_431(i246, i39, i247, i274, i265, i271, env, static) -{1,1}> main_GE_437(i246, i39, i247, i274, iconst_42, i265, i271, env, static) :|: 1 <= i271 && iconst_42 = 42 && 1 <= i265

(22) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
main_GE_437(i246, i39, i247, i283, 42, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
main_GE_437(i246, i39, i247, i282, 42, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265

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

Moved arithmethic from lhss to constraints.

main_GE_437(i246, i39, i247, i282, 42, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265
was transformed to
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42

main_GE_437(i246, i39, i247, i283, 42, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271
was transformed to
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

(24) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

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

Moved arithmethic from constraints to rhss.

main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i284', i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42
was transformed to
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 + -1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42

main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i285', env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42
was transformed to
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 + -1, env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

(26) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 + -1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 + -1, env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

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

Simplified expressions.

main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
was transformed to
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271

main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 + -1, env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42
was transformed to
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 - 1, env, static) :|: i271 - 1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 + -1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42
was transformed to
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 - 1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 - 1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42

(28) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 - 1, env, static) :|: i271 - 1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 - 1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 - 1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42

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

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

(30) Obligation:

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

(32) Obligation:

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

Moved arithmethic from lhss to constraints.

(34) Obligation:

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

Moved arithmethic from constraints to rhss.

(36) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 + -1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 + -1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271 && 0 < 1
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 + -1, env, static) :|: i271 + -1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42

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

Simplified expressions.

(38) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i3, i6, env, static) -{16,16}> main_LE_400(i1, i3, i6, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_400(i246, i39, i247, i264, i249, env, static) -{0,0}> main_LE_404(i246, i39, i247, i264, i249, env, static) :|: i264 <= 0
main_LE_414(i246, i39, i247, i271, i265, env, static) -{6,6}> main_GE_437(i246, i39, i247, i274', 42, i265, i271, env, static) :|: 0 < i271 && 1 <= i265 && 1 <= i271
main_LE_400(i246, i39, i247, i265, i249, env, static) -{2,2}> main_LE_414(i246, i39, i247, i249, i265, env, static) :|: 1 <= i265 && 0 < i265
main_LE_414(i246, i39, i247, i270, i265, env, static) -{0,0}> main_LE_416(i246, i39, i247, i270, i265, env, static) :|: i270 <= 0 && 1 <= i265
main_GE_437(i246, i39, i247, i283, x, i265, i271, env, static) -{4,4}> main_LE_400(i246, i39, i247, i265, i271 - 1, env, static) :|: i271 - 1 = i285' && 1 <= i265 && 0 <= i285' && 42 <= i283 && 1 <= i271 && x = 42
main_GE_437(i246, i39, i247, i282, x, i265, i271, env, static) -{6,6}> main_LE_400(i246, i39, i247, i265 - 1, i247, env, static) :|: 0 <= i284' && i282 < 42 && i265 - 1 = i284' && 1 <= i271 && i282 <= 41 && 1 <= i265 && x = 42