time complexity proof of /tmp/tmpMBWafU/PastaB16.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 27 + 24 * |#0| + 18 * |#1|).

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 342 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 17 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 101 ms)

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 31 ms)

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

        ↳11 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳12 WeightedIntTrs

        ↳13 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 3 ms)

        ↳14 WeightedIntTrs

        ↳15 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 87 ms)

    ↳18 WeightedIntTrs

        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 35 ms)

        ↳20 WeightedIntTrs

        ↳21 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳22 WeightedIntTrs

        ↳23 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳24 WeightedIntTrs

        ↳25 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳26 WeightedIntTrs

        ↳27 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 9 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 85 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 32 ms)

    ↳36 WeightedIntTrs

    ↳37 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳38 WeightedIntTrs

    ↳39 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳40 WeightedIntTrs

    ↳41 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳42 WeightedIntTrs

    ↳43 koat Proof (⇔, 183 ms)

    ↳44 BOUNDS(CONSTANT, 21 + 24 * |#0| + 18 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaB16 {
    public static void main(int x, int y) {
        while (x > 0) {
            while (y > 0) {
                y--;
            }
            x--;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaB16.main(II)V: Graph of 62 nodes with 2 SCCs.

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

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

(4) Obligation:

Set of 58 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 58 jbc graph edges to a weighted ITS with 58 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 58 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_43(i1, i3, env, static) :|: 0 <= static
main_Load_43(i1, i3, env, static) -{0,0}> main_Load_45(i1, i3, env, static) :|: 0 >= 0
main_Load_45(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_56(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_56(i12, i3, env, static) -{1,1}> main_LE_58(i12, i3, env, static) :|: 1 <= i12
main_LE_58(i12, i3, env, static) -{0,0}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12
main_LE_629(i184, i199, i186, env, static) -{0,0}> main_LE_634(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_629(i184, i200, i186, env, static) -{0,0}> main_LE_635(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184
main_LE_634(i184, i199, i186, env, static) -{1,1}> main_Inc_639(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_635(i184, i200, i186, env, static) -{1,1}> main_Inc_641(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184 && 0 < i200
main_Inc_639(i184, i199, i186, env, static) -{1,1}> main_JMP_643(i184, i199, i203, env, static) :|: 1 <= i186 && i186 + -1 = i203 && i199 <= 0 && 0 <= i203 && 1 <= i184
main_Inc_641(i184, i200, i186, env, static) -{1,1}> main_JMP_645(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184 && i200 + -1 = i204
main_JMP_643(i184, i199, i203, env, static) -{1,1}> main_Load_647(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_JMP_645(i184, i200, i186, i204, env, static) -{1,1}> main_Load_650(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_Load_647(i184, i199, i203, env, static) -{1,1}> main_LE_658(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{0,0}> main_LE_669(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184 && 0 <= i227
main_LE_665(i184, i200, iconst_0, i186, env, static) -{0,0}> main_LE_671(i184, i200, iconst_0, i186, env, static) :|: 1 <= i186 && 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_665(i184, i229, i228, i186, env, static) -{0,0}> main_LE_672(i184, i229, i228, i186, env, static) :|: 1 <= i186 && 1 <= i229 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i228
main_LE_669(i184, i199, i227, env, static) -{1,1}> main_Load_678(i184, i199, i227, env, static) :|: 0 < i227 && i199 <= 0 && 1 <= i227 && 1 <= i184
main_LE_671(i184, i200, iconst_0, i186, env, static) -{1,1}> main_Inc_682(i184, i200, i186, iconst_0, env, static) :|: 1 <= i186 && iconst_0 <= 0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_672(i184, i229, i228, i186, env, static) -{1,1}> main_Inc_684(i184, i229, i186, i228, env, static) :|: 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 < i228
main_Load_678(i184, i199, i227, env, static) -{1,1}> main_LE_686(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_Inc_682(i184, i200, i186, iconst_0, env, static) -{1,1}> main_JMP_687(i184, i200, i234, iconst_0, env, static) :|: 1 <= i186 && i186 + -1 = i234 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Inc_684(i184, i229, i186, i228, env, static) -{1,1}> main_JMP_688(i184, i229, i186, i235, env, static) :|: i228 + -1 = i235 && 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_LE_686(i184, i199, i227, env, static) -{0,0}> main_LE_629(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_JMP_687(i184, i200, i234, iconst_0, env, static) -{1,1}> main_Load_689(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_JMP_688(i184, i229, i186, i235, env, static) -{1,1}> main_Load_704(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_Load_689(i184, i200, i234, iconst_0, env, static) -{1,1}> main_LE_713(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Load_704(i184, i229, i186, i235, env, static) -{0,0}> main_Load_650(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 1 <= i229 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_LE_713(i184, i200, iconst_0, iconst_0, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_713(i184, i200, i256, iconst_0, env, static) -{0,0}> main_LE_716(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256 && 0 <= i256
main_LE_716(i184, i200, i256, iconst_0, env, static) -{1,1}> main_Load_732(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 < i256 && 1 <= i256
main_Load_732(i184, i200, i256, iconst_0, env, static) -{0,0}> main_Load_650(i184, i200, i256, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256

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

obtained
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_43(i1, i3, env, static) :|: 0 <= static
main_Load_43(i1, i3, env, static) -{0,0}> main_Load_45(i1, i3, env, static) :|: 0 >= 0
main_Load_45(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0

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

obtained
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
by chaining
main_LE_629(i184, i200, i186, env, static) -{0,0}> main_LE_635(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184
main_LE_635(i184, i200, i186, env, static) -{1,1}> main_Inc_641(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184 && 0 < i200
main_Inc_641(i184, i200, i186, env, static) -{1,1}> main_JMP_645(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184 && i200 + -1 = i204
main_JMP_645(i184, i200, i186, i204, env, static) -{1,1}> main_Load_650(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184

obtained
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
by chaining
main_LE_665(i184, i229, i228, i186, env, static) -{0,0}> main_LE_672(i184, i229, i228, i186, env, static) :|: 1 <= i186 && 1 <= i229 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i228
main_LE_672(i184, i229, i228, i186, env, static) -{1,1}> main_Inc_684(i184, i229, i186, i228, env, static) :|: 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 < i228
main_Inc_684(i184, i229, i186, i228, env, static) -{1,1}> main_JMP_688(i184, i229, i186, i235, env, static) :|: i228 + -1 = i235 && 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_JMP_688(i184, i229, i186, i235, env, static) -{1,1}> main_Load_704(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_Load_704(i184, i229, i186, i235, env, static) -{0,0}> main_Load_650(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 1 <= i229 && 2 <= i229 && 1 <= i184 && 0 <= i235

obtained
main_LE_665(i184, i200, 0, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234'
by chaining
main_LE_665(i184, i200, iconst_0, i186, env, static) -{0,0}> main_LE_671(i184, i200, iconst_0, i186, env, static) :|: 1 <= i186 && 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_671(i184, i200, iconst_0, i186, env, static) -{1,1}> main_Inc_682(i184, i200, i186, iconst_0, env, static) :|: 1 <= i186 && iconst_0 <= 0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_Inc_682(i184, i200, i186, iconst_0, env, static) -{1,1}> main_JMP_687(i184, i200, i234, iconst_0, env, static) :|: 1 <= i186 && i186 + -1 = i234 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_JMP_687(i184, i200, i234, iconst_0, env, static) -{1,1}> main_Load_689(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Load_689(i184, i200, i234, iconst_0, env, static) -{1,1}> main_LE_713(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234

obtained
main_LE_713(i184, i200, i256, 0, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0
by chaining
main_LE_713(i184, i200, i256, iconst_0, env, static) -{0,0}> main_LE_716(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256 && 0 <= i256
main_LE_716(i184, i200, i256, iconst_0, env, static) -{1,1}> main_Load_732(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 < i256 && 1 <= i256
main_Load_732(i184, i200, i256, iconst_0, env, static) -{0,0}> main_Load_650(i184, i200, i256, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256

obtained
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
by chaining
main_LE_629(i184, i199, i186, env, static) -{0,0}> main_LE_634(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_634(i184, i199, i186, env, static) -{1,1}> main_Inc_639(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_Inc_639(i184, i199, i186, env, static) -{1,1}> main_JMP_643(i184, i199, i203, env, static) :|: 1 <= i186 && i186 + -1 = i203 && i199 <= 0 && 0 <= i203 && 1 <= i184
main_JMP_643(i184, i199, i203, env, static) -{1,1}> main_Load_647(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_Load_647(i184, i199, i203, env, static) -{1,1}> main_LE_658(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184

obtained
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
by chaining
main_LE_658(i184, i199, i227, env, static) -{0,0}> main_LE_669(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184 && 0 <= i227
main_LE_669(i184, i199, i227, env, static) -{1,1}> main_Load_678(i184, i199, i227, env, static) :|: 0 < i227 && i199 <= 0 && 1 <= i227 && 1 <= i184
main_Load_678(i184, i199, i227, env, static) -{1,1}> main_LE_686(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_LE_686(i184, i199, i227, env, static) -{0,0}> main_LE_629(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184

(8) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, 0, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234'
main_LE_713(i184, i200, iconst_0, iconst_0, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_713(i184, i200, i256, 0, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227

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

Moved arithmethic from lhss to constraints.

main_LE_665(i184, i200, 0, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234'
was transformed to
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0

main_LE_713(i184, i200, i256, 0, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0
was transformed to
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0

(10) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_LE_713(i184, i200, iconst_0, iconst_0, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0

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

Linearized lhss.

main_LE_713(i184, i200, iconst_0, iconst_0, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
was transformed to
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0

(12) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184

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

Moved arithmethic from constraints to rhss.

main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
was transformed to
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228

main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
was transformed to
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 + -1, 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0

main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
was transformed to
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'

main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
was transformed to
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 + -1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'

main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
was transformed to
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, 0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184

main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0
was transformed to
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, 0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0

(14) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 + -1, 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 + -1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, 0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, 0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0

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

Simplified expressions.

main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
was transformed to
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 - 1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 - 1 = i204'

main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
was transformed to
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227

main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 + -1, 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
was transformed to
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 - 1, 0, env, static) :|: 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 - 1 = i234' && x = 0

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

main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 + -1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
was transformed to
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 - 1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 - 1 = i203'

main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
was transformed to
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 - 1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 - 1 = i235' && 0 < i228

main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0
was transformed to
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && x = 0

(16) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, 0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && x = 0
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, 0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 - 1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 - 1 = i203'
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 - 1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 - 1 = i235' && 0 < i228
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 - 1, 0, env, static) :|: 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 - 1 = i234' && x = 0
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 - 1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 - 1 = i204'

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

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

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Linearized lhss.

(24) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i234', 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, iconst_0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 12 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1, env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186, env, static) -{4,4}> main_LE_713(i184, i200, i186 + -1, 0, env, static) :|: 0 <= 0 && 0 <= i234' && 1 <= i186 && 1 <= i184 && 1 <= i200 && i186 + -1 = i234' && x = 0
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1, env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_LE_52(i12, i3, env, static) -{2,2}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12 && 0 < i12
main_LE_658(i184, i199, i227, env, static) -{2,2}> main_LE_629(i184, i199, i227, env, static) :|: 0 <= i227 && 1 <= i184 && 1 <= i227 && i199 <= 0 && 0 < i227
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_629(i184, i199, i186, env, static) -{4,4}> main_LE_658(i184, i199, i186 + -1, env, static) :|: 1 <= i186 && 1 <= i184 && i199 <= 0 && 0 <= i203' && i186 + -1 = i203'
main_LE_52(i11, i3, env, static) -{0,0}> main_LE_53(i11, i3, env, static) :|: i11 <= 0
main_Load_1(i1, i3, env, static) -{16,16}> main_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_713(i184, i200, i256, x, env, static) -{1,1}> main_Load_650(i184, i200, i256, 0, env, static) :|: 1 <= i200 && 1 <= i256 && 1 <= i184 && 0 < i256 && 0 <= i256 && 0 <= 0 && x = 0
main_LE_658(i184, i199, iconst_0, env, static) -{0,0}> main_LE_667(i184, i199, 0, env, static) :|: 0 <= iconst_0 && i199 <= 0 && iconst_0 = 0 && 1 <= i184
main_LE_713(i184, i200, iconst_0, x, env, static) -{0,0}> main_LE_715(i184, i200, 0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && x = iconst_0

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

Simplified expressions.

(28) Obligation:

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

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

(30) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 55 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_43(i1, i3, env, static) :|: 0 <= static
main_Load_43(i1, i3, env, static) -{0,0}> main_Load_45(i1, i3, env, static) :|: 0 >= 0
main_Load_45(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_56(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_56(i12, i3, env, static) -{1,1}> main_LE_58(i12, i3, env, static) :|: 1 <= i12
main_LE_58(i12, i3, env, static) -{0,0}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12
main_LE_629(i184, i199, i186, env, static) -{0,0}> main_LE_634(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_629(i184, i200, i186, env, static) -{0,0}> main_LE_635(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184
main_LE_634(i184, i199, i186, env, static) -{1,1}> main_Inc_639(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_635(i184, i200, i186, env, static) -{1,1}> main_Inc_641(i184, i200, i186, env, static) :|: 1 <= i186 && 1 <= i200 && 1 <= i184 && 0 < i200
main_Inc_639(i184, i199, i186, env, static) -{1,1}> main_JMP_643(i184, i199, i203, env, static) :|: 1 <= i186 && i186 + -1 = i203 && i199 <= 0 && 0 <= i203 && 1 <= i184
main_Inc_641(i184, i200, i186, env, static) -{1,1}> main_JMP_645(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184 && i200 + -1 = i204
main_JMP_643(i184, i199, i203, env, static) -{1,1}> main_Load_647(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_JMP_645(i184, i200, i186, i204, env, static) -{1,1}> main_Load_650(i184, i200, i186, i204, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_Load_647(i184, i199, i203, env, static) -{1,1}> main_LE_658(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{0,0}> main_LE_669(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184 && 0 <= i227
main_LE_665(i184, i200, iconst_0, i186, env, static) -{0,0}> main_LE_671(i184, i200, iconst_0, i186, env, static) :|: 1 <= i186 && 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_665(i184, i229, i228, i186, env, static) -{0,0}> main_LE_672(i184, i229, i228, i186, env, static) :|: 1 <= i186 && 1 <= i229 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i228
main_LE_669(i184, i199, i227, env, static) -{1,1}> main_Load_678(i184, i199, i227, env, static) :|: 0 < i227 && i199 <= 0 && 1 <= i227 && 1 <= i184
main_LE_671(i184, i200, iconst_0, i186, env, static) -{1,1}> main_Inc_682(i184, i200, i186, iconst_0, env, static) :|: 1 <= i186 && iconst_0 <= 0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_672(i184, i229, i228, i186, env, static) -{1,1}> main_Inc_684(i184, i229, i186, i228, env, static) :|: 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 < i228
main_Load_678(i184, i199, i227, env, static) -{1,1}> main_LE_686(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_Inc_682(i184, i200, i186, iconst_0, env, static) -{1,1}> main_JMP_687(i184, i200, i234, iconst_0, env, static) :|: 1 <= i186 && i186 + -1 = i234 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Inc_684(i184, i229, i186, i228, env, static) -{1,1}> main_JMP_688(i184, i229, i186, i235, env, static) :|: i228 + -1 = i235 && 1 <= i186 && 1 <= i228 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_LE_686(i184, i199, i227, env, static) -{0,0}> main_LE_629(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_JMP_687(i184, i200, i234, iconst_0, env, static) -{1,1}> main_Load_689(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_JMP_688(i184, i229, i186, i235, env, static) -{1,1}> main_Load_704(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_Load_689(i184, i200, i234, iconst_0, env, static) -{1,1}> main_LE_713(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Load_704(i184, i229, i186, i235, env, static) -{0,0}> main_Load_650(i184, i229, i186, i235, env, static) :|: 1 <= i186 && 1 <= i229 && 2 <= i229 && 1 <= i184 && 0 <= i235
main_LE_713(i184, i200, i256, iconst_0, env, static) -{0,0}> main_LE_716(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256 && 0 <= i256
main_LE_716(i184, i200, i256, iconst_0, env, static) -{1,1}> main_Load_732(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 < i256 && 1 <= i256
main_Load_732(i184, i200, i256, iconst_0, env, static) -{0,0}> main_Load_650(i184, i200, i256, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256

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

obtained
main_Load_1(i1, i3, env, static) -{18,18}> main_LE_629(i1, i3, i1, env, static'1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i3, env, static) -{1,1}> main_Load_41(i1, i3, env, static) :|: 0 >= 0
main_Load_41(i1, i3, env, static) -{0,0}> main_Load_42(i1, i3, env, static) :|: 0 >= 0
main_Load_42(i1, i3, env, static) -{0,0}> main_Load_43(i1, i3, env, static) :|: 0 <= static
main_Load_43(i1, i3, env, static) -{0,0}> main_Load_45(i1, i3, env, static) :|: 0 >= 0
main_Load_45(i1, i3, env, static) -{0,0}> main_Load_47(i1, i3, env, static) :|: 0 >= 0
main_Load_47(i1, i3, env, static) -{1,1}> main_LE_52(i1, i3, env, static) :|: 0 >= 0
main_LE_52(i12, i3, env, static) -{0,0}> main_LE_54(i12, i3, env, static) :|: 1 <= i12
main_LE_54(i12, i3, env, static) -{1,1}> main_Load_56(i12, i3, env, static) :|: 0 < i12 && 1 <= i12
main_Load_56(i12, i3, env, static) -{1,1}> main_LE_58(i12, i3, env, static) :|: 1 <= i12
main_LE_58(i12, i3, env, static) -{0,0}> main_LE_629(i12, i3, i12, env, static) :|: 1 <= i12

obtained
main_LE_665(i184, i200, 0, i186, env, static) -{5,5}> main_Load_650(i184, i200, i234', 0, env, static) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186
by chaining
main_LE_665(i184, i200, iconst_0, i186, env, static) -{0,0}> main_LE_671(i184, i200, iconst_0, i186, env, static) :|: 1 <= i186 && 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_LE_671(i184, i200, iconst_0, i186, env, static) -{1,1}> main_Inc_682(i184, i200, i186, iconst_0, env, static) :|: 1 <= i186 && iconst_0 <= 0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184
main_Inc_682(i184, i200, i186, iconst_0, env, static) -{1,1}> main_JMP_687(i184, i200, i234, iconst_0, env, static) :|: 1 <= i186 && i186 + -1 = i234 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_JMP_687(i184, i200, i234, iconst_0, env, static) -{1,1}> main_Load_689(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_Load_689(i184, i200, i234, iconst_0, env, static) -{1,1}> main_LE_713(i184, i200, i234, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 <= i234
main_LE_713(i184, i200, i256, iconst_0, env, static) -{0,0}> main_LE_716(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256 && 0 <= i256
main_LE_716(i184, i200, i256, iconst_0, env, static) -{1,1}> main_Load_732(i184, i200, i256, iconst_0, env, static) :|: 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 0 < i256 && 1 <= i256
main_Load_732(i184, i200, i256, iconst_0, env, static) -{0,0}> main_Load_650(i184, i200, i256, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i200 && iconst_0 = 0 && 1 <= i184 && 1 <= i256

obtained
main_LE_629(i184, i199, i186, env, static) -{6,6}> main_LE_629(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'
by chaining
main_LE_629(i184, i199, i186, env, static) -{0,0}> main_LE_634(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_LE_634(i184, i199, i186, env, static) -{1,1}> main_Inc_639(i184, i199, i186, env, static) :|: 1 <= i186 && i199 <= 0 && 1 <= i184
main_Inc_639(i184, i199, i186, env, static) -{1,1}> main_JMP_643(i184, i199, i203, env, static) :|: 1 <= i186 && i186 + -1 = i203 && i199 <= 0 && 0 <= i203 && 1 <= i184
main_JMP_643(i184, i199, i203, env, static) -{1,1}> main_Load_647(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_Load_647(i184, i199, i203, env, static) -{1,1}> main_LE_658(i184, i199, i203, env, static) :|: i199 <= 0 && 0 <= i203 && 1 <= i184
main_LE_658(i184, i199, i227, env, static) -{0,0}> main_LE_669(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184 && 0 <= i227
main_LE_669(i184, i199, i227, env, static) -{1,1}> main_Load_678(i184, i199, i227, env, static) :|: 0 < i227 && i199 <= 0 && 1 <= i227 && 1 <= i184
main_Load_678(i184, i199, i227, env, static) -{1,1}> main_LE_686(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184
main_LE_686(i184, i199, i227, env, static) -{0,0}> main_LE_629(i184, i199, i227, env, static) :|: i199 <= 0 && 1 <= i227 && 1 <= i184

(34) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, env, static) -{18,18}> main_LE_629(i1, i3, i1, env, static'1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_629(i184, i200, i186, env, static) -{3,3}> main_Load_650(i184, i200, i186, i204', env, static) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204, env, static) -{1,1}> main_LE_665(i184, i200, i204, i186, env, static) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i229, i228, i186, env, static) -{3,3}> main_Load_650(i184, i229, i186, i235', env, static) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, 0, i186, env, static) -{5,5}> main_Load_650(i184, i200, i234', 0, env, static) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186
main_LE_629(i184, i199, i186, env, static) -{6,6}> main_LE_629(i184, i199, i203', env, static) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'

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

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

main_Load_1(x1, x2, x3, x4) → main_Load_1(x1, x2, x4)
main_LE_629(x1, x2, x3, x4, x5) → main_LE_629(x1, x2, x3)
main_Load_650(x1, x2, x3, x4, x5, x6) → main_Load_650(x1, x2, x3, x4)
main_LE_665(x1, x2, x3, x4, x5, x6) → main_LE_665(x1, x2, x3, x4)

(36) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i204') :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204) -{1,1}> main_LE_665(i184, i200, i204, i186) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i235') :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, 0, i186) -{5,5}> main_Load_650(i184, i200, i234', 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i203') :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'

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

Moved arithmethic from lhss to constraints.

main_LE_665(i184, i200, 0, i186) -{5,5}> main_Load_650(i184, i200, i234', 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186
was transformed to
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i234', 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0

(38) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i203') :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i204') :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_Load_650(i184, i200, i186, i204) -{1,1}> main_LE_665(i184, i200, i204, i186) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i235') :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i234', 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0

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

Moved arithmethic from constraints to rhss.

main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i204') :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
was transformed to
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'

main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i203') :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'
was transformed to
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i186 + -1) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'

main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i235') :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
was transformed to
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228

main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i234', 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0
was transformed to
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i186 + -1, 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0

(40) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i186 + -1) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'
main_Load_650(i184, i200, i186, i204) -{1,1}> main_LE_665(i184, i200, i204, i186) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i186 + -1, 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0

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

Simplified expressions.

main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i228 + -1) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 + -1 = i235' && 0 <= i228 && 0 < i228
was transformed to
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i228 - 1) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 - 1 = i235' && 0 < i228

main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i200 + -1) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 + -1 = i204'
was transformed to
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i200 - 1) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 - 1 = i204'

main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i186 + -1) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 + -1 = i203' && 0 <= i203'
was transformed to
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i186 - 1) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 - 1 = i203'

main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i186 + -1, 0) :|: 0 <= i234' && 1 <= i234' && i186 + -1 = i234' && 1 <= i184 && 1 <= i200 && 0 <= 0 && 0 < i234' && 1 <= i186 && x = 0
was transformed to
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i186 - 1, 0) :|: 1 <= i234' && i186 - 1 = i234' && 1 <= i184 && 1 <= i200 && 0 < i234' && 1 <= i186 && x = 0

(42) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_650(i184, i200, i186, i204) -{1,1}> main_LE_665(i184, i200, i204, i186) :|: 1 <= i186 && 0 <= i204 && 1 <= i200 && 1 <= i184
main_LE_665(i184, i229, i228, i186) -{3,3}> main_Load_650(i184, i229, i186, i228 - 1) :|: 1 <= i229 && 0 <= i235' && 1 <= i228 && 1 <= i184 && 2 <= i229 && 1 <= i186 && i228 - 1 = i235' && 0 < i228
main_Load_1(i1, i3, static) -{18,18}> main_LE_629(i1, i3, i1) :|: 1 <= i1 && 0 < i1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_665(i184, i200, x, i186) -{5,5}> main_Load_650(i184, i200, i186 - 1, 0) :|: 1 <= i234' && i186 - 1 = i234' && 1 <= i184 && 1 <= i200 && 0 < i234' && 1 <= i186 && x = 0
main_LE_629(i184, i200, i186) -{3,3}> main_Load_650(i184, i200, i186, i200 - 1) :|: 0 <= i204' && 1 <= i184 && 0 < i200 && 1 <= i200 && 1 <= i186 && i200 - 1 = i204'
main_LE_629(i184, i199, i186) -{6,6}> main_LE_629(i184, i199, i186 - 1) :|: 1 <= i186 && 1 <= i184 && 0 < i203' && i199 <= 0 && 1 <= i203' && i186 - 1 = i203'

(43) koat Proof (EQUIVALENT transformation)

YES(?, 24*ar_0 + 18*ar_1 + 21)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 1) main_Load_650(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_665(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3, ar_2 - 1)) [ 1 <= ar_1 /\ 0 <= i235' /\ 1 <= ar_2 /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_3 /\ ar_2 - 1 = i235' /\ 0 < ar_2 ]
(Comp: ?, Cost: 18) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 5) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3 - 1, 0)) [ 1 <= i234' /\ ar_3 - 1 = i234' /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < i234' /\ 1 <= ar_3 /\ ar_2 = 0 ]
(Comp: ?, Cost: 3) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_2, ar_1 - 1)) [ 0 <= i204' /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ ar_1 - 1 = i204' ]
(Comp: ?, Cost: 6) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_2 - 1, arityPad)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 0 < i203' /\ ar_1 <= 0 /\ 1 <= i203' /\ ar_2 - 1 = i203' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 1) main_Load_650(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_665(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 3) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3, ar_2 - 1)) [ 1 <= ar_1 /\ 0 <= i235' /\ 1 <= ar_2 /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_3 /\ ar_2 - 1 = i235' /\ 0 < ar_2 ]
(Comp: 1, Cost: 18) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 5) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3 - 1, 0)) [ 1 <= i234' /\ ar_3 - 1 = i234' /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < i234' /\ 1 <= ar_3 /\ ar_2 = 0 ]
(Comp: 1, Cost: 3) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_2, ar_1 - 1)) [ 0 <= i204' /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ ar_1 - 1 = i204' ]
(Comp: ?, Cost: 6) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_2 - 1, arityPad)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 0 < i203' /\ ar_1 <= 0 /\ 1 <= i203' /\ ar_2 - 1 = i203' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_650) = 2*V_3 + 2*V_4
Pol(main_LE_665) = 2*V_3 + 2*V_4 - 1
Pol(main_Load_1) = 2*V_1 + 2*V_2
Pol(main_LE_629) = 2*V_2 + 2*V_3
Pol(koat_start) = 2*V_1 + 2*V_2
orients all transitions weakly and the transitions
main_Load_650(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_665(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3, ar_2 - 1)) [ 1 <= ar_1 /\ 0 <= i235' /\ 1 <= ar_2 /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_3 /\ ar_2 - 1 = i235' /\ 0 < ar_2 ]
main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3 - 1, 0)) [ 1 <= i234' /\ ar_3 - 1 = i234' /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < i234' /\ 1 <= ar_3 /\ ar_2 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 2*ar_0 + 2*ar_1, Cost: 1) main_Load_650(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_665(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 3) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3, ar_2 - 1)) [ 1 <= ar_1 /\ 0 <= i235' /\ 1 <= ar_2 /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_3 /\ ar_2 - 1 = i235' /\ 0 < ar_2 ]
(Comp: 1, Cost: 18) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 5) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3 - 1, 0)) [ 1 <= i234' /\ ar_3 - 1 = i234' /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < i234' /\ 1 <= ar_3 /\ ar_2 = 0 ]
(Comp: 1, Cost: 3) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_2, ar_1 - 1)) [ 0 <= i204' /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ ar_1 - 1 = i204' ]
(Comp: ?, Cost: 6) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_2 - 1, arityPad)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 0 < i203' /\ ar_1 <= 0 /\ 1 <= i203' /\ ar_2 - 1 = i203' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_650) = 0
Pol(main_LE_665) = 0
Pol(main_Load_1) = V_1
Pol(main_LE_629) = V_3
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_2 - 1, arityPad)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 0 < i203' /\ ar_1 <= 0 /\ 1 <= i203' /\ ar_2 - 1 = i203' ]
strictly and produces the following problem:
4: T:
(Comp: 2*ar_0 + 2*ar_1, Cost: 1) main_Load_650(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_665(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 1 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 3) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3, ar_2 - 1)) [ 1 <= ar_1 /\ 0 <= i235' /\ 1 <= ar_2 /\ 1 <= ar_0 /\ 2 <= ar_1 /\ 1 <= ar_3 /\ ar_2 - 1 = i235' /\ 0 < ar_2 ]
(Comp: 1, Cost: 18) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 < ar_0 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 5) main_LE_665(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_3 - 1, 0)) [ 1 <= i234' /\ ar_3 - 1 = i234' /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < i234' /\ 1 <= ar_3 /\ ar_2 = 0 ]
(Comp: 1, Cost: 3) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_650(ar_0, ar_1, ar_2, ar_1 - 1)) [ 0 <= i204' /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ ar_1 - 1 = i204' ]
(Comp: ar_0, Cost: 6) main_LE_629(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_629(ar_0, ar_1, ar_2 - 1, arityPad)) [ 1 <= ar_2 /\ 1 <= ar_0 /\ 0 < i203' /\ ar_1 <= 0 /\ 1 <= i203' /\ ar_2 - 1 = i203' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 24*ar_0 + 18*ar_1 + 21

Time: 0.180 sec (SMT: 0.161 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

(43) koat Proof (EQUIVALENT transformation)

(44) BOUNDS(CONSTANT, 21 + 24 * |#0| + 18 * |#1|)