time complexity proof of /tmp/tmpIoAg6m/PastaB17.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 33 + 16 * |#0| + 5 * |#1| + 21 * |#2|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

    ↳13 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 82 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 9 ms)

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

↳22 JBCComplexityEdges

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

    ↳24 WeightedIntTrs

    ↳25 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 49 ms)

    ↳26 WeightedIntTrs

    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 41 ms)

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 83 ms)

    ↳34 BOUNDS(CONSTANT, 27 + 16 * |#0| + 5 * |#1| + 21 * |#2|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

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

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaB17.main(III)V: Graph of 72 nodes with 2 SCCs.

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

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

(4) Obligation:

Set of 68 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 68 jbc graph edges to a weighted ITS with 68 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 68 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_LE_54(i1, i4, i6, env, static) :|: 0 >= 0
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_56(i1, i4, i6, env, static) :|: i1 <= i6
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_57(i1, i4, i6, env, static) :|: i6 < i1
main_LE_57(i1, i4, i6, env, static) -{1,1}> main_Load_63(i1, i4, i6, env, static) :|: i6 < i1
main_Load_63(i1, i4, i6, env, static) -{1,1}> main_Load_65(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_65(i1, i4, i6, env, static) -{1,1}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_78(i1, i4, i6, env, static) :|: i4 <= i6
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_80(i1, i4, i6, env, static) :|: i6 < i4
main_LE_78(i1, i4, i6, env, static) -{1,1}> main_Inc_81(i1, i4, i6, env, static) :|: i4 <= i6
main_LE_80(i1, i4, i6, env, static) -{1,1}> main_Inc_82(i1, i4, i6, env, static) :|: i6 < i4
main_Inc_81(i1, i4, i6, env, static) -{1,1}> main_JMP_83(i1, i4, i6, i9, env, static) :|: i1 + -1 = i9
main_Inc_82(i1, i4, i6, env, static) -{1,1}> main_JMP_84(i1, i4, i6, i10, env, static) :|: i4 + -1 = i10
main_JMP_83(i1, i4, i6, i9, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i9, env, static) :|: 0 >= 0
main_JMP_84(i1, i4, i6, i10, env, static) -{0,0}> main_JMP_198(i1, i4, i6, i10, env, static) :|: 0 >= 0
main_JMP_198(i1, i4, i6, i41, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i1, i41, env, static) :|: 0 >= 0
main_JMP_286(i1, i4, i6, i70, env, static) -{1,1}> main_Load_292(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_292(i1, i4, i6, i70, env, static) -{1,1}> main_Load_308(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_308(i1, i4, i6, i70, env, static) -{1,1}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_328(i1, i4, i6, i70, env, static) :|: i70 <= i6
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_329(i1, i4, i6, i70, env, static) :|: i6 < i70
main_LE_329(i1, i4, i6, i70, env, static) -{1,1}> main_Load_347(i1, i4, i6, i70, env, static) :|: i6 < i70
main_Load_347(i1, i4, i6, i70, env, static) -{1,1}> main_Load_370(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_370(i1, i4, i6, i70, env, static) -{1,1}> main_LE_385(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_385(i1, i4, i6, i70, env, static) -{0,0}> main_LE_433(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_LE_433(i1, i4, i6, i70, env, static) -{1,1}> main_Inc_442(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_Inc_442(i1, i4, i6, i70, env, static) -{1,1}> main_JMP_458(i1, i4, i6, i165, env, static) :|: i70 + -1 = i165
main_JMP_458(i1, i4, i6, i165, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i165, env, static) :|: 0 >= 0
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_Load_483(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_506(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_Load_506(i1, i4, i6, i181, i180, env, static) -{1,1}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_538(i1, i4, i6, i181, i180, env, static) :|: i181 <= i6
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_539(i1, i4, i6, i181, i180, env, static) :|: i6 < i181
main_LE_538(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_561(i1, i4, i6, i180, i181, env, static) :|: i181 <= i6
main_LE_539(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_562(i1, i4, i6, i180, i181, env, static) :|: i6 < i181
main_Inc_561(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_573(i1, i4, i6, i220, i181, env, static) :|: i180 + -1 = i220
main_Inc_562(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_583(i1, i4, i6, i180, i225, env, static) :|: i181 + -1 = i225
main_JMP_573(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_584(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_JMP_583(i1, i4, i6, i180, i225, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i180, i225, env, static) :|: 0 >= 0
main_Load_584(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_600(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_600(i1, i4, i6, i220, i181, env, static) -{1,1}> main_LE_604(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_609(i1, i4, i6, i220, i181, env, static) :|: i220 <= i6
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_610(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_LE_610(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_625(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_Load_625(i1, i4, i6, i220, i181, env, static) -{0,0}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i4, i6, env, static) -{17,17}> main_LE_54(i1, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_LE_54(i1, i4, i6, env, static) :|: 0 >= 0

obtained
main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0 && i6 < i1
by chaining
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_57(i1, i4, i6, env, static) :|: i6 < i1
main_LE_57(i1, i4, i6, env, static) -{1,1}> main_Load_63(i1, i4, i6, env, static) :|: i6 < i1
main_Load_63(i1, i4, i6, env, static) -{1,1}> main_Load_65(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_65(i1, i4, i6, env, static) -{1,1}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0

obtained
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i1, i10', env, static) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
by chaining
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_80(i1, i4, i6, env, static) :|: i6 < i4
main_LE_80(i1, i4, i6, env, static) -{1,1}> main_Inc_82(i1, i4, i6, env, static) :|: i6 < i4
main_Inc_82(i1, i4, i6, env, static) -{1,1}> main_JMP_84(i1, i4, i6, i10, env, static) :|: i4 + -1 = i10
main_JMP_84(i1, i4, i6, i10, env, static) -{0,0}> main_JMP_198(i1, i4, i6, i10, env, static) :|: 0 >= 0
main_JMP_198(i1, i4, i6, i41, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i1, i41, env, static) :|: 0 >= 0

obtained
main_Load_483(i1, i4, i6, i180, i181, env, static) -{2,2}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
by chaining
main_Load_483(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_506(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_Load_506(i1, i4, i6, i181, i180, env, static) -{1,1}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0

obtained
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i225', env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
by chaining
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_539(i1, i4, i6, i181, i180, env, static) :|: i6 < i181
main_LE_539(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_562(i1, i4, i6, i180, i181, env, static) :|: i6 < i181
main_Inc_562(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_583(i1, i4, i6, i180, i225, env, static) :|: i181 + -1 = i225
main_JMP_583(i1, i4, i6, i180, i225, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i180, i225, env, static) :|: 0 >= 0

obtained
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i220', i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'
by chaining
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_538(i1, i4, i6, i181, i180, env, static) :|: i181 <= i6
main_LE_538(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_561(i1, i4, i6, i180, i181, env, static) :|: i181 <= i6
main_Inc_561(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_573(i1, i4, i6, i220, i181, env, static) :|: i180 + -1 = i220
main_JMP_573(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_584(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_584(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_600(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_600(i1, i4, i6, i220, i181, env, static) -{1,1}> main_LE_604(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0

obtained
main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220 && 0 >= 0
by chaining
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_610(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_LE_610(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_625(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_Load_625(i1, i4, i6, i220, i181, env, static) -{0,0}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0

obtained
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_286(i1, i4, i6, i9', env, static) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
by chaining
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_78(i1, i4, i6, env, static) :|: i4 <= i6
main_LE_78(i1, i4, i6, env, static) -{1,1}> main_Inc_81(i1, i4, i6, env, static) :|: i4 <= i6
main_Inc_81(i1, i4, i6, env, static) -{1,1}> main_JMP_83(i1, i4, i6, i9, env, static) :|: i1 + -1 = i9
main_JMP_83(i1, i4, i6, i9, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i9, env, static) :|: 0 >= 0

obtained
main_JMP_286(i1, i4, i6, i70, env, static) -{3,3}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
by chaining
main_JMP_286(i1, i4, i6, i70, env, static) -{1,1}> main_Load_292(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_292(i1, i4, i6, i70, env, static) -{1,1}> main_Load_308(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_308(i1, i4, i6, i70, env, static) -{1,1}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0

obtained
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i165', env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
by chaining
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_329(i1, i4, i6, i70, env, static) :|: i6 < i70
main_LE_329(i1, i4, i6, i70, env, static) -{1,1}> main_Load_347(i1, i4, i6, i70, env, static) :|: i6 < i70
main_Load_347(i1, i4, i6, i70, env, static) -{1,1}> main_Load_370(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_370(i1, i4, i6, i70, env, static) -{1,1}> main_LE_385(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_385(i1, i4, i6, i70, env, static) -{0,0}> main_LE_433(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_LE_433(i1, i4, i6, i70, env, static) -{1,1}> main_Inc_442(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_Inc_442(i1, i4, i6, i70, env, static) -{1,1}> main_JMP_458(i1, i4, i6, i165, env, static) :|: i70 + -1 = i165
main_JMP_458(i1, i4, i6, i165, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i165, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 14 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, i4, i6, env, static) -{17,17}> main_LE_54(i1, i4, i6, 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_54(i1, i4, i6, env, static) -{0,0}> main_LE_56(i1, i4, i6, env, static) :|: i1 <= i6
main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0 && i6 < i1
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i1, i10', env, static) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_Load_483(i1, i4, i6, i180, i181, env, static) -{2,2}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i225', env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i220', i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_609(i1, i4, i6, i220, i181, env, static) :|: i220 <= i6
main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220 && 0 >= 0
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_286(i1, i4, i6, i9', env, static) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
main_JMP_286(i1, i4, i6, i70, env, static) -{3,3}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_328(i1, i4, i6, i70, env, static) :|: i70 <= i6
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i165', env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'

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

Moved arithmethic from constraints to rhss.

main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i225', env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
was transformed to
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i181 + -1, env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'

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

main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i220', i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'
was transformed to
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i180 + -1, i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'

main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i165', env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
was transformed to
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i70 + -1, env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'

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

(10) Obligation:

IntTrs with 14 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i181 + -1, env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_56(i1, i4, i6, env, static) :|: i1 <= i6
main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0 && i6 < i1
main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220 && 0 >= 0
main_Load_483(i1, i4, i6, i180, i181, env, static) -{2,2}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_286(i1, i4, i6, i1 + -1, env, static) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i180 + -1, i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i70 + -1, env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_609(i1, i4, i6, i220, i181, env, static) :|: i220 <= i6
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i1, i4 + -1, env, static) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
main_Load_1(i1, i4, i6, env, static) -{17,17}> main_LE_54(i1, i4, i6, 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_JMP_286(i1, i4, i6, i70, env, static) -{3,3}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_328(i1, i4, i6, i70, env, static) :|: i70 <= i6

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

Simplified expressions.

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

main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0 && i6 < i1
was transformed to
main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: i6 < i1

main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220 && 0 >= 0
was transformed to
main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220

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

main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i180 + -1, i181, env, static) :|: 0 >= 0 && i181 <= i6 && i180 + -1 = i220'
was transformed to
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i180 - 1, i181, env, static) :|: i181 <= i6 && i180 - 1 = i220'

main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i181 + -1, env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
was transformed to
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i181 - 1, env, static) :|: i6 < i181 && i181 - 1 = i225'

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

main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i70 + -1, env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
was transformed to
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i70 - 1, env, static) :|: i6 < i70 && i4 <= i6 && i70 - 1 = i165'

(12) Obligation:

IntTrs with 14 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_54(i1, i4, i6, env, static) -{3,3}> main_LE_70(i1, i4, i6, env, static) :|: i6 < i1
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_56(i1, i4, i6, env, static) :|: i1 <= i6
main_LE_320(i1, i4, i6, i70, env, static) -{5,5}> main_JMP_286(i1, i4, i6, i70 - 1, env, static) :|: i6 < i70 && i4 <= i6 && i70 - 1 = i165'
main_Load_483(i1, i4, i6, i180, i181, env, static) -{2,2}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_537(i1, i4, i6, i181, i180, env, static) -{5,5}> main_LE_604(i1, i4, i6, i180 - 1, i181, env, static) :|: i181 <= i6 && i180 - 1 = i220'
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i181 - 1, env, static) :|: i6 < i181 && i181 - 1 = i225'
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i1, i4 - 1, env, static) :|: i4 - 1 = i10' && i6 < i4
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_609(i1, i4, i6, i220, i181, env, static) :|: i220 <= i6
main_Load_1(i1, i4, i6, env, static) -{17,17}> main_LE_54(i1, i4, i6, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_286(i1, i4, i6, i1 - 1, env, static) :|: i4 <= i6 && i1 - 1 = i9'
main_JMP_286(i1, i4, i6, i70, env, static) -{3,3}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_604(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_328(i1, i4, i6, i70, env, static) :|: i70 <= i6

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

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

(14) Obligation:

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

(16) Obligation:

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

Moved arithmethic from constraints to rhss.

(18) Obligation:

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

Simplified expressions.

(20) Obligation:

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

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

(22) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 65 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_LE_54(i1, i4, i6, env, static) :|: 0 >= 0
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_57(i1, i4, i6, env, static) :|: i6 < i1
main_LE_57(i1, i4, i6, env, static) -{1,1}> main_Load_63(i1, i4, i6, env, static) :|: i6 < i1
main_Load_63(i1, i4, i6, env, static) -{1,1}> main_Load_65(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_65(i1, i4, i6, env, static) -{1,1}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_78(i1, i4, i6, env, static) :|: i4 <= i6
main_LE_70(i1, i4, i6, env, static) -{0,0}> main_LE_80(i1, i4, i6, env, static) :|: i6 < i4
main_LE_78(i1, i4, i6, env, static) -{1,1}> main_Inc_81(i1, i4, i6, env, static) :|: i4 <= i6
main_LE_80(i1, i4, i6, env, static) -{1,1}> main_Inc_82(i1, i4, i6, env, static) :|: i6 < i4
main_Inc_81(i1, i4, i6, env, static) -{1,1}> main_JMP_83(i1, i4, i6, i9, env, static) :|: i1 + -1 = i9
main_Inc_82(i1, i4, i6, env, static) -{1,1}> main_JMP_84(i1, i4, i6, i10, env, static) :|: i4 + -1 = i10
main_JMP_83(i1, i4, i6, i9, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i9, env, static) :|: 0 >= 0
main_JMP_84(i1, i4, i6, i10, env, static) -{0,0}> main_JMP_198(i1, i4, i6, i10, env, static) :|: 0 >= 0
main_JMP_198(i1, i4, i6, i41, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i1, i41, env, static) :|: 0 >= 0
main_JMP_286(i1, i4, i6, i70, env, static) -{1,1}> main_Load_292(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_292(i1, i4, i6, i70, env, static) -{1,1}> main_Load_308(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_308(i1, i4, i6, i70, env, static) -{1,1}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_329(i1, i4, i6, i70, env, static) :|: i6 < i70
main_LE_329(i1, i4, i6, i70, env, static) -{1,1}> main_Load_347(i1, i4, i6, i70, env, static) :|: i6 < i70
main_Load_347(i1, i4, i6, i70, env, static) -{1,1}> main_Load_370(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_370(i1, i4, i6, i70, env, static) -{1,1}> main_LE_385(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_385(i1, i4, i6, i70, env, static) -{0,0}> main_LE_433(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_LE_433(i1, i4, i6, i70, env, static) -{1,1}> main_Inc_442(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_Inc_442(i1, i4, i6, i70, env, static) -{1,1}> main_JMP_458(i1, i4, i6, i165, env, static) :|: i70 + -1 = i165
main_JMP_458(i1, i4, i6, i165, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i165, env, static) :|: 0 >= 0
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_Load_483(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_506(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_Load_506(i1, i4, i6, i181, i180, env, static) -{1,1}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_538(i1, i4, i6, i181, i180, env, static) :|: i181 <= i6
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_539(i1, i4, i6, i181, i180, env, static) :|: i6 < i181
main_LE_538(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_561(i1, i4, i6, i180, i181, env, static) :|: i181 <= i6
main_LE_539(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_562(i1, i4, i6, i180, i181, env, static) :|: i6 < i181
main_Inc_561(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_573(i1, i4, i6, i220, i181, env, static) :|: i180 + -1 = i220
main_Inc_562(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_583(i1, i4, i6, i180, i225, env, static) :|: i181 + -1 = i225
main_JMP_573(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_584(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_JMP_583(i1, i4, i6, i180, i225, env, static) -{0,0}> main_JMP_480(i1, i4, i6, i180, i225, env, static) :|: 0 >= 0
main_Load_584(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_600(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_600(i1, i4, i6, i220, i181, env, static) -{1,1}> main_LE_604(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_610(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_LE_610(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_625(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_Load_625(i1, i4, i6, i220, i181, env, static) -{0,0}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i1, i4, i6, env, static) -{20,20}> main_LE_70(i1, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && i6 < i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i1, i4, i6, env, static) -{0,0}> main_Load_4(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_29(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_31(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_38(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_43(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, i4, i6, env, static) -{1,1}> main_Load_46(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i1, i4, i6, env, static) -{0,0}> main_Load_47(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 <= static
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{0,0}> main_Load_50(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_LE_54(i1, i4, i6, env, static) :|: 0 >= 0
main_LE_54(i1, i4, i6, env, static) -{0,0}> main_LE_57(i1, i4, i6, env, static) :|: i6 < i1
main_LE_57(i1, i4, i6, env, static) -{1,1}> main_Load_63(i1, i4, i6, env, static) :|: i6 < i1
main_Load_63(i1, i4, i6, env, static) -{1,1}> main_Load_65(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_65(i1, i4, i6, env, static) -{1,1}> main_LE_70(i1, i4, i6, env, static) :|: 0 >= 0

obtained
main_LE_537(i1, i4, i6, i181, i180, env, static) -{6,6}> main_Load_483(i1, i4, i6, i220', i181, env, static) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
by chaining
main_LE_537(i1, i4, i6, i181, i180, env, static) -{0,0}> main_LE_538(i1, i4, i6, i181, i180, env, static) :|: i181 <= i6
main_LE_538(i1, i4, i6, i181, i180, env, static) -{1,1}> main_Inc_561(i1, i4, i6, i180, i181, env, static) :|: i181 <= i6
main_Inc_561(i1, i4, i6, i180, i181, env, static) -{1,1}> main_JMP_573(i1, i4, i6, i220, i181, env, static) :|: i180 + -1 = i220
main_JMP_573(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_584(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_584(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_600(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_Load_600(i1, i4, i6, i220, i181, env, static) -{1,1}> main_LE_604(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0
main_LE_604(i1, i4, i6, i220, i181, env, static) -{0,0}> main_LE_610(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_LE_610(i1, i4, i6, i220, i181, env, static) -{1,1}> main_Load_625(i1, i4, i6, i220, i181, env, static) :|: i6 < i220
main_Load_625(i1, i4, i6, i220, i181, env, static) -{0,0}> main_Load_483(i1, i4, i6, i220, i181, env, static) :|: 0 >= 0

obtained
main_JMP_286(i1, i4, i6, i70, env, static) -{8,8}> main_JMP_286(i1, i4, i6, i165', env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
by chaining
main_JMP_286(i1, i4, i6, i70, env, static) -{1,1}> main_Load_292(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_292(i1, i4, i6, i70, env, static) -{1,1}> main_Load_308(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_308(i1, i4, i6, i70, env, static) -{1,1}> main_LE_320(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_320(i1, i4, i6, i70, env, static) -{0,0}> main_LE_329(i1, i4, i6, i70, env, static) :|: i6 < i70
main_LE_329(i1, i4, i6, i70, env, static) -{1,1}> main_Load_347(i1, i4, i6, i70, env, static) :|: i6 < i70
main_Load_347(i1, i4, i6, i70, env, static) -{1,1}> main_Load_370(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_Load_370(i1, i4, i6, i70, env, static) -{1,1}> main_LE_385(i1, i4, i6, i70, env, static) :|: 0 >= 0
main_LE_385(i1, i4, i6, i70, env, static) -{0,0}> main_LE_433(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_LE_433(i1, i4, i6, i70, env, static) -{1,1}> main_Inc_442(i1, i4, i6, i70, env, static) :|: i4 <= i6
main_Inc_442(i1, i4, i6, i70, env, static) -{1,1}> main_JMP_458(i1, i4, i6, i165, env, static) :|: i70 + -1 = i165
main_JMP_458(i1, i4, i6, i165, env, static) -{0,0}> main_JMP_286(i1, i4, i6, i165, env, static) :|: 0 >= 0

(26) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, env, static) -{20,20}> main_LE_70(i1, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && i6 < i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i1, i10', env, static) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
main_JMP_480(i1, i4, i6, i180, i181, env, static) -{1,1}> main_Load_483(i1, i4, i6, i180, i181, env, static) :|: 0 >= 0
main_Load_483(i1, i4, i6, i180, i181, env, static) -{2,2}> main_LE_537(i1, i4, i6, i181, i180, env, static) :|: 0 >= 0
main_LE_537(i1, i4, i6, i181, i180, env, static) -{2,2}> main_JMP_480(i1, i4, i6, i180, i225', env, static) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
main_LE_537(i1, i4, i6, i181, i180, env, static) -{6,6}> main_Load_483(i1, i4, i6, i220', i181, env, static) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
main_LE_70(i1, i4, i6, env, static) -{2,2}> main_JMP_286(i1, i4, i6, i9', env, static) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
main_JMP_286(i1, i4, i6, i70, env, static) -{8,8}> main_JMP_286(i1, i4, i6, i165', env, static) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'

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

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

main_Load_1(x1, x2, x3, x4, x5) → main_Load_1(x1, x2, x3, x5)
main_LE_70(x1, x2, x3, x4, x5) → main_LE_70(x1, x2, x3)
main_LE_537(x1, x2, x3, x4, x5, x6, x7) → main_LE_537(x3, x4, x5)
main_JMP_286(x1, x2, x3, x4, x5, x6) → main_JMP_286(x2, x3, x4)
main_Load_483(x1, x2, x3, x4, x5, x6, x7) → main_Load_483(x3, x4, x5)
main_JMP_480(x1, x2, x3, x4, x5, x6, x7) → main_JMP_480(x3, x4, x5)

(28) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, static) -{20,20}> main_LE_70(i1, i4, i6) :|: 0 >= 0 && 0 < 2 && i6 < i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i10') :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
main_JMP_480(i6, i180, i181) -{1,1}> main_Load_483(i6, i180, i181) :|: 0 >= 0
main_Load_483(i6, i180, i181) -{2,2}> main_LE_537(i6, i181, i180) :|: 0 >= 0
main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i225') :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i220', i181) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i9') :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i165') :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'

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

Moved arithmethic from constraints to rhss.

main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i9') :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
was transformed to
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i1 + -1) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'

main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i220', i181) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
was transformed to
main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i180 + -1, i181) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6

main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i10') :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
was transformed to
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i4 + -1) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4

main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i225') :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
was transformed to
main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i181 + -1) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'

main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i165') :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
was transformed to
main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i70 + -1) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'

(30) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, i4, i6, static) -{20,20}> main_LE_70(i1, i4, i6) :|: 0 >= 0 && 0 < 2 && i6 < i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i1 + -1) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i180 + -1, i181) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i4 + -1) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i181 + -1) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
main_JMP_480(i6, i180, i181) -{1,1}> main_Load_483(i6, i180, i181) :|: 0 >= 0
main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i70 + -1) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
main_Load_483(i6, i180, i181) -{2,2}> main_LE_537(i6, i181, i180) :|: 0 >= 0

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

Simplified expressions.

main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i181 + -1) :|: 0 >= 0 && i6 < i181 && i181 + -1 = i225'
was transformed to
main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i181 - 1) :|: i6 < i181 && i181 - 1 = i225'

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

main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i180 + -1, i181) :|: 0 >= 0 && i180 + -1 = i220' && i6 < i220' && i181 <= i6
was transformed to
main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i180 - 1, i181) :|: i180 - 1 = i220' && i6 < i220' && i181 <= i6

main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i70 + -1) :|: 0 >= 0 && i6 < i70 && i4 <= i6 && i70 + -1 = i165'
was transformed to
main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i70 - 1) :|: i6 < i70 && i4 <= i6 && i70 - 1 = i165'

main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i4 + -1) :|: 0 >= 0 && i4 + -1 = i10' && i6 < i4
was transformed to
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i4 - 1) :|: i4 - 1 = i10' && i6 < i4

main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i1 + -1) :|: 0 >= 0 && i4 <= i6 && i1 + -1 = i9'
was transformed to
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i1 - 1) :|: i4 <= i6 && i1 - 1 = i9'

(32) Obligation:

IntTrs with 8 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_JMP_286(i4, i6, i70) -{8,8}> main_JMP_286(i4, i6, i70 - 1) :|: i6 < i70 && i4 <= i6 && i70 - 1 = i165'
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_286(i4, i6, i1 - 1) :|: i4 <= i6 && i1 - 1 = i9'
main_JMP_480(i6, i180, i181) -{1,1}> main_Load_483(i6, i180, i181) :|: 0 >= 0
main_LE_70(i1, i4, i6) -{2,2}> main_JMP_480(i6, i1, i4 - 1) :|: i4 - 1 = i10' && i6 < i4
main_Load_483(i6, i180, i181) -{2,2}> main_LE_537(i6, i181, i180) :|: 0 >= 0
main_LE_537(i6, i181, i180) -{6,6}> main_Load_483(i6, i180 - 1, i181) :|: i180 - 1 = i220' && i6 < i220' && i181 <= i6
main_Load_1(i1, i4, i6, static) -{20,20}> main_LE_70(i1, i4, i6) :|: i6 < i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_537(i6, i181, i180) -{2,2}> main_JMP_480(i6, i180, i181 - 1) :|: i6 < i181 && i181 - 1 = i225'

(33) koat Proof (EQUIVALENT transformation)

YES(?, 16*ar_0 + 21*ar_2 + 5*ar_1 + 27)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
(Comp: ?, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_1, ar_2, ar_0 - 1, arityPad)) [ ar_1 <= ar_2 /\ ar_0 - 1 = i9' ]
(Comp: ?, Cost: 1) main_JMP_480(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_2, ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i10' /\ ar_2 < ar_1 ]
(Comp: ?, Cost: 2) main_Load_483(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_537(ar_0, ar_2, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 6) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
(Comp: ?, Cost: 20) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_70(ar_0, ar_1, ar_2, arityPad)) [ ar_2 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
(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: 8) main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_1, ar_2, ar_0 - 1, arityPad)) [ ar_1 <= ar_2 /\ ar_0 - 1 = i9' ]
(Comp: ?, Cost: 1) main_JMP_480(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_2, ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i10' /\ ar_2 < ar_1 ]
(Comp: ?, Cost: 2) main_Load_483(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_537(ar_0, ar_2, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 6) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_70(ar_0, ar_1, ar_2, arityPad)) [ ar_2 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
(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_JMP_286) = -V_2 + V_3
Pol(main_LE_70) = V_1 - V_3
Pol(main_JMP_480) = -V_1 + V_2
Pol(main_Load_483) = -V_1 + V_2
Pol(main_LE_537) = -V_1 + V_3
Pol(main_Load_1) = V_1 - V_3
Pol(koat_start) = V_1 - V_3
orients all transitions weakly and the transitions
main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + ar_2, Cost: 8) main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_1, ar_2, ar_0 - 1, arityPad)) [ ar_1 <= ar_2 /\ ar_0 - 1 = i9' ]
(Comp: ?, Cost: 1) main_JMP_480(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_2, ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i10' /\ ar_2 < ar_1 ]
(Comp: ?, Cost: 2) main_Load_483(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_537(ar_0, ar_2, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ar_0 + ar_2, Cost: 6) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_70(ar_0, ar_1, ar_2, arityPad)) [ ar_2 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
(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_JMP_286) = V_1 - V_2
Pol(main_LE_70) = V_2 - V_3
Pol(main_JMP_480) = -V_1 + V_3
Pol(main_Load_483) = -V_1 + V_3
Pol(main_LE_537) = -V_1 + V_2
Pol(main_Load_1) = V_2 - V_3
Pol(koat_start) = V_2 - V_3
orients all transitions weakly and the transition
main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
strictly and produces the following problem:
4: T:
(Comp: ar_0 + ar_2, Cost: 8) main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_1, ar_2, ar_0 - 1, arityPad)) [ ar_1 <= ar_2 /\ ar_0 - 1 = i9' ]
(Comp: ?, Cost: 1) main_JMP_480(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_2, ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i10' /\ ar_2 < ar_1 ]
(Comp: ?, Cost: 2) main_Load_483(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_537(ar_0, ar_2, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ar_0 + ar_2, Cost: 6) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_70(ar_0, ar_1, ar_2, arityPad)) [ ar_2 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_1 + ar_2, Cost: 2) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
(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 4 produces the following problem:
5: T:
(Comp: ar_0 + ar_2, Cost: 8) main_JMP_286(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 < ar_2 /\ ar_0 <= ar_1 /\ ar_2 - 1 = i165' ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_286(ar_1, ar_2, ar_0 - 1, arityPad)) [ ar_1 <= ar_2 /\ ar_0 - 1 = i9' ]
(Comp: ar_1 + ar_2 + 1, Cost: 1) main_JMP_480(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 2) main_LE_70(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_2, ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i10' /\ ar_2 < ar_1 ]
(Comp: ar_0 + 2*ar_2 + ar_1 + 1, Cost: 2) main_Load_483(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_537(ar_0, ar_2, ar_1, arityPad)) [ 0 >= 0 ]
(Comp: ar_0 + ar_2, Cost: 6) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_483(ar_0, ar_2 - 1, ar_1, arityPad)) [ ar_2 - 1 = i220' /\ ar_0 < i220' /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_LE_70(ar_0, ar_1, ar_2, arityPad)) [ ar_2 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_1 + ar_2, Cost: 2) main_LE_537(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_JMP_480(ar_0, ar_2, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i225' ]
(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 16*ar_0 + 21*ar_2 + 5*ar_1 + 27

Time: 0.202 sec (SMT: 0.171 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) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 27 + 16 * |#0| + 5 * |#1| + 21 * |#2|)