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

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 379 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 0 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 87 ms)
    ↳6 WeightedIntTrs
        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 37 ms)
        ↳8 WeightedIntTrs
        ↳9 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳10 WeightedIntTrs
        ↳11 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳12 WeightedIntTrs
    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 57 ms)
    ↳14 WeightedIntTrs
        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 12 ms)
        ↳16 WeightedIntTrs
        ↳17 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳18 WeightedIntTrs
        ↳19 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳20 WeightedIntTrs
        ↳21 koat Proof (⇔, 113 ms)
        ↳22 BOUNDS(CONSTANT, 23 + 6 * |#0| + 6 * |#1|)
↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 0 ms)
↳24 JBCComplexityEdges
    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 91 ms)
    ↳26 WeightedIntTrs
    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 26 ms)
    ↳28 WeightedIntTrs
    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 20 ms)
    ↳30 WeightedIntTrs
    ↳31 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳32 WeightedIntTrs
    ↳33 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳34 WeightedIntTrs
    ↳35 koat Proof (⇔, 63 ms)
    ↳36 BOUNDS(CONSTANT, 20 + 6 * |#0| + 6 * |#1|)

(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 PastaA8 {
    public static void main(int x, int y) {
        while (x > y) {
            x++;
            y += 2;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaA8.main(II)V: Graph of 44 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 40 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 40 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0

obtained
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
by chaining
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0

obtained
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
by chaining
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0

obtained
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
by chaining
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

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

Moved arithmethic from constraints to rhss.

main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
was transformed to
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
was transformed to
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

(10) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

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

Simplified expressions.

main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
was transformed to
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
was transformed to
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

(12) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

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

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

(14) Obligation:

IntTrs with 40 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0

obtained
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
by chaining
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0

obtained
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
by chaining
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0

obtained
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
by chaining
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

(16) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

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

Moved arithmethic from constraints to rhss.

main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
was transformed to
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i7', i8', env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
was transformed to
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

(18) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

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

Simplified expressions.

main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: 0 >= 0 && i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
was transformed to
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1

main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: 0 >= 0 && i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
was transformed to
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25

(20) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_JMP_128(i1, i3, i25, i30, env, static) -{3,3}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_146(i1, i3, i25, i30, env, static) :|: i25 <= i30
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_58(i1, i3, env, static) :|: i1 <= i3
main_LE_55(i1, i3, env, static) -{3,3}> main_JMP_128(i1, i3, i1 + 1, i3 + 2, env, static) :|: i1 + 1 = i7' && i3 + 2 = i8' && i3 < i1
main_LE_145(i1, i3, i25, i30, env, static) -{3,3}> main_JMP_128(i1, i3, i25 + 1, i30 + 2, env, static) :|: i25 + 1 = i53' && i30 + 2 = i58' && i30 < i25
main_Load_1(i1, i3, env, static) -{17,17}> main_LE_55(i1, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(21) koat Proof (EQUIVALENT transformation)

YES(?, 6*ar_0 + 6*ar_1 + 23)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 >= 0 ]
(Comp: ?, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ ar_2 <= ar_3 ]
(Comp: ?, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3, arityPad, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2, ar_2, ar_3)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2, ar_4, ar_5)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: ?, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1, arityPad, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [ar_0, ar_1, ar_2, ar_3].
We thus obtain the following problem:
2: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: ?, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
(Comp: ?, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3)) [ 0 >= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: 1, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
(Comp: ?, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3)) [ 0 >= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 1
Pol(main_Load_1) = 1
Pol(main_LE_55) = 1
Pol(main_LE_145) = 1
Pol(main_JMP_128) = 1
Pol(main_LE_58) = 0
Pol(main_LE_146) = 0
orients all transitions weakly and the transition
main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: 1, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3)) [ ar_0 <= ar_1 ]
(Comp: 1, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
(Comp: ?, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3)) [ 0 >= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = V_1 - V_2
Pol(main_Load_1) = V_1 - V_2
Pol(main_LE_55) = V_1 - V_2 - 1
Pol(main_LE_145) = V_3 - V_4
Pol(main_JMP_128) = V_3 - V_4
Pol(main_LE_58) = V_1 - V_2 - 1
Pol(main_LE_146) = V_3 - V_4
orients all transitions weakly and the transition
main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_0 + ar_1, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: 1, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3)) [ ar_0 <= ar_1 ]
(Comp: 1, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
(Comp: ?, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3)) [ 0 >= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 1, Cost: 17) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_55(ar_0, ar_1, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_0 + ar_1, Cost: 3) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_2 + 1, ar_3 + 2)) [ ar_2 + 1 = i53' /\ ar_3 + 2 = i58' /\ ar_3 < ar_2 ]
(Comp: 1, Cost: 3) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_128(ar_0, ar_1, ar_0 + 1, ar_1 + 2)) [ ar_0 + 1 = i7' /\ ar_1 + 2 = i8' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 0) main_LE_55(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_58(ar_0, ar_1, ar_2, ar_3)) [ ar_0 <= ar_1 ]
(Comp: 1, Cost: 0) main_LE_145(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_146(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= ar_3 ]
(Comp: ar_0 + ar_1 + 1, Cost: 3) main_JMP_128(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_145(ar_0, ar_1, ar_2, ar_3)) [ 0 >= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 6*ar_0 + 6*ar_1 + 23

Time: 0.240 sec (SMT: 0.192 sec)

(22) BOUNDS(CONSTANT, 23 + 6 * |#0| + 6 * |#1|)

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

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

(24) Obligation:

Set of 38 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(26) Obligation:

IntTrs with 38 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i3, env, static) -{20,20}> main_JMP_128(i1, i3, i7', i8', env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_4(i1, i3, env, static) :|: 0 >= 0
main_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_30(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_31(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_32(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_32(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_33(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_33(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_34(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_34(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_36(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_37(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_38(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_40(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i3, env, static) -{1,1}> main_Load_46(i1, i3, env, static) :|: 0 >= 0
main_Load_46(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{0,0}> main_Load_48(i1, i3, env, static) :|: 0 <= static
main_Load_48(i1, i3, env, static) -{0,0}> main_Load_49(i1, i3, env, static) :|: 0 >= 0
main_Load_49(i1, i3, env, static) -{0,0}> main_Load_50(i1, i3, env, static) :|: 0 >= 0
main_Load_50(i1, i3, env, static) -{1,1}> main_Load_51(i1, i3, env, static) :|: 0 >= 0
main_Load_51(i1, i3, env, static) -{1,1}> main_LE_55(i1, i3, env, static) :|: 0 >= 0
main_LE_55(i1, i3, env, static) -{0,0}> main_LE_60(i1, i3, env, static) :|: i3 < i1
main_LE_60(i1, i3, env, static) -{1,1}> main_Inc_62(i1, i3, env, static) :|: i3 < i1
main_Inc_62(i1, i3, env, static) -{1,1}> main_Inc_64(i1, i3, i7, env, static) :|: i1 + 1 = i7
main_Inc_64(i1, i3, i7, env, static) -{1,1}> main_JMP_65(i1, i3, i7, i8, env, static) :|: i3 + 2 = i8
main_JMP_65(i1, i3, i7, i8, env, static) -{0,0}> main_JMP_128(i1, i3, i7, i8, env, static) :|: 0 >= 0

obtained
main_JMP_128(i1, i3, i25, i30, env, static) -{6,6}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'
by chaining
main_JMP_128(i1, i3, i25, i30, env, static) -{1,1}> main_Load_135(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_135(i1, i3, i25, i30, env, static) -{1,1}> main_Load_136(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_Load_136(i1, i3, i25, i30, env, static) -{1,1}> main_LE_145(i1, i3, i25, i30, env, static) :|: 0 >= 0
main_LE_145(i1, i3, i25, i30, env, static) -{0,0}> main_LE_147(i1, i3, i25, i30, env, static) :|: i30 < i25
main_LE_147(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_156(i1, i3, i25, i30, env, static) :|: i30 < i25
main_Inc_156(i1, i3, i25, i30, env, static) -{1,1}> main_Inc_168(i1, i3, i53, i30, env, static) :|: i25 + 1 = i53
main_Inc_168(i1, i3, i53, i30, env, static) -{1,1}> main_JMP_169(i1, i3, i53, i58, env, static) :|: i30 + 2 = i58
main_JMP_169(i1, i3, i53, i58, env, static) -{0,0}> main_JMP_128(i1, i3, i53, i58, env, static) :|: 0 >= 0

(28) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{20,20}> main_JMP_128(i1, i3, i7', i8', env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
main_JMP_128(i1, i3, i25, i30, env, static) -{6,6}> main_JMP_128(i1, i3, i53', i58', env, static) :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

(29) 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_1(x1, x2, x3, x4) → main_Load_1(x1, x2, x4)
main_JMP_128(x1, x2, x3, x4, x5, x6) → main_JMP_128(x3, x4)

(30) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i7', i8') :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i53', i58') :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

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

Moved arithmethic from constraints to rhss.

main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i7', i8') :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
was transformed to
main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i1 + 1, i3 + 2) :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2

main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i53', i58') :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'
was transformed to
main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i25 + 1, i30 + 2) :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

(32) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i1 + 1, i3 + 2) :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i25 + 1, i30 + 2) :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

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

Simplified expressions.

main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i25 + 1, i30 + 2) :|: 0 >= 0 && i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'
was transformed to
main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i25 + 1, i30 + 2) :|: i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i1 + 1, i3 + 2) :|: 0 >= 0 && static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8' && 0 < 2
was transformed to
main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i1 + 1, i3 + 2) :|: static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8'

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{20,20}> main_JMP_128(i1 + 1, i3 + 2) :|: static'1 <= static''' + 1 && i1 + 1 = i7' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i3 < i1 && i3 + 2 = i8'
main_JMP_128(i25, i30) -{6,6}> main_JMP_128(i25 + 1, i30 + 2) :|: i30 < i25 && i25 + 1 = i53' && i30 + 2 = i58'

(35) koat Proof (EQUIVALENT transformation)

YES(?, 6*ar_0 + 6*ar_1 + 20)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ static'1 <= static''' + 1 /\ ar_0 + 1 = i7' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_1 + 2 = i8' ]
(Comp: ?, Cost: 6) main_JMP_128(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ ar_1 < ar_0 /\ ar_0 + 1 = i53' /\ ar_1 + 2 = i58' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ static'1 <= static''' + 1 /\ ar_0 + 1 = i7' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_1 + 2 = i8' ]
(Comp: ?, Cost: 6) main_JMP_128(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ ar_1 < ar_0 /\ ar_0 + 1 = i53' /\ ar_1 + 2 = i58' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = V_1 - V_2
Pol(main_JMP_128) = V_1 - V_2
Pol(koat_start) = V_1 - V_2
orients all transitions weakly and the transition
main_JMP_128(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ ar_1 < ar_0 /\ ar_0 + 1 = i53' /\ ar_1 + 2 = i58' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ static'1 <= static''' + 1 /\ ar_0 + 1 = i7' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_1 + 2 = i8' ]
(Comp: ar_0 + ar_1, Cost: 6) main_JMP_128(ar_0, ar_1, ar_2) -> Com_1(main_JMP_128(ar_0 + 1, ar_1 + 2, arityPad)) [ ar_1 < ar_0 /\ ar_0 + 1 = i53' /\ ar_1 + 2 = i58' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 6*ar_0 + 6*ar_1 + 20

Time: 0.219 sec (SMT: 0.215 sec)

(36) BOUNDS(CONSTANT, 20 + 6 * |#0| + 6 * |#1|)