The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 39 + 6 * |#0| + 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 PastaC11 {
    public static void main(int x, int y, int z) {
        while (true) {
			if (x >= 0) {
				x--;
				y = z;
			} else if (y >= 0) {
				y--;
			} else {
				break;
			}
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaC11.main(III)V: Graph of 64 nodes with 3 SCCs.

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

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

(4) Obligation:

Set of 60 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 60 jbc graph edges to a weighted ITS with 60 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 60 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

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

obtained
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0

obtained
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
by chaining
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138

obtained
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
by chaining
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171

obtained
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
by chaining
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1

obtained
main_Load_643(i138, i50, i219, -1, i220, env, static) -{6,6}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
by chaining
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

obtained
main_LT_404(i137, i50, i6, i51, env, static) -{6,6}> main_LT_404(i137, i50, i6, i146', env, static) :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
by chaining
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146

(8) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
main_Load_643(i138, i50, i219, -1, i220, env, static) -{6,6}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
main_LT_404(i137, i50, i6, i51, env, static) -{6,6}> main_LT_404(i137, i50, i6, i146', env, static) :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51

(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, x5) → main_Load_1(x1, x2, x3, x5)
main_LT_404(x1, x2, x3, x4, x5, x6) → main_LT_404(x1, x3, x4)
main_LT_454(x1, x2, x3, x4, x5, x6) → main_LT_454(x1, x3, x4)
main_Load_643(x1, x2, x3, x4, x5, x6, x7) → main_Load_643(x1, x5)

(10) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 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_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i143') :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i176') :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_454(i138, i6, -1) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i241') :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i146') :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51

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

Moved arithmethic from lhss to constraints.

main_LT_454(i138, i6, -1) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1
was transformed to
main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1

(12) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i176') :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i241') :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i146') :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i143') :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Moved arithmethic from constraints to rhss.

main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i176') :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i170 + -1) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i241') :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
was transformed to
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i220 + -1) :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'

main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i146') :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
was transformed to
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i51 + -1) :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51

main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i143') :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i138 + -1) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138

(14) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i170 + -1) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i220 + -1) :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i51 + -1) :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i138 + -1) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i138 + -1) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i138 - 1) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138

main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i170 + -1) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i170 - 1) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
was transformed to
main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: 0 <= i138 && x = -1

main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i51 + -1) :|: i51 + -1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
was transformed to
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i51 - 1) :|: i51 - 1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51

main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i220 + -1) :|: -1 < 0 && 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 + -1 = i241'
was transformed to
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i220 - 1) :|: 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 - 1 = i241'

(16) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_643(i138, i220) -{6,6}> main_Load_643(i138, i220 - 1) :|: 0 <= i220 && -1 <= i241' && 0 <= i138 && i220 - 1 = i241'
main_LT_454(i171, i6, i170) -{6,6}> main_LT_454(i171, i6, i170 - 1) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_454(i138, i6, x) -{1,1}> main_Load_643(i138, i6) :|: 0 <= i138 && x = -1
main_LT_404(i137, i6, i51) -{6,6}> main_LT_404(i137, i6, i51 - 1) :|: i51 - 1 = i146' && i137 <= -1 && -1 <= i146' && i137 < 0 && 0 <= i51
main_LT_404(i138, i6, i51) -{6,6}> main_LT_454(i138, i6, i138 - 1) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, static) -{16,16}> main_LT_404(i1, i6, i4) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(17) koat Proof (EQUIVALENT transformation)

YES(?, 6*ar_2 + 6*ar_0 + 6*ar_1 + 35)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ?, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: ?, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ?, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: ?, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_643) = 0
Pol(main_LT_454) = 1
Pol(main_LT_404) = 1
Pol(main_Load_1) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ?, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_643) = V_2 + 1
Pol(main_LT_454) = V_2 + 1
Pol(main_LT_404) = V_2 + 1
Pol(main_Load_1) = V_3 + 1
Pol(koat_start) = V_3 + 1
orients all transitions weakly and the transition
main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
strictly and produces the following problem:
4: T:
(Comp: ar_2 + 1, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ?, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_643) = 0
Pol(main_LT_454) = V_3 + 1
Pol(main_LT_404) = V_1
Pol(main_Load_1) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
strictly and produces the following problem:
5: T:
(Comp: ar_2 + 1, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ar_0, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ?, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LT_404) = V_3 + 1
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-3) = ar_3
S("main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ar_2
S("main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-2) = ar_1
S("main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-3) = ?
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\\ -1 <= i143' /\\ 0 <= ar_0 ]", 0-0) = ar_0
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\\ -1 <= i143' /\\ 0 <= ar_0 ]", 0-1) = ar_2
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\\ -1 <= i143' /\\ 0 <= ar_0 ]", 0-2) = ar_0 + 1
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\\ -1 <= i143' /\\ 0 <= ar_0 ]", 0-3) = ?
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\\ ar_0 <= -1 /\\ -1 <= i146' /\\ ar_0 < 0 /\\ 0 <= ar_2 ]", 0-0) = ar_0
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\\ ar_0 <= -1 /\\ -1 <= i146' /\\ ar_0 < 0 /\\ 0 <= ar_2 ]", 0-1) = ar_2
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\\ ar_0 <= -1 /\\ -1 <= i146' /\\ ar_0 < 0 /\\ 0 <= ar_2 ]", 0-2) = ar_1 + 1
S("main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\\ ar_0 <= -1 /\\ -1 <= i146' /\\ ar_0 < 0 /\\ 0 <= ar_2 ]", 0-3) = ?
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\\ ar_2 = -1 ]", 0-0) = ar_0
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\\ ar_2 = -1 ]", 0-1) = ar_2
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\\ ar_2 = -1 ]", 0-2) = ?
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\\ ar_2 = -1 ]", 0-3) = ?
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\\ 1 <= ar_0 /\\ 0 <= ar_0 /\\ -1 <= i176' /\\ -1 <= ar_2 /\\ 0 <= ar_2 ]", 0-0) = ar_0
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\\ 1 <= ar_0 /\\ 0 <= ar_0 /\\ -1 <= i176' /\\ -1 <= ar_2 /\\ 0 <= ar_2 ]", 0-1) = ar_2
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\\ 1 <= ar_0 /\\ 0 <= ar_0 /\\ -1 <= i176' /\\ -1 <= ar_2 /\\ 0 <= ar_2 ]", 0-2) = ar_0 + 2
S("main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\\ 1 <= ar_0 /\\ 0 <= ar_0 /\\ -1 <= i176' /\\ -1 <= ar_2 /\\ 0 <= ar_2 ]", 0-3) = ?
S("main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\\ -1 <= i241' /\\ 0 <= ar_0 /\\ ar_1 - 1 = i241' ]", 0-0) = ar_0
S("main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\\ -1 <= i241' /\\ 0 <= ar_0 /\\ ar_1 - 1 = i241' ]", 0-1) = ar_2 + 1
S("main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\\ -1 <= i241' /\\ 0 <= ar_0 /\\ ar_1 - 1 = i241' ]", 0-2) = ?
S("main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\\ -1 <= i241' /\\ 0 <= ar_0 /\\ ar_1 - 1 = i241' ]", 0-3) = ?
orients the transitions
main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
weakly and the transition
main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
strictly and produces the following problem:
6: T:
(Comp: ar_2 + 1, Cost: 6) main_Load_643(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1 - 1, arityPad, arityPad)) [ 0 <= ar_1 /\ -1 <= i241' /\ 0 <= ar_0 /\ ar_1 - 1 = i241' ]
(Comp: ar_0, Cost: 6) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i176' /\ 1 <= ar_0 /\ 0 <= ar_0 /\ -1 <= i176' /\ -1 <= ar_2 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 1) main_LT_454(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_643(ar_0, ar_1, arityPad, arityPad)) [ 0 <= ar_0 /\ ar_2 = -1 ]
(Comp: ar_1 + 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_2 - 1 = i146' /\ ar_0 <= -1 /\ -1 <= i146' /\ ar_0 < 0 /\ 0 <= ar_2 ]
(Comp: 1, Cost: 6) main_LT_404(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_454(ar_0, ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i143' /\ -1 <= i143' /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LT_404(ar_0, ar_2, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 6*ar_2 + 6*ar_0 + 6*ar_1 + 35

Time: 0.246 sec (SMT: 0.220 sec)

(18) BOUNDS(CONSTANT, 35 + 6 * |#0| + 6 * |#1| + 6 * |#2|)

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

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

(20) Obligation:

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

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

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

(22) Obligation:

IntTrs with 62 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(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

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

obtained
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0

obtained
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
by chaining
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138

obtained
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
by chaining
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171

obtained
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
by chaining
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1

obtained
main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
by chaining
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

obtained
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
by chaining
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1

obtained
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
by chaining
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146

(24) 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(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

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

Moved arithmethic from lhss to constraints.

main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1

main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
was transformed to
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1

(26) 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0

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

Moved arithmethic from constraints to rhss.

main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138

main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
was transformed to
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1

main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
was transformed to
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1

main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
was transformed to
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1

main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

(28) 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_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0

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

Simplified expressions.

main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
was transformed to
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: 0 <= i138 && x = -1

main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 - 1, env, static) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138

main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 - 1, env, static) :|: 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 - 1 = i241' && x = -1

main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
was transformed to
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 - 1, env, static) :|: i145 - 1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 - 1, env, static) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

(30) 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 - 1, env, static) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: 0 <= i138 && x = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 - 1, env, static) :|: i145 - 1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 - 1, env, static) :|: 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 - 1 = i241' && x = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 - 1, env, static) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

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

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

(32) Obligation:

IntTrs with 62 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(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

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

obtained
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_45(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_45(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{1,1}> main_LT_52(i1, i4, i6, env, static) :|: 0 >= 0
main_LT_52(i1, i4, i6, env, static) -{0,0}> main_LT_404(i1, i4, i6, i4, env, static) :|: 0 >= 0

obtained
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
by chaining
main_LT_404(i138, i50, i6, i51, env, static) -{0,0}> main_LT_411(i138, i50, i6, i51, env, static) :|: 0 <= i138
main_LT_411(i138, i50, i6, i51, env, static) -{1,1}> main_Inc_416(i138, i50, i6, env, static) :|: 0 <= i138
main_Inc_416(i138, i50, i6, env, static) -{1,1}> main_Load_421(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138 && i138 + -1 = i143
main_Load_421(i138, i50, i6, i143, env, static) -{1,1}> main_Store_426(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Store_426(i138, i50, i6, i143, env, static) -{1,1}> main_JMP_432(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_JMP_432(i138, i50, i6, i143, env, static) -{1,1}> main_Load_439(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138
main_Load_439(i138, i50, i6, i143, env, static) -{1,1}> main_LT_454(i138, i50, i6, i143, env, static) :|: -1 <= i143 && 0 <= i138

obtained
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
by chaining
main_LT_454(i171, i50, i6, i170, env, static) -{0,0}> main_LT_465(i171, i50, i6, i170, env, static) :|: 0 <= i171 && -1 <= i170 && 1 <= i171 && 0 <= i170
main_LT_465(i171, i50, i6, i170, env, static) -{1,1}> main_Inc_472(i171, i50, i6, i170, env, static) :|: 1 <= i171 && 0 <= i170
main_Inc_472(i171, i50, i6, i170, env, static) -{1,1}> main_Load_484(i171, i50, i6, i176, env, static) :|: -1 <= i176 && i170 + -1 = i176 && 1 <= i171 && 0 <= i170
main_Load_484(i171, i50, i6, i176, env, static) -{1,1}> main_Store_490(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Store_490(i171, i50, i6, i176, env, static) -{1,1}> main_JMP_500(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_JMP_500(i171, i50, i6, i176, env, static) -{1,1}> main_Load_510(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_Load_510(i171, i50, i6, i176, env, static) -{1,1}> main_LT_608(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 1 <= i171
main_LT_608(i171, i50, i6, i176, env, static) -{0,0}> main_LT_454(i171, i50, i6, i176, env, static) :|: -1 <= i176 && 0 <= i171 && 1 <= i171

obtained
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
by chaining
main_LT_454(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_LT_464(i138, i50, i6, iconst_NEG1, env, static) :|: -1 <= iconst_NEG1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_464(i138, i50, i6, iconst_NEG1, env, static) -{1,1}> main_Load_469(i138, i50, i6, iconst_NEG1, env, static) :|: iconst_NEG1 < 0 && 0 <= i138 && iconst_NEG1 = -1
main_Load_469(i138, i50, i6, iconst_NEG1, env, static) -{0,0}> main_Load_643(i138, i50, i6, iconst_NEG1, i6, env, static) :|: 0 <= i138 && iconst_NEG1 = -1

obtained
main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
by chaining
main_LT_651(i138, i50, i219, i235, iconst_NEG1, env, static) -{0,0}> main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_LT_655(i138, i50, i219, i235, iconst_NEG1, env, static) -{1,1}> main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) :|: 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235
main_Inc_662(i138, i50, i219, iconst_NEG1, i235, env, static) -{1,1}> main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1 && 0 <= i235 && i235 + -1 = i241
main_JMP_669(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_677(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_LT_683(i138, i50, i219, iconst_NEG1, i241, env, static) -{1,1}> main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) :|: iconst_NEG1 < 0 && -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1
main_Load_690(i138, i50, i219, iconst_NEG1, i241, env, static) -{0,0}> main_Load_643(i138, i50, i219, iconst_NEG1, i241, env, static) :|: -1 <= i241 && 0 <= i138 && iconst_NEG1 = -1

obtained
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
by chaining
main_LT_404(i137, i50, i6, i51, env, static) -{0,0}> main_LT_410(i137, i50, i6, i51, env, static) :|: i137 <= -1
main_LT_410(i137, i50, i6, i51, env, static) -{1,1}> main_Load_414(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_Load_414(i137, i50, i6, i51, env, static) -{1,1}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1

obtained
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
by chaining
main_LT_419(i137, i50, i6, i145, env, static) -{0,0}> main_LT_425(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_LT_425(i137, i50, i6, i145, env, static) -{1,1}> main_Inc_430(i137, i50, i6, i145, env, static) :|: i137 <= -1 && 0 <= i145
main_Inc_430(i137, i50, i6, i145, env, static) -{1,1}> main_JMP_436(i137, i50, i6, i146, env, static) :|: i145 + -1 = i146 && i137 <= -1 && -1 <= i146 && 0 <= i145
main_JMP_436(i137, i50, i6, i146, env, static) -{1,1}> main_Load_443(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_Load_443(i137, i50, i6, i146, env, static) -{1,1}> main_LT_461(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146
main_LT_461(i137, i50, i6, i146, env, static) -{0,0}> main_LT_404(i137, i50, i6, i146, env, static) :|: i137 <= -1 && -1 <= i146

(34) 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(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

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

Moved arithmethic from lhss to constraints.

main_LT_651(i138, i50, i219, i235, -1, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241'
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1

main_LT_454(i138, i50, i6, -1, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1
was transformed to
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1

(36) 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0

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

Moved arithmethic from constraints to rhss.

main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i143', env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138

main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, iconst_NEG1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
was transformed to
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1

main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i146', env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
was transformed to
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i241', env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1

main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, iconst_NEG1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
was transformed to
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1

main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i176', env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

(38) 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_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, 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_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0

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

Simplified expressions.

main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: -1 < 0 && 0 <= i138 && -1 <= -1 && x = -1
was transformed to
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: 0 <= i138 && x = -1

main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 + -1, env, static) :|: i138 + -1 = i143' && -1 <= i143' && 0 <= i138
was transformed to
main_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 - 1, env, static) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138

main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 + -1, env, static) :|: -1 < 0 && 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 + -1 = i241' && x = -1
was transformed to
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 - 1, env, static) :|: 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 - 1 = i241' && x = -1

main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 + -1, env, static) :|: i145 + -1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
was transformed to
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 - 1, env, static) :|: i145 - 1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145

main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 + -1, env, static) :|: i170 + -1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170
was transformed to
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 - 1, env, static) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170

(40) 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_LT_404(i138, i50, i6, i51, env, static) -{6,6}> main_LT_454(i138, i50, i6, i138 - 1, env, static) :|: i138 - 1 = i143' && -1 <= i143' && 0 <= i138
main_Load_1(i1, i4, i6, env, static) -{16,16}> main_LT_404(i1, i4, i6, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LT_454(i138, i50, i6, x, env, static) -{1,1}> main_Load_643(i138, i50, i6, -1, i6, env, static) :|: 0 <= i138 && x = -1
main_LT_419(i137, i50, i6, i145, env, static) -{4,4}> main_LT_404(i137, i50, i6, i145 - 1, env, static) :|: i145 - 1 = i146' && i137 <= -1 && -1 <= i146' && 0 <= i145
main_LT_419(i137, i50, i6, i144, env, static) -{0,0}> main_LT_423(i137, i50, i6, i144, env, static) :|: i144 <= -1 && i137 <= -1
main_Load_643(i138, i50, i219, iconst_NEG1, i220, env, static) -{1,1}> main_LT_651(i138, i50, i219, i220, -1, env, static) :|: 0 <= i138 && iconst_NEG1 = -1
main_LT_404(i137, i50, i6, i51, env, static) -{2,2}> main_LT_419(i137, i50, i6, i51, env, static) :|: i137 <= -1 && i137 < 0
main_LT_651(i138, i50, i219, i234, iconst_NEG1, env, static) -{0,0}> main_LT_654(i138, i50, i219, i234, -1, env, static) :|: i234 <= -1 && 0 <= i138 && iconst_NEG1 = -1
main_LT_651(i138, i50, i219, i235, x, env, static) -{5,5}> main_Load_643(i138, i50, i219, -1, i235 - 1, env, static) :|: 0 <= i235 && -1 <= i241' && 0 <= i138 && i235 - 1 = i241' && x = -1
main_LT_454(i171, i50, i6, i170, env, static) -{6,6}> main_LT_454(i171, i50, i6, i170 - 1, env, static) :|: i170 - 1 = i176' && 1 <= i171 && 0 <= i171 && -1 <= i176' && -1 <= i170 && 0 <= i170