The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(22 + 7 * #0 + -7 * #1, 29)).

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

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 40 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, env, static) -{21,21}> main_JMP_115(i2, i3, i9', env, static'1) :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0

obtained
main_JMP_115(i2, i3, i26, env, static) -{7,7}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'
by chaining
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, env, static) -{21,21}> main_JMP_115(i2, i3, i9', env, static'1) :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2
main_JMP_115(i2, i3, i26, env, static) -{7,7}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'

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

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

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

(10) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i9') :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2
main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i46') :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'

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

Moved arithmethic from constraints to rhss.

main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i46') :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'
was transformed to
main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i26 + 1) :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'

main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i9') :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2
was transformed to
main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i3 + 1) :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2

(12) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i26 + 1) :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'
main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i3 + 1) :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2

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

Simplified expressions.

main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i26 + 1) :|: 0 >= 0 && i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'
was transformed to
main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i26 + 1) :|: i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'

main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i3 + 1) :|: 0 >= 0 && i3 + 1 = i6' && i6' <= i2 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9' && 0 <= 2
was transformed to
main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i3 + 1) :|: i3 + 1 = i6' && i6' <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9'

(14) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_JMP_115(i2, i3, i26) -{7,7}> main_JMP_115(i2, i3, i26 + 1) :|: i26 + 1 = i34' && i34' <= i2 && i26 + 1 = i46'
main_Load_1(i2, i3, static) -{21,21}> main_JMP_115(i2, i3, i3 + 1) :|: i3 + 1 = i6' && i6' <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i3 + 1 = i9'

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

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

(16) Obligation:

Set of 42 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

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

Transformed 42 jbc graph edges to a weighted ITS with 42 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 42 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6

obtained
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
by chaining
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0

obtained
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
by chaining
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34

obtained
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
by chaining
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

(20) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'

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

Moved arithmethic from constraints to rhss.

main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
was transformed to
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'

main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2

main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
was transformed to
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'

main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
was transformed to
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'

(22) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'

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

Simplified expressions.

main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: i3 + 1 = i6' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
was transformed to
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: i26 + 1 = i34'

main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
was transformed to
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: i34 <= i2 && i26 + 1 = i46'

main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
was transformed to
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: i6 <= i2 && i3 + 1 = i9'

(24) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: i34 <= i2 && i26 + 1 = i46'
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: i26 + 1 = i34'
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: i3 + 1 = i6' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: i6 <= i2 && i3 + 1 = i9'

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

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

(26) Obligation:

IntTrs with 42 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
by chaining
main_Load_1(i2, i3, env, static) -{0,0}> main_Load_4(i2, i3, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_46(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i2, i3, env, static) -{1,1}> main_Load_47(i2, i3, env, static) :|: 0 >= 0
main_Load_47(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_50(i2, i3, env, static) :|: 0 <= static
main_Load_50(i2, i3, env, static) -{0,0}> main_Load_51(i2, i3, env, static) :|: 0 >= 0
main_Load_51(i2, i3, env, static) -{0,0}> main_Load_52(i2, i3, env, static) :|: 0 >= 0
main_Load_52(i2, i3, env, static) -{1,1}> main_Load_53(i2, i3, env, static) :|: 0 >= 0
main_Load_53(i2, i3, env, static) -{1,1}> main_ConstantStackPush_54(i2, i3, env, static) :|: 0 >= 0
main_ConstantStackPush_54(i2, i3, env, static) -{1,1}> main_IntArithmetic_55(i2, i3, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_55(i2, i3, iconst_1, env, static) -{1,1}> main_LT_67(i2, i3, i6, env, static) :|: iconst_1 = 1 && i3 + iconst_1 = i6

obtained
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
by chaining
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_69(i2, i3, i6, env, static) :|: i6 <= i2
main_LT_69(i2, i3, i6, env, static) -{1,1}> main_Inc_71(i2, i3, env, static) :|: i6 <= i2
main_Inc_71(i2, i3, env, static) -{1,1}> main_JMP_73(i2, i3, i9, env, static) :|: i3 + 1 = i9
main_JMP_73(i2, i3, i9, env, static) -{0,0}> main_JMP_115(i2, i3, i9, env, static) :|: 0 >= 0

obtained
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
by chaining
main_JMP_115(i2, i3, i26, env, static) -{1,1}> main_Load_118(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_118(i2, i3, i26, env, static) -{1,1}> main_Load_119(i2, i3, i26, env, static) :|: 0 >= 0
main_Load_119(i2, i3, i26, env, static) -{1,1}> main_ConstantStackPush_120(i2, i3, i26, env, static) :|: 0 >= 0
main_ConstantStackPush_120(i2, i3, i26, env, static) -{1,1}> main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) :|: iconst_1 = 1
main_IntArithmetic_124(i2, i3, i26, iconst_1, env, static) -{1,1}> main_LT_133(i2, i3, i34, i26, env, static) :|: iconst_1 = 1 && i26 + iconst_1 = i34

obtained
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
by chaining
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_137(i2, i3, i34, i26, env, static) :|: i34 <= i2
main_LT_137(i2, i3, i34, i26, env, static) -{1,1}> main_Inc_148(i2, i3, i26, env, static) :|: i34 <= i2
main_Inc_148(i2, i3, i26, env, static) -{1,1}> main_JMP_150(i2, i3, i46, env, static) :|: i26 + 1 = i46
main_JMP_150(i2, i3, i46, env, static) -{0,0}> main_JMP_115(i2, i3, i46, env, static) :|: 0 >= 0

(28) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'

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

Moved arithmethic from constraints to rhss.

main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i46', env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
was transformed to
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'

main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i6', env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2

main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i34', i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
was transformed to
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'

main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i9', env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
was transformed to
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'

(30) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'

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

Simplified expressions.

main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: 0 < 2 && i3 + 1 = i6' && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: i3 + 1 = i6' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: 0 >= 0 && i26 + 1 = i34'
was transformed to
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: i26 + 1 = i34'

main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: 0 >= 0 && i34 <= i2 && i26 + 1 = i46'
was transformed to
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: i34 <= i2 && i26 + 1 = i46'

main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: 0 >= 0 && i6 <= i2 && i3 + 1 = i9'
was transformed to
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: i6 <= i2 && i3 + 1 = i9'

(32) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LT_133(i2, i3, i34, i26, env, static) -{2,2}> main_JMP_115(i2, i3, i26 + 1, env, static) :|: i34 <= i2 && i26 + 1 = i46'
main_LT_67(i2, i3, i6, env, static) -{0,0}> main_LT_68(i2, i3, i6, env, static) :|: i2 < i6
main_JMP_115(i2, i3, i26, env, static) -{5,5}> main_LT_133(i2, i3, i26 + 1, i26, env, static) :|: i26 + 1 = i34'
main_LT_133(i2, i3, i34, i26, env, static) -{0,0}> main_LT_136(i2, i3, i34, i26, env, static) :|: i2 < i34
main_Load_1(i2, i3, env, static) -{19,19}> main_LT_67(i2, i3, i3 + 1, env, static'1) :|: i3 + 1 = i6' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LT_67(i2, i3, i6, env, static) -{2,2}> main_JMP_115(i2, i3, i3 + 1, env, static) :|: i6 <= i2 && i3 + 1 = i9'

(33) CESProof (EQUIVALENT transformation)

proved upper bound max(19 + 7 * #0 + -7 * #1, 26) using cofloco

(34) BOUNDS(CONSTANT, max(19 + 7 * #0 + -7 * #1, 26))