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

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 298 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(8)), 0 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 90 ms)
    ↳6 WeightedIntTrs
        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 30 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), 66 ms)
    ↳14 WeightedIntTrs
        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(8)), 0 ms)
↳22 JBCComplexityEdges
    ↳23 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 72 ms)
    ↳24 WeightedIntTrs
    ↳25 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 ms)
    ↳26 WeightedIntTrs
    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 28 ms)
    ↳28 WeightedIntTrs
    ↳29 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳30 WeightedIntTrs
    ↳31 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳32 WeightedIntTrs
    ↳33 koat Proof (⇔, 75 ms)
    ↳34 BOUNDS(CONSTANT, 23 + 7 * |#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 PastaB6 {
    public static void main(int x, int y) {
        while (x > 0 && y > 0) {
            x--;
            y--;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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


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

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

(4) Obligation:

Set of 47 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 47 jbc graph edges to a weighted ITS with 47 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 47 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

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

obtained
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0

obtained
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
by chaining
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12

obtained
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
by chaining
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12

obtained
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
by chaining
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20

obtained
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
by chaining
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62

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

Moved arithmethic from constraints to rhss.

main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
was transformed to
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62

main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
was transformed to
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12

main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
was transformed to
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'

main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
was transformed to
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20

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

Simplified expressions.

main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
was transformed to
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 - 1, i62 - 1, env, static) :|: 1 <= i63 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 - 1 = i68' && i43 - 1 = i66' && 1 <= i62

main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
was transformed to
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44

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

main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
was transformed to
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 - 1, i20 - 1, env, static) :|: i20 - 1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 - 1 = i22'

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 - 1, i62 - 1, env, static) :|: 1 <= i63 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 - 1 = i68' && i43 - 1 = i66' && 1 <= i62
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 - 1, i20 - 1, env, static) :|: i20 - 1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 - 1 = i22'
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12

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

Transformed 47 jbc graph edges to a weighted ITS with 47 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 47 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

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

obtained
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0

obtained
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
by chaining
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12

obtained
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
by chaining
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12

obtained
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
by chaining
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20

obtained
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
by chaining
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

(16) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62

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

Moved arithmethic from constraints to rhss.

main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i66', i68', env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
was transformed to
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62

main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, iconst_0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
was transformed to
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12

main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i22', i24', env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
was transformed to
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'

main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, iconst_0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
was transformed to
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20

(18) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20

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

Simplified expressions.

main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 + -1, i62 + -1, env, static) :|: 1 <= i63 && 0 <= i68' && 0 <= i62 && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 + -1 = i68' && i43 + -1 = i66' && 1 <= i62
was transformed to
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 - 1, i62 - 1, env, static) :|: 1 <= i63 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 - 1 = i68' && i43 - 1 = i66' && 1 <= i62

main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44 && 0 <= i43
was transformed to
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44

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

main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 + -1, i20 + -1, env, static) :|: i20 + -1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 + -1 = i22'
was transformed to
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 - 1, i20 - 1, env, static) :|: i20 - 1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 - 1 = i22'

(20) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_64(i12, i19, env, static) -{0,0}> main_LE_67(i12, i19, env, static) :|: i19 <= 0 && 1 <= i12
main_LE_116(i44, i63, i62, i43, env, static) -{5,5}> main_LE_92(i44, i63, i43 - 1, i62 - 1, env, static) :|: 1 <= i63 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i63 && 0 < i62 && 2 <= i44 && 0 <= i66' && i62 - 1 = i68' && i43 - 1 = i66' && 1 <= i62
main_Load_2(i2, i3, env, static) -{16,16}> main_LE_52(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_64(i12, i20, env, static) -{5,5}> main_LE_92(i12, i20, i12 - 1, i20 - 1, env, static) :|: i20 - 1 = i24' && 1 <= i12 && 0 <= i22' && 1 <= i20 && 0 < i20 && 0 <= i24' && i12 - 1 = i22'
main_LE_116(i44, i20, iconst_0, i43, env, static) -{0,0}> main_LE_119(i44, i20, 0, i43, env, static) :|: 0 <= iconst_0 && 2 <= i44 && iconst_0 = 0 && 1 <= i43 && 1 <= i20
main_LE_92(i44, i20, i43, i24, env, static) -{2,2}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 < i43 && 1 <= i20 && 0 <= i24 && 1 <= i43 && 1 <= i44 && 2 <= i44
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_64(i12, i3, env, static) :|: 1 <= i12 && 0 < i12
main_LE_92(i12, i20, iconst_0, i24, env, static) -{0,0}> main_LE_95(i12, i20, 0, i24, env, static) :|: 0 <= i24 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i20 && 1 <= i12

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

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

(22) Obligation:

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

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 43 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

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

obtained
main_Load_2(i2, i3, env, static) -{23,23}> main_LE_92(i2, i3, i22', i24', env, static'1) :|: 0 < 2 && 1 <= i2 && 0 <= static'1 && 1 <= i3 && i3 + -1 = i24' && 0 <= i24' && 0 <= i22' && 0 < i3 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1 && 0 < i2 && i2 + -1 = i22'
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{1,1}> main_LE_52(i2, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_58(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_58(i12, i3, env, static) -{1,1}> main_LE_64(i12, i3, env, static) :|: 1 <= i12
main_LE_64(i12, i20, env, static) -{0,0}> main_LE_68(i12, i20, env, static) :|: 1 <= i20 && 1 <= i12
main_LE_68(i12, i20, env, static) -{1,1}> main_Inc_71(i12, i20, env, static) :|: 0 < i20 && 1 <= i20 && 1 <= i12
main_Inc_71(i12, i20, env, static) -{1,1}> main_Inc_74(i12, i20, i22, env, static) :|: 0 <= i22 && 1 <= i20 && 1 <= i12 && i12 + -1 = i22
main_Inc_74(i12, i20, i22, env, static) -{1,1}> main_JMP_77(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && i20 + -1 = i24 && 1 <= i12
main_JMP_77(i12, i20, i22, i24, env, static) -{1,1}> main_Load_79(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12
main_Load_79(i12, i20, i22, i24, env, static) -{1,1}> main_LE_92(i12, i20, i22, i24, env, static) :|: 0 <= i24 && 0 <= i22 && 1 <= i20 && 1 <= i12

obtained
main_LE_92(i44, i20, i43, i24, env, static) -{7,7}> main_LE_92(i44, i20, i66', i68', env, static) :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24
by chaining
main_LE_92(i44, i20, i43, i24, env, static) -{0,0}> main_LE_96(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i44 && 1 <= i43 && 1 <= i20 && 0 <= i43
main_LE_96(i44, i20, i43, i24, env, static) -{1,1}> main_Load_104(i44, i20, i43, i24, env, static) :|: 0 <= i24 && 0 < i43 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_Load_104(i44, i20, i43, i24, env, static) -{1,1}> main_LE_116(i44, i20, i24, i43, env, static) :|: 0 <= i24 && 2 <= i44 && 1 <= i43 && 1 <= i20
main_LE_116(i44, i63, i62, i43, env, static) -{0,0}> main_LE_120(i44, i63, i62, i43, env, static) :|: 0 <= i62 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_LE_120(i44, i63, i62, i43, env, static) -{1,1}> main_Inc_130(i44, i63, i43, i62, env, static) :|: 2 <= i44 && 2 <= i63 && 0 < i62 && 1 <= i43 && 1 <= i62
main_Inc_130(i44, i63, i43, i62, env, static) -{1,1}> main_Inc_135(i44, i63, i66, i62, env, static) :|: 0 <= i66 && 2 <= i44 && i43 + -1 = i66 && 2 <= i63 && 1 <= i43 && 1 <= i62
main_Inc_135(i44, i63, i66, i62, env, static) -{1,1}> main_JMP_138(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68 && i62 + -1 = i68 && 1 <= i62
main_JMP_138(i44, i63, i66, i68, env, static) -{1,1}> main_Load_143(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_Load_143(i44, i63, i66, i68, env, static) -{1,1}> main_LE_457(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 2 <= i44 && 2 <= i63 && 0 <= i68
main_LE_457(i44, i63, i66, i68, env, static) -{0,0}> main_LE_92(i44, i63, i66, i68, env, static) :|: 0 <= i66 && 1 <= i63 && 2 <= i44 && 2 <= i63 && 1 <= i44 && 0 <= i68

(26) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, env, static) -{23,23}> main_LE_92(i2, i3, i22', i24', env, static'1) :|: 0 < 2 && 1 <= i2 && 0 <= static'1 && 1 <= i3 && i3 + -1 = i24' && 0 <= i24' && 0 <= i22' && 0 < i3 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1 && 0 < i2 && i2 + -1 = i22'
main_LE_92(i44, i20, i43, i24, env, static) -{7,7}> main_LE_92(i44, i20, i66', i68', env, static) :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_LE_92(x1, x2, x3, x4, x5, x6) → main_LE_92(x1, x2, x3, x4)

(28) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, static) -{23,23}> main_LE_92(i2, i3, i22', i24') :|: 0 < 2 && 1 <= i2 && 0 <= static'1 && 1 <= i3 && i3 + -1 = i24' && 0 <= i24' && 0 <= i22' && 0 < i3 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1 && 0 < i2 && i2 + -1 = i22'
main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i66', i68') :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24

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

Moved arithmethic from constraints to rhss.

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

main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i66', i68') :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24
was transformed to
main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i43 + -1, i24 + -1) :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24

(30) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, static) -{23,23}> main_LE_92(i2, i3, i2 + -1, i3 + -1) :|: 0 < 2 && 1 <= i2 && 0 <= static'1 && 1 <= i3 && i3 + -1 = i24' && 0 <= i24' && 0 <= i22' && 0 < i3 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1 && 0 < i2 && i2 + -1 = i22'
main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i43 + -1, i24 + -1) :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24

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

Simplified expressions.

main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i43 + -1, i24 + -1) :|: 0 <= i43 && 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 + -1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && 0 <= i24 && i24 + -1 = i68' && 0 < i43 && 1 <= i24
was transformed to
main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i43 - 1, i24 - 1) :|: 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 - 1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && i24 - 1 = i68' && 0 < i43 && 1 <= i24

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

(32) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, static) -{23,23}> main_LE_92(i2, i3, i2 - 1, i3 - 1) :|: 1 <= i2 && 0 <= static'1 && 1 <= i3 && i3 - 1 = i24' && 0 <= i24' && 0 <= i22' && 0 < i3 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 < i2 && i2 - 1 = i22'
main_LE_92(i44, i20, i43, i24) -{7,7}> main_LE_92(i44, i20, i43 - 1, i24 - 1) :|: 0 <= i68' && 1 <= i44 && 1 <= i43 && 2 <= i20 && i43 - 1 = i66' && 2 <= i44 && 0 < i24 && 0 <= i66' && 1 <= i20 && i24 - 1 = i68' && 0 < i43 && 1 <= i24

(33) koat Proof (EQUIVALENT transformation)

YES(?, 7*ar_1 + 23)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_0 - 1, ar_1 - 1)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i24' /\ 0 <= i24' /\ 0 <= i22' /\ 0 < ar_1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ 0 < ar_0 /\ ar_0 - 1 = i22' ]
(Comp: ?, Cost: 7) main_LE_92(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_2 - 1, ar_3 - 1)) [ 0 <= i68' /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 2 <= ar_1 /\ ar_2 - 1 = i66' /\ 2 <= ar_0 /\ 0 < ar_3 /\ 0 <= i66' /\ 1 <= ar_1 /\ ar_3 - 1 = i68' /\ 0 < ar_2 /\ 1 <= ar_3 ]
(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: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_0 - 1, ar_1 - 1)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i24' /\ 0 <= i24' /\ 0 <= i22' /\ 0 < ar_1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ 0 < ar_0 /\ ar_0 - 1 = i22' ]
(Comp: ?, Cost: 7) main_LE_92(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_2 - 1, ar_3 - 1)) [ 0 <= i68' /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 2 <= ar_1 /\ ar_2 - 1 = i66' /\ 2 <= ar_0 /\ 0 < ar_3 /\ 0 <= i66' /\ 1 <= ar_1 /\ ar_3 - 1 = i68' /\ 0 < ar_2 /\ 1 <= ar_3 ]
(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
Pol(main_LE_92) = V_4
Pol(koat_start) = V_2
orients all transitions weakly and the transition
main_LE_92(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_2 - 1, ar_3 - 1)) [ 0 <= i68' /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 2 <= ar_1 /\ ar_2 - 1 = i66' /\ 2 <= ar_0 /\ 0 < ar_3 /\ 0 <= i66' /\ 1 <= ar_1 /\ ar_3 - 1 = i68' /\ 0 < ar_2 /\ 1 <= ar_3 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 23) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_0 - 1, ar_1 - 1)) [ 1 <= ar_0 /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i24' /\ 0 <= i24' /\ 0 <= i22' /\ 0 < ar_1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ 0 < ar_0 /\ ar_0 - 1 = i22' ]
(Comp: ar_1, Cost: 7) main_LE_92(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_92(ar_0, ar_1, ar_2 - 1, ar_3 - 1)) [ 0 <= i68' /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 2 <= ar_1 /\ ar_2 - 1 = i66' /\ 2 <= ar_0 /\ 0 < ar_3 /\ 0 <= i66' /\ 1 <= ar_1 /\ ar_3 - 1 = i68' /\ 0 < ar_2 /\ 1 <= ar_3 ]
(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 7*ar_1 + 23

Time: 0.167 sec (SMT: 0.144 sec)

(34) BOUNDS(CONSTANT, 23 + 7 * |#1|)