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


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

Constructed TerminationGraph.

(2) Obligation:

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


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

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

(4) Obligation:

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

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 52 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

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

obtained
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0

obtained
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
by chaining
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0

obtained
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
by chaining
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313

obtained
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
by chaining
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370

obtained
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
by chaining
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
by chaining
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

(8) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0

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

Moved arithmethic from lhss to constraints.

main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0

main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

(10) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Linearized lhss.

main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1

(12) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Removed div and mod.

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

(14) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Moved arithmethic from constraints to rhss.

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'

main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
was transformed to
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0

(16) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

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

Simplified expressions.

main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'

main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0

main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
was transformed to
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1

main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0

(18) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(19) koat Proof (EQUIVALENT transformation)

YES(?, 15*ar_1 + 30)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: ?, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: ?, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: ?, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 1
Pol(main_NE_613) = 0
Pol(main_LE_518) = 1
Pol(main_LE_521) = 0
Pol(main_LE_604) = 1
Pol(main_Load_602) = 1
Pol(main_NE_65) = 1
Pol(main_NE_66) = 0
Pol(main_Load_2) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: ?, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 1
Pol(main_LE_518) = 0
Pol(main_Load_602) = 2
Pol(main_LE_604) = 2
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-3) = ar_3
S("koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]", 0-4) = ar_4
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-1) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-2) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-3) = ar_2
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\\ 0 < ar_1 /\\ 1 <= ar_1 ]", 0-4) = ar_3 + 3
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-0) = ar_0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-1) = 0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-2) = ar_2
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-3) = ar_3 + 3
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\\ ar_2 = 0 ]", 0-4) = ?
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-1) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]", 0-4) = ?
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'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_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-2) = ar_2
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-3) = ar_3 + 3
S("main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_3 /\\ static''' <= ar_3 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-4) = ?
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-0) = ar_0
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-1) = ar_0
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-2) = ?
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-3) = ar_2
S("main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]", 0-4) = ar_3 + 3
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-0) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-2) = 0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-3) = ar_2
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]", 0-4) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-1) = ar_1
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]", 0-4) = ?
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-0) = ar_0
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-1) = ar_1
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-2) = ar_2
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-3) = ar_3 + 3
S("main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]", 0-4) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-0) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-2) = ar_0
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-3) = ar_2
S("main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\\ 1 <= ar_1 /\\ ar_1 - 1 = i370' /\\ 0 < ar_1 /\\ ar_2 - 1 = i356' ]", 0-4) = ar_3 + 3
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-1) = ar_0
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-2) = ar_2
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-3) = ar_3 + 3
S("main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]", 0-4) = ?
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-0) = ar_0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-1) = ?
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-2) = 0
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-3) = ar_2
S("main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]", 0-4) = ar_3 + 3
orients the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
weakly and the transitions
main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: 2, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: 2, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_611) = 0
Pol(main_NE_613) = 0
Pol(main_LE_518) = 3*V_2
Pol(main_LE_521) = 3*V_2
Pol(main_LE_604) = 2*V_2
Pol(main_Load_602) = 2*V_3 + 1
Pol(main_NE_65) = 3*V_2
Pol(main_NE_66) = 3*V_2
Pol(main_Load_2) = 3*V_2
Pol(koat_start) = 3*V_2
orients all transitions weakly and the transitions
main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_613(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_521(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 <= 0 ]
(Comp: 3*ar_1, Cost: 4) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_2 - 1, ar_1 - 1, ar_3, ar_4)) [ 0 <= i370' /\ 1 <= ar_1 /\ ar_1 - 1 = i370' /\ 0 < ar_1 /\ ar_2 - 1 = i356' ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_0 < ar_1 ]
(Comp: 1, Cost: 0) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_66(ar_0, ar_1, ar_2, ar_3, arityPad)) [ ar_1 < ar_0 ]
(Comp: 2, Cost: 3) main_LE_604(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_611(ar_0, ar_2, 0, ar_3, ar_4)) [ ar_1 = 0 ]
(Comp: 3*ar_1, Cost: 1) main_Load_602(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_604(ar_0, ar_2, ar_1, ar_3, ar_4)) [ 0 <= ar_2 ]
(Comp: 1, Cost: 17) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_NE_65(ar_0, ar_1, ar_2, static'1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 2) main_NE_65(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, ar_0, ar_2, ar_3, arityPad)) [ ar_1 = ar_0 ]
(Comp: 2, Cost: 2) main_NE_611(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_518(ar_0, 0, ar_3, ar_4, arityPad)) [ ar_1 = 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_602(ar_0, ar_1, ar_1, ar_2, ar_3)) [ -1 <= ar_1 /\ 0 < ar_1 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 15*ar_1 + 30

Time: 0.265 sec (SMT: 0.229 sec)

(20) BOUNDS(CONSTANT, 30 + 15 * |#1|)

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

Transformed 52 jbc graph edges to a weighted ITS with 52 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 52 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

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

obtained
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0

obtained
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
by chaining
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0

obtained
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
by chaining
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313

obtained
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
by chaining
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370

obtained
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
by chaining
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
by chaining
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

(24) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0

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

Moved arithmethic from lhss to constraints.

main_NE_611(i269, 0, 0, env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0

main_LE_604(i269, 0, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

(26) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Linearized lhss.

main_NE_65(i1, i1, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1

(28) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Removed div and mod.

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: !(i1 = i4)
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

(30) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0

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

Moved arithmethic from constraints to rhss.

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'

main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, iconst_0, env, static) :|: iconst_0 = 0
was transformed to
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0

(32) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4

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

Simplified expressions.

main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, 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_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: 0 >= 0 && x = i1
was transformed to
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1

main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 + -1, i349 + -1, env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'

main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: 0 >= 0 && x = 0 && x' = 0
was transformed to
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0

main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
was transformed to
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 > i4
was transformed to
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1

main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: 0 <= 0 && x = 0
was transformed to
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0

(34) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_611(i269, i371, iconst_0, env, static) -{0,0}> main_NE_613(i269, i371, 0, env, static) :|: iconst_0 = 0
main_LE_518(i269, i276, env, static) -{0,0}> main_LE_521(i269, i276, env, static) :|: i276 <= 0
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i343 - 1, i349 - 1, env, static) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i1 < i4
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_66(i1, i4, env, static) :|: i4 < i1
main_LE_604(i269, x, i343, env, static) -{3,3}> main_NE_611(i269, i343, 0, env, static) :|: x = 0
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_Load_2(i1, i4, env, static) -{17,17}> main_NE_65(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_NE_65(i1, x, env, static) -{2,2}> main_LE_518(i1, i1, env, static) :|: x = i1
main_NE_611(i269, x, x', env, static) -{2,2}> main_LE_518(i269, 0, env, static) :|: x = 0 && x' = 0
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(35) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

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

(36) Obligation:

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

Considered paths: all paths from start

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

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

(38) Obligation:

IntTrs with 49 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

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

obtained
main_Load_2(i1, i1, env, static) -{19,19}> main_LE_518(i1, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_35(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_35(i1, i4, env, static) -{1,1}> main_Load_40(i1, i4, env, static) :|: 0 >= 0
main_Load_40(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 <= static
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_49(i1, i4, env, static) :|: 0 >= 0
main_Load_49(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{1,1}> main_Load_51(i1, i4, env, static) :|: 0 >= 0
main_Load_51(i1, i4, env, static) -{1,1}> main_NE_65(i1, i4, env, static) :|: 0 >= 0
main_NE_65(i1, i4, env, static) -{0,0}> main_NE_67(i4, env, static) :|: i1 = i4
main_NE_67(i4, env, static) -{1,1}> main_Load_70(i4, env, static) :|: i4 = i4
main_Load_70(i4, env, static) -{1,1}> main_LE_72(i4, env, static) :|: 0 >= 0
main_LE_72(i4, env, static) -{0,0}> main_LE_518(i4, i4, env, static) :|: 0 >= 0

obtained
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
by chaining
main_LE_518(i269, i277, env, static) -{0,0}> main_LE_522(i269, i277, env, static) :|: 1 <= i277
main_LE_522(i269, i277, env, static) -{1,1}> main_Load_527(i269, i277, env, static) :|: 1 <= i277 && 0 < i277
main_Load_527(i269, i277, env, static) -{0,0}> main_Load_548(i269, i277, i277, env, static) :|: 1 <= i277 && 0 <= i277
main_Load_548(i269, i283, i284, env, static) -{0,0}> main_Load_584(i269, i283, i284, env, static) :|: 0 <= i284 && -1 <= i283 && 0 <= i283
main_Load_584(i269, i313, i314, env, static) -{0,0}> main_Load_602(i269, i313, i314, env, static) :|: 0 <= i314 && -1 <= i313

obtained
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
by chaining
main_LE_604(i269, i349, i343, env, static) -{0,0}> main_LE_606(i269, i349, i343, env, static) :|: 0 <= i349 && 1 <= i349
main_LE_606(i269, i349, i343, env, static) -{1,1}> main_Inc_608(i269, i343, i349, env, static) :|: 0 < i349 && 1 <= i349
main_Inc_608(i269, i343, i349, env, static) -{1,1}> main_Inc_610(i269, i356, i349, env, static) :|: i343 + -1 = i356 && 1 <= i349
main_Inc_610(i269, i356, i349, env, static) -{1,1}> main_JMP_612(i269, i356, i370, env, static) :|: 0 <= i370 && i349 + -1 = i370 && 1 <= i349
main_JMP_612(i269, i356, i370, env, static) -{1,1}> main_Load_615(i269, i356, i370, env, static) :|: 0 <= i370
main_Load_615(i269, i356, i370, env, static) -{0,0}> main_Load_602(i269, i356, i370, env, static) :|: 0 <= i370

obtained
main_LE_604(i269, 0, 0, env, static) -{5,5}> main_LE_518(i269, 0, env, static) :|: 0 <= 0
by chaining
main_LE_604(i269, iconst_0, i343, env, static) -{0,0}> main_LE_605(i269, iconst_0, i343, env, static) :|: 0 <= iconst_0 && iconst_0 = 0
main_LE_605(i269, iconst_0, i343, env, static) -{1,1}> main_Load_607(i269, i343, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0
main_Load_607(i269, i343, iconst_0, env, static) -{1,1}> main_Load_609(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_Load_609(i269, i343, iconst_0, env, static) -{1,1}> main_NE_611(i269, i343, iconst_0, env, static) :|: iconst_0 = 0
main_NE_611(i269, iconst_0, iconst_0, env, static) -{0,0}> main_NE_614(i269, iconst_0, env, static) :|: iconst_0 = 0
main_NE_614(i269, iconst_0, env, static) -{1,1}> main_Load_627(i269, iconst_0, env, static) :|: iconst_0 = 0
main_Load_627(i269, iconst_0, env, static) -{1,1}> main_LE_629(i269, iconst_0, env, static) :|: iconst_0 = 0
main_LE_629(i269, iconst_0, env, static) -{0,0}> main_LE_518(i269, iconst_0, env, static) :|: iconst_0 = 0

(40) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i1, env, static) -{19,19}> main_LE_518(i1, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i269, i277, env, static) -{1,1}> main_Load_602(i269, i277, i277, env, static) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i269, i343, i344, env, static) -{1,1}> main_LE_604(i269, i344, i343, env, static) :|: 0 <= i344
main_LE_604(i269, i349, i343, env, static) -{4,4}> main_Load_602(i269, i356', i370', env, static) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(i269, 0, 0, env, static) -{5,5}> main_LE_518(i269, 0, env, static) :|: 0 <= 0

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_LE_518(x1, x2, x3, x4) → main_LE_518(x2)
main_Load_602(x1, x2, x3, x4, x5) → main_Load_602(x2, x3)
main_LE_604(x1, x2, x3, x4, x5) → main_LE_604(x2, x3)

(42) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0

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

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

main_Load_2(x1, x2, x3) → main_Load_2(x2, x3)

(44) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0

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

Moved arithmethic from lhss to constraints.

main_LE_604(0, 0) -{5,5}> main_LE_518(0) :|: 0 <= 0
was transformed to
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0

(46) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277

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

Moved arithmethic from constraints to rhss.

main_LE_604(i349, i343) -{4,4}> main_Load_602(i356', i370') :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'

(48) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277

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

Simplified expressions.

main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: 0 <= 0 && x = 0 && x' = 0
was transformed to
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: x = 0 && x' = 0

main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 + -1, i349 + -1) :|: 0 <= i370' && 1 <= i349 && 0 <= i349 && i349 + -1 = i370' && 0 < i349 && i343 + -1 = i356'
was transformed to
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 - 1, i349 - 1) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'

main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 <= i277 && 0 < i277 && 1 <= i277
was transformed to
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(50) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{19,19}> main_LE_518(i1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_604(x, x') -{5,5}> main_LE_518(0) :|: x = 0 && x' = 0
main_LE_604(i349, i343) -{4,4}> main_Load_602(i343 - 1, i349 - 1) :|: 0 <= i370' && 1 <= i349 && i349 - 1 = i370' && 0 < i349 && i343 - 1 = i356'
main_Load_602(i343, i344) -{1,1}> main_LE_604(i344, i343) :|: 0 <= i344
main_LE_518(i277) -{1,1}> main_Load_602(i277, i277) :|: -1 <= i277 && 0 < i277 && 1 <= i277

(51) koat Proof (EQUIVALENT transformation)

YES(?, 15*ar_0 + 25)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: ?, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_602) = 1
Pol(main_LE_604) = 1
Pol(main_LE_518) = 0
and size complexities
S("koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]", 0-1) = ar_1
S("main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-1) = ar_0
S("main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]", 0-0) = ar_0
S("main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]", 0-1) = ?
S("main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\\ 1 <= ar_0 /\\ ar_0 - 1 = i370' /\\ 0 < ar_0 /\\ ar_1 - 1 = i356' ]", 0-0) = ?
S("main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\\ 1 <= ar_0 /\\ ar_0 - 1 = i370' /\\ 0 < ar_0 /\\ ar_1 - 1 = i356' ]", 0-1) = ar_0
S("main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\\ ar_1 = 0 ]", 0-0) = 0
S("main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\\ ar_1 = 0 ]", 0-1) = ?
S("main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\\ 0 <= ar_1 /\\ static''' <= ar_1 + 2 /\\ 0 <= static''' /\\ static'1 <= static''' + 1 ]", 0-1) = ?
orients the transitions
main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
weakly and the transition
main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: ?, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_2) = 3*V_1
Pol(main_LE_518) = 3*V_1
Pol(main_LE_604) = 2*V_1
Pol(main_Load_602) = 2*V_2 + 1
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 19) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_518(ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 5) main_LE_604(ar_0, ar_1) -> Com_1(main_LE_518(0, arityPad)) [ ar_0 = 0 /\ ar_1 = 0 ]
(Comp: 3*ar_0, Cost: 4) main_LE_604(ar_0, ar_1) -> Com_1(main_Load_602(ar_1 - 1, ar_0 - 1)) [ 0 <= i370' /\ 1 <= ar_0 /\ ar_0 - 1 = i370' /\ 0 < ar_0 /\ ar_1 - 1 = i356' ]
(Comp: 3*ar_0, Cost: 1) main_Load_602(ar_0, ar_1) -> Com_1(main_LE_604(ar_1, ar_0)) [ 0 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_518(ar_0, ar_1) -> Com_1(main_Load_602(ar_0, ar_0)) [ -1 <= ar_0 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 15*ar_0 + 25

Time: 0.098 sec (SMT: 0.089 sec)

(52) BOUNDS(CONSTANT, 25 + 15 * |#1|)