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

(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 PastaB15 {
    public static void main(int x, int y, int z) {
        while (x == y && x > z) {
            while (y > z) {
                x--;
                y--;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 54 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 54 jbc graph edges to a weighted ITS with 54 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 54 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_236(i3, i5, i50, i36, env, static) :|: i50 <= i5
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_236(i3, i5, i50, i36, env, static) -{1,1}> main_Load_239(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Load_239(i3, i5, i36, i50, env, static) -{1,1}> main_Load_251(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Load_251(i3, i5, i36, i50, env, static) -{1,1}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0

obtained
main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
by chaining
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0

obtained
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
by chaining
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0

obtained
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
by chaining
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0

obtained
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
by chaining
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

obtained
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
by chaining
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_236(i3, i5, i50, i36, env, static) :|: i50 <= i5
main_LE_236(i3, i5, i50, i36, env, static) -{1,1}> main_Load_239(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_Load_239(i3, i5, i36, i50, env, static) -{1,1}> main_Load_251(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_251(i3, i5, i36, i50, env, static) -{1,1}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50

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

Linearized lhss.

main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
was transformed to
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2

(10) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

(11) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
was transformed to
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50

main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
was transformed to
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3

(12) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50

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

Moved arithmethic from constraints to rhss.

main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
was transformed to
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50

(14) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

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

Simplified expressions.

main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
was transformed to
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: x = i2

main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 - 1, i50 - 1, env, static) :|: i36 - 1 = i77' && i50 - 1 = i91' && i5 < i50

main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
was transformed to
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i3 < i2

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: i50 <= i5

main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
was transformed to
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i50 < i36

main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
was transformed to
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 - 1, i3 - 1, env, static) :|: i5 < i3 && i3 - 1 = i10' && i3 - 1 = i11'

(16) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i3 < i2
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 - 1, i50 - 1, env, static) :|: i36 - 1 = i77' && i50 - 1 = i91' && i5 < i50
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: x = i2
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i50 < i36
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 - 1, i3 - 1, env, static) :|: i5 < i3 && i3 - 1 = i10' && i3 - 1 = i11'
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

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

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

(18) Obligation:

IntTrs with 54 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_236(i3, i5, i50, i36, env, static) :|: i50 <= i5
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_236(i3, i5, i50, i36, env, static) -{1,1}> main_Load_239(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Load_239(i3, i5, i36, i50, env, static) -{1,1}> main_Load_251(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Load_251(i3, i5, i36, i50, env, static) -{1,1}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0

obtained
main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
by chaining
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0

obtained
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
by chaining
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0

obtained
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
by chaining
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0

obtained
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
by chaining
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

obtained
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
by chaining
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_236(i3, i5, i50, i36, env, static) :|: i50 <= i5
main_LE_236(i3, i5, i50, i36, env, static) -{1,1}> main_Load_239(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_Load_239(i3, i5, i36, i50, env, static) -{1,1}> main_Load_251(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_251(i3, i5, i36, i50, env, static) -{1,1}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0

(20) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50

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

Linearized lhss.

main_NE_55(i2, i2, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0
was transformed to
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2

(22) Obligation:

IntTrs with 10 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

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

Removed div and mod.

main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: !(i36 = i50)
was transformed to
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50

main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: !(i2 = i3)
was transformed to
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3

(24) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50

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

Moved arithmethic from constraints to rhss.

main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i10', i11', env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
was transformed to
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50

(26) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

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

Simplified expressions.

main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: 0 >= 0 && x = i2
was transformed to
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: x = i2

main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, 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(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 + -1, i50 + -1, env, static) :|: 0 >= 0 && i36 + -1 = i77' && i50 + -1 = i91' && i5 < i50
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 - 1, i50 - 1, env, static) :|: i36 - 1 = i77' && i50 - 1 = i91' && i5 < i50

main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 > i3
was transformed to
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i3 < i2

main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: 0 >= 0 && i50 <= i5
was transformed to
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: i50 <= i5

main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 > i50
was transformed to
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i50 < i36

main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 + -1, i3 + -1, env, static) :|: 0 >= 0 && i5 < i3 && i3 + -1 = i10' && i3 + -1 = i11'
was transformed to
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 - 1, i3 - 1, env, static) :|: i5 < i3 && i3 - 1 = i10' && i3 - 1 = i11'

(28) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i2 < i3
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_60(i2, i3, i5, env, static) :|: i3 < i2
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_JMP_194(i3, i5, i36 - 1, i50 - 1, env, static) :|: i36 - 1 = i77' && i50 - 1 = i91' && i5 < i50
main_NE_55(i2, x, i5, env, static) -{3,3}> main_LE_69(i2, i5, env, static) :|: x = i2
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i36 < i50
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_307(i3, i5, i36, i50, env, static) :|: i50 < i36
main_LE_69(i3, i5, env, static) -{6,6}> main_JMP_194(i3, i5, i3 - 1, i3 - 1, env, static) :|: i5 < i3 && i3 - 1 = i10' && i3 - 1 = i11'
main_NE_279(i3, i5, i36, i50, env, static) -{0,0}> main_NE_308(i3, i5, i50, env, static) :|: i36 = i50
main_LE_229(i3, i5, i50, i36, env, static) -{3,3}> main_NE_279(i3, i5, i36, i50, env, static) :|: i50 <= i5
main_JMP_194(i3, i5, i36, i50, env, static) -{3,3}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_1(i2, i3, i5, env, static) -{17,17}> main_NE_55(i2, i3, i5, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_74(i3, i5, env, static) :|: i3 <= i5

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(13)) transformation)

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

(30) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 46 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i2, i5, env, static) -{26,26}> main_JMP_194(i2, i5, i10', i11', env, static'1) :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
by chaining
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_4(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_4(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, i5, env, static) -{1,1}> main_Load_41(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_41(i2, i3, i5, env, static) -{0,0}> main_Load_42(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_42(i2, i3, i5, env, static) -{0,0}> main_Load_44(i2, i3, i5, env, static) :|: 0 <= static
main_Load_44(i2, i3, i5, env, static) -{0,0}> main_Load_45(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_45(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{1,1}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{1,1}> main_NE_55(i2, i3, i5, env, static) :|: 0 >= 0
main_NE_55(i2, i3, i5, env, static) -{0,0}> main_NE_61(i3, i5, env, static) :|: i2 = i3
main_NE_61(i3, i5, env, static) -{1,1}> main_Load_63(i3, i5, env, static) :|: i3 = i3
main_Load_63(i3, i5, env, static) -{1,1}> main_Load_65(i3, i5, env, static) :|: 0 >= 0
main_Load_65(i3, i5, env, static) -{1,1}> main_LE_69(i3, i5, env, static) :|: 0 >= 0
main_LE_69(i3, i5, env, static) -{0,0}> main_LE_75(i3, i5, env, static) :|: i5 < i3
main_LE_75(i3, i5, env, static) -{1,1}> main_Load_79(i3, i5, env, static) :|: i5 < i3
main_Load_79(i3, i5, env, static) -{1,1}> main_Load_81(i3, i5, env, static) :|: 0 >= 0
main_Load_81(i3, i5, env, static) -{1,1}> main_LE_87(i3, i5, env, static) :|: 0 >= 0
main_LE_87(i3, i5, env, static) -{0,0}> main_LE_88(i3, i5, env, static) :|: i5 < i3
main_LE_88(i3, i5, env, static) -{1,1}> main_Inc_89(i3, i5, env, static) :|: i5 < i3
main_Inc_89(i3, i5, env, static) -{1,1}> main_Inc_90(i3, i5, i10, env, static) :|: i3 + -1 = i10
main_Inc_90(i3, i5, i10, env, static) -{1,1}> main_JMP_91(i3, i5, i10, i11, env, static) :|: i3 + -1 = i11
main_JMP_91(i3, i5, i10, i11, env, static) -{0,0}> main_JMP_194(i3, i5, i10, i11, env, static) :|: 0 >= 0

obtained
main_JMP_194(i3, i5, i36, i50, env, static) -{6,6}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'
by chaining
main_JMP_194(i3, i5, i36, i50, env, static) -{1,1}> main_Load_204(i3, i5, i36, i50, env, static) :|: 0 >= 0
main_Load_204(i3, i5, i36, i50, env, static) -{1,1}> main_Load_214(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_Load_214(i3, i5, i50, i36, env, static) -{1,1}> main_LE_229(i3, i5, i50, i36, env, static) :|: 0 >= 0
main_LE_229(i3, i5, i50, i36, env, static) -{0,0}> main_LE_237(i3, i5, i50, i36, env, static) :|: i5 < i50
main_LE_237(i3, i5, i50, i36, env, static) -{1,1}> main_Inc_250(i3, i5, i36, i50, env, static) :|: i5 < i50
main_Inc_250(i3, i5, i36, i50, env, static) -{1,1}> main_Inc_269(i3, i5, i77, i50, env, static) :|: i36 + -1 = i77
main_Inc_269(i3, i5, i77, i50, env, static) -{1,1}> main_JMP_305(i3, i5, i77, i91, env, static) :|: i50 + -1 = i91
main_JMP_305(i3, i5, i77, i91, env, static) -{0,0}> main_JMP_194(i3, i5, i77, i91, env, static) :|: 0 >= 0

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i2, i5, env, static) -{26,26}> main_JMP_194(i2, i5, i10', i11', env, static'1) :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
main_JMP_194(i3, i5, i36, i50, env, static) -{6,6}> main_JMP_194(i3, i5, i77', i91', env, static) :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'

(35) 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, x5) → main_Load_1(x1, x2, x3, x5)
main_JMP_194(x1, x2, x3, x4, x5, x6) → main_JMP_194(x2, x3, x4)

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i2, i5, static) -{26,26}> main_JMP_194(i5, i10', i11') :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i77', i91') :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'

(37) WeightedIntTrsDuplicateArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they are duplicates. We removed arguments according to the following replacements:

main_Load_1(x1, x2, x3, x4) → main_Load_1(x2, x3, x4)

(38) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i10', i11') :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i77', i91') :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'

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

Moved arithmethic from constraints to rhss.

main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i10', i11') :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
was transformed to
main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i2 + -1, i2 + -1) :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2

main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i77', i91') :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'
was transformed to
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i36 + -1, i50 + -1) :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'

(40) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i2 + -1, i2 + -1) :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i36 + -1, i50 + -1) :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'

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

Simplified expressions.

main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i2 + -1, i2 + -1) :|: 0 >= 0 && 0 <= 2 && i2 + -1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 + -1 = i11' && 0 < 2
was transformed to
main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i2 - 1, i2 - 1) :|: i2 - 1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 - 1 = i11'

main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i36 + -1, i50 + -1) :|: 0 >= 0 && i5 < i50 && i36 + -1 = i77' && i50 + -1 = i91'
was transformed to
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i36 - 1, i50 - 1) :|: i5 < i50 && i36 - 1 = i77' && i50 - 1 = i91'

(42) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#1, #2, static)
Considered paths: all paths from start
Rules:
main_JMP_194(i5, i36, i50) -{6,6}> main_JMP_194(i5, i36 - 1, i50 - 1) :|: i5 < i50 && i36 - 1 = i77' && i50 - 1 = i91'
main_Load_1(i2, i5, static) -{26,26}> main_JMP_194(i5, i2 - 1, i2 - 1) :|: i2 - 1 = i10' && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i5 < i2 && i2 - 1 = i11'

(43) koat Proof (EQUIVALENT transformation)

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

Initial complexity problem:
1: T:
(Comp: ?, Cost: 6) main_JMP_194(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_0, ar_1 - 1, ar_2 - 1)) [ ar_0 < ar_2 /\ ar_1 - 1 = i77' /\ ar_2 - 1 = i91' ]
(Comp: ?, Cost: 26) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_1, ar_0 - 1, ar_0 - 1)) [ ar_0 - 1 = i10' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_0 - 1 = i11' ]
(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: ?, Cost: 6) main_JMP_194(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_0, ar_1 - 1, ar_2 - 1)) [ ar_0 < ar_2 /\ ar_1 - 1 = i77' /\ ar_2 - 1 = i91' ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_1, ar_0 - 1, ar_0 - 1)) [ ar_0 - 1 = i10' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_0 - 1 = i11' ]
(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_JMP_194) = -V_1 + V_3
Pol(main_Load_1) = V_1 - V_2
Pol(koat_start) = V_1 - V_2
orients all transitions weakly and the transition
main_JMP_194(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_0, ar_1 - 1, ar_2 - 1)) [ ar_0 < ar_2 /\ ar_1 - 1 = i77' /\ ar_2 - 1 = i91' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + ar_1, Cost: 6) main_JMP_194(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_0, ar_1 - 1, ar_2 - 1)) [ ar_0 < ar_2 /\ ar_1 - 1 = i77' /\ ar_2 - 1 = i91' ]
(Comp: 1, Cost: 26) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_JMP_194(ar_1, ar_0 - 1, ar_0 - 1)) [ ar_0 - 1 = i10' /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 /\ ar_0 - 1 = i11' ]
(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 + 26

Time: 0.105 sec (SMT: 0.100 sec)

(44) BOUNDS(CONSTANT, 26 + 6 * |#1| + 6 * |#2|)