time complexity proof of /tmp/tmpox4Jwr/PastaC7.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 27 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 (⇔, 32 ms)

    ↳16 BOUNDS(CONSTANT, 31 + 16 * |#1| + 16 * |#2|)

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

↳18 JBCComplexityEdges

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

    ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

        ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 31 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 PastaC7 {
    public static void main(int i, int j, int k) {
        while (i <= 100 && j <= k) {
            int t = i;
            i = j;
            j = i + 1;
            k--;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 61 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 61 jbc graph edges to a weighted ITS with 61 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 61 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_ConstantStackPush_51(i1, i4, i6, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, i6, env, static) -{1,1}> main_GT_54(i1, i4, i6, iconst_100, env, static) :|: iconst_100 = 100
main_GT_54(i13, i4, i6, iconst_100, env, static) -{0,0}> main_GT_55(i13, i4, i6, iconst_100, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_55(i13, i4, i6, iconst_100, env, static) -{1,1}> main_Load_58(i13, i4, i6, env, static) :|: i13 <= iconst_100 && i13 <= 100 && iconst_100 = 100
main_Load_58(i13, i4, i6, env, static) -{1,1}> main_Load_64(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_64(i13, i4, i6, env, static) -{1,1}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_79(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_GT_79(i13, i4, i6, env, static) -{1,1}> main_Load_87(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_Load_87(i13, i4, i6, env, static) -{1,1}> main_Store_89(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_89(i13, i4, i6, env, static) -{1,1}> main_Load_91(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_91(i13, i4, i6, env, static) -{1,1}> main_Store_93(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_93(i13, i4, i6, env, static) -{1,1}> main_Load_94(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_94(i13, i4, i6, env, static) -{1,1}> main_ConstantStackPush_95(i13, i4, i6, env, static) :|: i13 <= 100
main_ConstantStackPush_95(i13, i4, i6, env, static) -{1,1}> main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) -{1,1}> main_Store_97(i13, i4, i6, i21, env, static) :|: i4 + iconst_1 = i21 && i13 <= 100 && iconst_1 = 1
main_Store_97(i13, i4, i6, i21, env, static) -{1,1}> main_Inc_98(i13, i4, i6, i21, env, static) :|: i13 <= 100
main_Inc_98(i13, i4, i6, i21, env, static) -{1,1}> main_JMP_99(i13, i4, i6, i21, i22, env, static) :|: i6 + -1 = i22 && i13 <= 100
main_JMP_99(i13, i4, i6, i21, i22, env, static) -{1,1}> main_Load_100(i13, i4, i6, i21, i22, env, static) :|: i13 <= 100
main_Load_100(i13, i4, i6, i21, i22, env, static) -{0,0}> main_Load_390(i13, i4, i6, i4, i21, i22, env, static) :|: i13 <= 100
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_GT_397(i13, i217, i6, i218, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_397(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{0,0}> main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100
main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{1,1}> main_Load_424(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100 && i250 <= iconst_100
main_Load_424(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_433(i13, i217, i6, i219, i250, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_433(i13, i217, i6, i219, i250, i220, env, static) -{1,1}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_449(i13, i217, i6, i219, i220, i250, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_GT_449(i13, i217, i6, i219, i220, i250, env, static) -{1,1}> main_Load_452(i13, i217, i6, i250, i219, i220, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_Load_452(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Store_454(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Store_454(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_455(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_455(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Store_459(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Store_459(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Load_460(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Load_460(i13, i217, i6, i219, i220, env, static) -{1,1}> main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) -{1,1}> main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) -{1,1}> main_Store_469(i13, i217, i6, i308, i219, i220, env, static) :|: i219 + iconst_1 = i308 && i13 <= 100 && iconst_1 = 1
main_Store_469(i13, i217, i6, i308, i219, i220, env, static) -{1,1}> main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) :|: i13 <= 100
main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) -{1,1}> main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100 && i220 + -1 = i317
main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) -{1,1}> main_Load_486(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100
main_Load_486(i13, i217, i6, i219, i308, i317, env, static) -{0,0}> main_Load_390(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100

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

obtained
main_Load_2(i1, i4, i6, env, static) -{31,31}> main_Load_390(i1, i4, i6, i4, i21', i22', env, static'1) :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
by chaining
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_ConstantStackPush_51(i1, i4, i6, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, i6, env, static) -{1,1}> main_GT_54(i1, i4, i6, iconst_100, env, static) :|: iconst_100 = 100
main_GT_54(i13, i4, i6, iconst_100, env, static) -{0,0}> main_GT_55(i13, i4, i6, iconst_100, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_55(i13, i4, i6, iconst_100, env, static) -{1,1}> main_Load_58(i13, i4, i6, env, static) :|: i13 <= iconst_100 && i13 <= 100 && iconst_100 = 100
main_Load_58(i13, i4, i6, env, static) -{1,1}> main_Load_64(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_64(i13, i4, i6, env, static) -{1,1}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_79(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_GT_79(i13, i4, i6, env, static) -{1,1}> main_Load_87(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_Load_87(i13, i4, i6, env, static) -{1,1}> main_Store_89(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_89(i13, i4, i6, env, static) -{1,1}> main_Load_91(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_91(i13, i4, i6, env, static) -{1,1}> main_Store_93(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_93(i13, i4, i6, env, static) -{1,1}> main_Load_94(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_94(i13, i4, i6, env, static) -{1,1}> main_ConstantStackPush_95(i13, i4, i6, env, static) :|: i13 <= 100
main_ConstantStackPush_95(i13, i4, i6, env, static) -{1,1}> main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) -{1,1}> main_Store_97(i13, i4, i6, i21, env, static) :|: i4 + iconst_1 = i21 && i13 <= 100 && iconst_1 = 1
main_Store_97(i13, i4, i6, i21, env, static) -{1,1}> main_Inc_98(i13, i4, i6, i21, env, static) :|: i13 <= 100
main_Inc_98(i13, i4, i6, i21, env, static) -{1,1}> main_JMP_99(i13, i4, i6, i21, i22, env, static) :|: i6 + -1 = i22 && i13 <= 100
main_JMP_99(i13, i4, i6, i21, i22, env, static) -{1,1}> main_Load_100(i13, i4, i6, i21, i22, env, static) :|: i13 <= 100
main_Load_100(i13, i4, i6, i21, i22, env, static) -{0,0}> main_Load_390(i13, i4, i6, i4, i21, i22, env, static) :|: i13 <= 100

obtained
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{16,16}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'
by chaining
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_GT_397(i13, i217, i6, i218, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_397(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{0,0}> main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100
main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{1,1}> main_Load_424(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100 && i250 <= iconst_100
main_Load_424(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_433(i13, i217, i6, i219, i250, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_433(i13, i217, i6, i219, i250, i220, env, static) -{1,1}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_449(i13, i217, i6, i219, i220, i250, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_GT_449(i13, i217, i6, i219, i220, i250, env, static) -{1,1}> main_Load_452(i13, i217, i6, i250, i219, i220, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_Load_452(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Store_454(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Store_454(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_455(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_455(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Store_459(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Store_459(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Load_460(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Load_460(i13, i217, i6, i219, i220, env, static) -{1,1}> main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) -{1,1}> main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) -{1,1}> main_Store_469(i13, i217, i6, i308, i219, i220, env, static) :|: i219 + iconst_1 = i308 && i13 <= 100 && iconst_1 = 1
main_Store_469(i13, i217, i6, i308, i219, i220, env, static) -{1,1}> main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) :|: i13 <= 100
main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) -{1,1}> main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100 && i220 + -1 = i317
main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) -{1,1}> main_Load_486(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100
main_Load_486(i13, i217, i6, i219, i308, i317, env, static) -{0,0}> main_Load_390(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100

(8) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, env, static) -{31,31}> main_Load_390(i1, i4, i6, i4, i21', i22', env, static'1) :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{16,16}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'

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

(10) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i21', i22') :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i308', i317') :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'

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

Moved arithmethic from constraints to rhss.

main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i21', i22') :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
was transformed to
main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i4 + 1, i6 + -1) :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6

main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i308', i317') :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'
was transformed to
main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i219 + 1, i220 + -1) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'

(12) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i4 + 1, i6 + -1) :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i219 + 1, i220 + -1) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'

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

Simplified expressions.

main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i4 + 1, i6 + -1) :|: i1 <= 100 && i6 + -1 = i22' && 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 <= i6
was transformed to
main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i4 + 1, i6 - 1) :|: i1 <= 100 && i6 - 1 = i22' && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i6

main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i219 + 1, i220 + -1) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i218 <= 100 && i219 + 1 = i308'
was transformed to
main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i219 + 1, i220 - 1) :|: i13 <= 100 && i219 <= i220 && i220 - 1 = i317' && i218 <= 100 && i219 + 1 = i308'

(14) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, static) -{31,31}> main_Load_390(i1, i4, i4 + 1, i6 - 1) :|: i1 <= 100 && i6 - 1 = i22' && static'1 <= static''' + 1 && i4 + 1 = i21' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i6
main_Load_390(i13, i218, i219, i220) -{16,16}> main_Load_390(i13, i219, i219 + 1, i220 - 1) :|: i13 <= 100 && i219 <= i220 && i220 - 1 = i317' && i218 <= 100 && i219 + 1 = i308'

(15) koat Proof (EQUIVALENT transformation)

YES(?, 16*ar_1 + 16*ar_2 + 31)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 31) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_1, ar_1 + 1, ar_2 - 1)) [ ar_0 <= 100 /\ ar_2 - 1 = i22' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i21' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 <= ar_2 ]
(Comp: ?, Cost: 16) main_Load_390(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_2, ar_2 + 1, ar_3 - 1)) [ ar_0 <= 100 /\ ar_2 <= ar_3 /\ ar_3 - 1 = i317' /\ ar_1 <= 100 /\ ar_2 + 1 = i308' ]
(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: 1, Cost: 31) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_1, ar_1 + 1, ar_2 - 1)) [ ar_0 <= 100 /\ ar_2 - 1 = i22' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i21' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 <= ar_2 ]
(Comp: ?, Cost: 16) main_Load_390(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_2, ar_2 + 1, ar_3 - 1)) [ ar_0 <= 100 /\ ar_2 <= ar_3 /\ ar_3 - 1 = i317' /\ ar_1 <= 100 /\ ar_2 + 1 = i308' ]
(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_Load_2) = -V_2 + V_3
Pol(main_Load_390) = -V_3 + V_4 + 1
Pol(koat_start) = -V_2 + V_3
orients all transitions weakly and the transition
main_Load_390(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_2, ar_2 + 1, ar_3 - 1)) [ ar_0 <= 100 /\ ar_2 <= ar_3 /\ ar_3 - 1 = i317' /\ ar_1 <= 100 /\ ar_2 + 1 = i308' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 31) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_1, ar_1 + 1, ar_2 - 1)) [ ar_0 <= 100 /\ ar_2 - 1 = i22' /\ static'1 <= static''' + 1 /\ ar_1 + 1 = i21' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 <= ar_2 ]
(Comp: ar_1 + ar_2, Cost: 16) main_Load_390(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_390(ar_0, ar_2, ar_2 + 1, ar_3 - 1)) [ ar_0 <= 100 /\ ar_2 <= ar_3 /\ ar_3 - 1 = i317' /\ ar_1 <= 100 /\ ar_2 + 1 = i308' ]
(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 16*ar_1 + 16*ar_2 + 31

Time: 0.087 sec (SMT: 0.080 sec)

(16) BOUNDS(CONSTANT, 31 + 16 * |#1| + 16 * |#2|)

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

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

(18) Obligation:

Set of 65 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 65 jbc graph edges to a weighted ITS with 65 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 65 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, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_ConstantStackPush_51(i1, i4, i6, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, i6, env, static) -{1,1}> main_GT_54(i1, i4, i6, iconst_100, env, static) :|: iconst_100 = 100
main_GT_54(i13, i4, i6, iconst_100, env, static) -{0,0}> main_GT_55(i13, i4, i6, iconst_100, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, iconst_100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_GT_55(i13, i4, i6, iconst_100, env, static) -{1,1}> main_Load_58(i13, i4, i6, env, static) :|: i13 <= iconst_100 && i13 <= 100 && iconst_100 = 100
main_Load_58(i13, i4, i6, env, static) -{1,1}> main_Load_64(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_64(i13, i4, i6, env, static) -{1,1}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_79(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_GT_79(i13, i4, i6, env, static) -{1,1}> main_Load_87(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_Load_87(i13, i4, i6, env, static) -{1,1}> main_Store_89(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_89(i13, i4, i6, env, static) -{1,1}> main_Load_91(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_91(i13, i4, i6, env, static) -{1,1}> main_Store_93(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_93(i13, i4, i6, env, static) -{1,1}> main_Load_94(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_94(i13, i4, i6, env, static) -{1,1}> main_ConstantStackPush_95(i13, i4, i6, env, static) :|: i13 <= 100
main_ConstantStackPush_95(i13, i4, i6, env, static) -{1,1}> main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) -{1,1}> main_Store_97(i13, i4, i6, i21, env, static) :|: i4 + iconst_1 = i21 && i13 <= 100 && iconst_1 = 1
main_Store_97(i13, i4, i6, i21, env, static) -{1,1}> main_Inc_98(i13, i4, i6, i21, env, static) :|: i13 <= 100
main_Inc_98(i13, i4, i6, i21, env, static) -{1,1}> main_JMP_99(i13, i4, i6, i21, i22, env, static) :|: i6 + -1 = i22 && i13 <= 100
main_JMP_99(i13, i4, i6, i21, i22, env, static) -{1,1}> main_Load_100(i13, i4, i6, i21, i22, env, static) :|: i13 <= 100
main_Load_100(i13, i4, i6, i21, i22, env, static) -{0,0}> main_Load_390(i13, i4, i6, i4, i21, i22, env, static) :|: i13 <= 100
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_GT_397(i13, i217, i6, i218, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_397(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{0,0}> main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, iconst_100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{1,1}> main_Load_424(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100 && i250 <= iconst_100
main_Load_424(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_433(i13, i217, i6, i219, i250, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_433(i13, i217, i6, i219, i250, i220, env, static) -{1,1}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_449(i13, i217, i6, i219, i220, i250, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_GT_449(i13, i217, i6, i219, i220, i250, env, static) -{1,1}> main_Load_452(i13, i217, i6, i250, i219, i220, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_Load_452(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Store_454(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Store_454(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_455(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_455(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Store_459(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Store_459(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Load_460(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Load_460(i13, i217, i6, i219, i220, env, static) -{1,1}> main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) -{1,1}> main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) -{1,1}> main_Store_469(i13, i217, i6, i308, i219, i220, env, static) :|: i219 + iconst_1 = i308 && i13 <= 100 && iconst_1 = 1
main_Store_469(i13, i217, i6, i308, i219, i220, env, static) -{1,1}> main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) :|: i13 <= 100
main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) -{1,1}> main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100 && i220 + -1 = i317
main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) -{1,1}> main_Load_486(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100
main_Load_486(i13, i217, i6, i219, i308, i317, env, static) -{0,0}> main_Load_390(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100

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

obtained
main_Load_2(i1, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_ConstantStackPush_51(i1, i4, i6, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, i6, env, static) -{1,1}> main_GT_54(i1, i4, i6, iconst_100, env, static) :|: iconst_100 = 100

obtained
main_GT_54(i13, i4, i6, 100, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
by chaining
main_GT_54(i13, i4, i6, iconst_100, env, static) -{0,0}> main_GT_55(i13, i4, i6, iconst_100, env, static) :|: i13 <= 100 && iconst_100 = 100
main_GT_55(i13, i4, i6, iconst_100, env, static) -{1,1}> main_Load_58(i13, i4, i6, env, static) :|: i13 <= iconst_100 && i13 <= 100 && iconst_100 = 100
main_Load_58(i13, i4, i6, env, static) -{1,1}> main_Load_64(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_64(i13, i4, i6, env, static) -{1,1}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100

obtained
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i21', i22', env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
by chaining
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_79(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_GT_79(i13, i4, i6, env, static) -{1,1}> main_Load_87(i13, i4, i6, env, static) :|: i4 <= i6 && i13 <= 100
main_Load_87(i13, i4, i6, env, static) -{1,1}> main_Store_89(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_89(i13, i4, i6, env, static) -{1,1}> main_Load_91(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_91(i13, i4, i6, env, static) -{1,1}> main_Store_93(i13, i4, i6, env, static) :|: i13 <= 100
main_Store_93(i13, i4, i6, env, static) -{1,1}> main_Load_94(i13, i4, i6, env, static) :|: i13 <= 100
main_Load_94(i13, i4, i6, env, static) -{1,1}> main_ConstantStackPush_95(i13, i4, i6, env, static) :|: i13 <= 100
main_ConstantStackPush_95(i13, i4, i6, env, static) -{1,1}> main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_96(i13, i4, i6, iconst_1, env, static) -{1,1}> main_Store_97(i13, i4, i6, i21, env, static) :|: i4 + iconst_1 = i21 && i13 <= 100 && iconst_1 = 1
main_Store_97(i13, i4, i6, i21, env, static) -{1,1}> main_Inc_98(i13, i4, i6, i21, env, static) :|: i13 <= 100
main_Inc_98(i13, i4, i6, i21, env, static) -{1,1}> main_JMP_99(i13, i4, i6, i21, i22, env, static) :|: i6 + -1 = i22 && i13 <= 100
main_JMP_99(i13, i4, i6, i21, i22, env, static) -{1,1}> main_Load_100(i13, i4, i6, i21, i22, env, static) :|: i13 <= 100
main_Load_100(i13, i4, i6, i21, i22, env, static) -{0,0}> main_Load_390(i13, i4, i6, i4, i21, i22, env, static) :|: i13 <= 100

obtained
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
by chaining
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_391(i13, i217, i6, i218, i219, i220, env, static) -{1,1}> main_GT_397(i13, i217, i6, i218, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100

obtained
main_GT_397(i13, i217, i6, i250, 100, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
by chaining
main_GT_397(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{0,0}> main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100
main_GT_398(i13, i217, i6, i250, iconst_100, i219, i220, env, static) -{1,1}> main_Load_424(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && iconst_100 = 100 && i250 <= 100 && i250 <= iconst_100
main_Load_424(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_433(i13, i217, i6, i219, i250, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_433(i13, i217, i6, i219, i250, i220, env, static) -{1,1}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100

obtained
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
by chaining
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_449(i13, i217, i6, i219, i220, i250, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_GT_449(i13, i217, i6, i219, i220, i250, env, static) -{1,1}> main_Load_452(i13, i217, i6, i250, i219, i220, env, static) :|: i219 <= i220 && i13 <= 100 && i250 <= 100
main_Load_452(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Store_454(i13, i217, i6, i250, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Store_454(i13, i217, i6, i250, i219, i220, env, static) -{1,1}> main_Load_455(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100 && i250 <= 100
main_Load_455(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Store_459(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Store_459(i13, i217, i6, i219, i220, env, static) -{1,1}> main_Load_460(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_Load_460(i13, i217, i6, i219, i220, env, static) -{1,1}> main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) :|: i13 <= 100
main_ConstantStackPush_466(i13, i217, i6, i219, i220, env, static) -{1,1}> main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) :|: i13 <= 100 && iconst_1 = 1
main_IntArithmetic_468(i13, i217, i6, i219, iconst_1, i220, env, static) -{1,1}> main_Store_469(i13, i217, i6, i308, i219, i220, env, static) :|: i219 + iconst_1 = i308 && i13 <= 100 && iconst_1 = 1
main_Store_469(i13, i217, i6, i308, i219, i220, env, static) -{1,1}> main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) :|: i13 <= 100
main_Inc_470(i13, i217, i6, i219, i308, i220, env, static) -{1,1}> main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100 && i220 + -1 = i317
main_JMP_473(i13, i217, i6, i219, i308, i317, env, static) -{1,1}> main_Load_486(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100
main_Load_486(i13, i217, i6, i219, i308, i317, env, static) -{0,0}> main_Load_390(i13, i217, i6, i219, i308, i317, env, static) :|: i13 <= 100

(22) Obligation:

IntTrs with 10 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, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, iconst_100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_GT_54(i13, i4, i6, 100, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i21', i22', env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, iconst_100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_GT_397(i13, i217, i6, i250, 100, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'

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

Moved arithmethic from lhss to constraints.

main_GT_54(i13, i4, i6, 100, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100
was transformed to
main_GT_54(i13, i4, i6, x, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100 && x = 100

main_GT_397(i13, i217, i6, i250, 100, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100
was transformed to
main_GT_397(i13, i217, i6, i250, x, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && x = 100

(24) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, iconst_100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
main_GT_54(i13, i4, i6, x, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100 && x = 100
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, iconst_100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_GT_397(i13, i217, i6, i250, x, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && x = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i21', i22', env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_Load_2(i1, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1

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

Moved arithmethic from constraints to rhss.

main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, iconst_100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
was transformed to
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, 100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251

main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, iconst_100, env, static) :|: 101 <= i14 && iconst_100 = 100
was transformed to
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, 100, env, static) :|: 101 <= i14 && iconst_100 = 100

main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i308', i317', env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
was transformed to
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 + -1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'

main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i21', i22', env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
was transformed to
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 + -1, env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'

(26) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, 100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, 100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 + -1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 + -1, env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
main_GT_397(i13, i217, i6, i250, x, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && x = 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_54(i13, i4, i6, x, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100 && x = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_Load_2(i1, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1

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

Simplified expressions.

main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 + -1, env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
was transformed to
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 - 1, env, static) :|: i13 <= 100 && i6 - 1 = i22' && i4 <= i6 && i4 + 1 = i21'

main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 + -1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
was transformed to
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 - 1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 - 1 = i317' && i250 <= 100 && i219 + 1 = i308'

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

(28) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, 100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 - 1, env, static) :|: i13 <= 100 && i6 - 1 = i22' && i4 <= i6 && i4 + 1 = i21'
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, 100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_Load_2(i1, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_397(i13, i217, i6, i250, x, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && x = 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_54(i13, i4, i6, x, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100 && x = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 - 1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 - 1 = i317' && i250 <= 100 && i219 + 1 = i308'

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

Transformed 65 jbc graph edges to a weighted ITS with 65 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 10 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_397(i13, i217, i6, i251, iconst_100, i252, i220, env, static) -{0,0}> main_GT_399(i13, i217, i6, i251, 100, i252, i220, env, static) :|: i13 <= 100 && 102 <= i252 && iconst_100 = 100 && 101 <= i251
main_Load_390(i13, i217, i6, i218, i219, i220, env, static) -{2,2}> main_GT_397(i13, i217, i6, i218, 100, i219, i220, env, static) :|: i13 <= 100
main_GT_54(i14, i4, i6, iconst_100, env, static) -{0,0}> main_GT_56(i14, i4, i6, 100, env, static) :|: 101 <= i14 && iconst_100 = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{11,11}> main_Load_390(i13, i217, i6, i219, i219 + 1, i220 + -1, env, static) :|: i13 <= 100 && i219 <= i220 && i220 + -1 = i317' && i250 <= 100 && i219 + 1 = i308'
main_GT_69(i13, i4, i6, env, static) -{11,11}> main_Load_390(i13, i4, i6, i4, i4 + 1, i6 + -1, env, static) :|: i13 <= 100 && i6 + -1 = i22' && i4 <= i6 && i4 + 1 = i21'
main_GT_397(i13, i217, i6, i250, x, i219, i220, env, static) -{3,3}> main_GT_445(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && x = 100
main_GT_69(i13, i4, i6, env, static) -{0,0}> main_GT_78(i13, i4, i6, env, static) :|: i13 <= 100 && i6 < i4
main_GT_54(i13, i4, i6, x, env, static) -{3,3}> main_GT_69(i13, i4, i6, env, static) :|: i13 <= 100 && x = 100
main_GT_445(i13, i217, i6, i219, i220, i250, env, static) -{0,0}> main_GT_448(i13, i217, i6, i219, i220, i250, env, static) :|: i13 <= 100 && i250 <= 100 && i220 < i219
main_Load_2(i1, i4, i6, env, static) -{17,17}> main_GT_54(i1, i4, i6, 100, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1

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

Simplified expressions.

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

(15) koat Proof (EQUIVALENT transformation)

(16) BOUNDS(CONSTANT, 31 + 16 * |#1| + 16 * |#2|)

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation: