time complexity proof of /tmp/tmpNK4o1M/PastaB13.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 19 + 8 * |#0| + 14 * |#1| + 22 * |#2|).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 0 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 15 ms)

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 32 ms)

    ↳16 BOUNDS(CONSTANT, 17 + 8 * |#0| + 14 * |#1| + 22 * |#2|)

↳17 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 0 ms)

↳18 JBCComplexityEdges

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 95 ms)

    ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 3 ms)

        ↳26 WeightedIntTrs

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 53 ms)

    ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

(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 PastaB13 {
    public static void main(int x, int y, int z) {
        while (x > z || y > z) {
            if (x > z) {
                x--;
            } else if (y > z) {
                y--;
            } else {
                continue;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 54 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, env, static) -{0,0}> main_Load_3(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_3(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{0,0}> main_Load_704(i2, i3, i5, i2, i3, env, static) :|: 0 >= 0
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_706(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_707(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_GT_706(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_708(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_GT_707(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_709(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_708(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_710(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_709(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_711(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_710(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_712(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_711(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_712(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_714(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_716(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_714(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Inc_717(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_LE_716(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Load_719(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_717(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_720(i2, i3, i5, i356, i349, env, static) :|: i348 + -1 = i356
main_Load_719(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_722(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_JMP_720(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_723(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_Load_722(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_724(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_723(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_725(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_LE_724(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_726(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_725(i2, i3, i5, i356, i349, env, static) -{0,0}> main_Load_704(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_LE_726(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_727(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_727(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_728(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_728(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_729(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_729(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_730(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_730(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Inc_731(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_731(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_732(i2, i3, i5, i348, i360, env, static) :|: i349 + -1 = i360
main_JMP_732(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_733(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_733(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_734(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_734(i2, i3, i5, i348, i360, env, static) -{0,0}> main_Load_704(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0

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

obtained
main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, 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(i2, i3, i5, env, static) -{0,0}> main_Load_3(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_3(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{0,0}> main_Load_704(i2, i3, i5, i2, i3, env, static) :|: 0 >= 0

obtained
main_GT_705(i2, i3, i5, i348, i349, env, static) -{13,13}> main_Load_704(i2, i3, i5, i348, i360', env, static) :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
by chaining
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_707(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_GT_707(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_709(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_709(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_711(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_711(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_716(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_716(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Load_719(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Load_719(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_722(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_722(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_724(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_724(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_726(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_LE_726(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_727(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_727(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_728(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_728(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_729(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_729(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_730(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_730(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Inc_731(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_731(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_732(i2, i3, i5, i348, i360, env, static) :|: i349 + -1 = i360
main_JMP_732(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_733(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_733(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_734(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_734(i2, i3, i5, i348, i360, env, static) -{0,0}> main_Load_704(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0

obtained
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i356', i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
by chaining
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_706(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_GT_706(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_708(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_Load_708(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_710(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_710(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_712(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_712(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_714(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_LE_714(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Inc_717(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_Inc_717(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_720(i2, i3, i5, i356, i349, env, static) :|: i348 + -1 = i356
main_JMP_720(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_723(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_Load_723(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_725(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_Load_725(i2, i3, i5, i356, i349, env, static) -{0,0}> main_Load_704(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_GT_705(i2, i3, i5, i348, i349, env, static) -{13,13}> main_Load_704(i2, i3, i5, i348, i360', env, static) :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i356', i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348

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

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

main_Load_1(x1, x2, x3, x4, x5) → main_Load_1(x1, x2, x3, x5)
main_GT_705(x1, x2, x3, x4, x5, x6, x7) → main_GT_705(x3, x4, x5)
main_Load_704(x1, x2, x3, x4, x5, x6, x7) → main_Load_704(x3, x4, x5)

(10) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i3, i5, static) -{16,16}> main_Load_704(i5, i2, i3) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_704(i5, i348, i349) -{1,1}> main_GT_705(i5, i348, i349) :|: 0 >= 0
main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i360') :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i356', i349) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348

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

Moved arithmethic from constraints to rhss.

main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i360') :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
was transformed to
main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i349 + -1) :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'

main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i356', i349) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
was transformed to
main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i348 + -1, i349) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348

(12) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i349 + -1) :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
main_Load_704(i5, i348, i349) -{1,1}> main_GT_705(i5, i348, i349) :|: 0 >= 0
main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i348 + -1, i349) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
main_Load_1(i2, i3, i5, static) -{16,16}> main_Load_704(i5, i2, i3) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i348 + -1, i349) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
was transformed to
main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i348 - 1, i349) :|: i348 - 1 = i356' && i5 < i348

main_Load_1(i2, i3, i5, static) -{16,16}> main_Load_704(i5, i2, i3) :|: 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(i2, i3, i5, static) -{16,16}> main_Load_704(i5, i2, i3) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i349 + -1) :|: 0 >= 0 && i348 <= i5 && i5 < i349 && i349 + -1 = i360'
was transformed to
main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i349 - 1) :|: i348 <= i5 && i5 < i349 && i349 - 1 = i360'

(14) Obligation:

IntTrs with 4 rules
Start term: main_Load_1(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GT_705(i5, i348, i349) -{13,13}> main_Load_704(i5, i348, i349 - 1) :|: i348 <= i5 && i5 < i349 && i349 - 1 = i360'
main_GT_705(i5, i348, i349) -{7,7}> main_Load_704(i5, i348 - 1, i349) :|: i348 - 1 = i356' && i5 < i348
main_Load_704(i5, i348, i349) -{1,1}> main_GT_705(i5, i348, i349) :|: 0 >= 0
main_Load_1(i2, i3, i5, static) -{16,16}> main_Load_704(i5, i2, i3) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(15) koat Proof (EQUIVALENT transformation)

YES(?, 14*ar_1 + 22*ar_2 + 8*ar_0 + 17)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 13) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
(Comp: ?, Cost: 7) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 1) main_Load_704(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GT_705(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: ?, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_2, ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 13) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
(Comp: ?, Cost: 7) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 1) main_Load_704(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GT_705(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_2, ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_GT_705) = -V_1 + V_3
Pol(main_Load_704) = -V_1 + V_3
Pol(main_Load_1) = V_2 - V_3
Pol(koat_start) = V_2 - V_3
orients all transitions weakly and the transition
main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
strictly and produces the following problem:
3: T:
(Comp: ar_1 + ar_2, Cost: 13) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
(Comp: ?, Cost: 7) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 1) main_Load_704(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GT_705(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_2, ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_GT_705) = -V_1 + V_2
Pol(main_Load_704) = -V_1 + V_2
Pol(main_Load_1) = V_1 - V_3
Pol(koat_start) = V_1 - V_3
orients all transitions weakly and the transition
main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: ar_1 + ar_2, Cost: 13) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
(Comp: ar_0 + ar_2, Cost: 7) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 1) main_Load_704(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GT_705(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_2, ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: ar_1 + ar_2, Cost: 13) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1, ar_2 - 1, arityPad)) [ ar_1 <= ar_0 /\ ar_0 < ar_2 /\ ar_2 - 1 = i360' ]
(Comp: ar_0 + ar_2, Cost: 7) main_GT_705(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_0, ar_1 - 1, ar_2, arityPad)) [ ar_1 - 1 = i356' /\ ar_0 < ar_1 ]
(Comp: ar_0 + 2*ar_2 + ar_1 + 1, Cost: 1) main_Load_704(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GT_705(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 16) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_704(ar_2, ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 14*ar_1 + 22*ar_2 + 8*ar_0 + 17

Time: 0.078 sec (SMT: 0.068 sec)

(16) BOUNDS(CONSTANT, 17 + 8 * |#0| + 14 * |#1| + 22 * |#2|)

(17) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

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

(18) Obligation:

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

(19) 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.
Did no encode lower bounds for putfield and astore.

(20) Obligation:

IntTrs with 55 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(i2, i3, i5, env, static) -{0,0}> main_Load_3(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_3(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, i5, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, i5, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, i5, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, i5, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, i5, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, i5, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, i5, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, i5, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, i5, env, static) -{1,1}> main_Load_46(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_46(i2, i3, i5, env, static) -{0,0}> main_Load_47(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_47(i2, i3, i5, env, static) -{0,0}> main_Load_48(i2, i3, i5, env, static) :|: 0 <= static
main_Load_48(i2, i3, i5, env, static) -{0,0}> main_Load_49(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_49(i2, i3, i5, env, static) -{0,0}> main_Load_50(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_50(i2, i3, i5, env, static) -{1,1}> main_Load_51(i2, i3, i5, env, static) :|: 0 >= 0
main_Load_51(i2, i3, i5, env, static) -{0,0}> main_Load_704(i2, i3, i5, i2, i3, env, static) :|: 0 >= 0
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_706(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_707(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_GT_706(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_708(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_GT_707(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_709(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_708(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_710(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_709(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_711(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_710(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_712(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_711(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_712(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_714(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_715(i2, i3, i5, i349, i348, env, static) :|: i349 <= i5
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_716(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_714(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Inc_717(i2, i3, i5, i348, i349, env, static) :|: i5 < i348
main_LE_716(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Load_719(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_717(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_720(i2, i3, i5, i356, i349, env, static) :|: i348 + -1 = i356
main_Load_719(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_722(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_JMP_720(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_723(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_Load_722(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_724(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_723(i2, i3, i5, i356, i349, env, static) -{1,1}> main_Load_725(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_LE_724(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_726(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_725(i2, i3, i5, i356, i349, env, static) -{0,0}> main_Load_704(i2, i3, i5, i356, i349, env, static) :|: 0 >= 0
main_LE_726(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_727(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_727(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_728(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_728(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_729(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_729(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_730(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_730(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Inc_731(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_731(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_732(i2, i3, i5, i348, i360, env, static) :|: i349 + -1 = i360
main_JMP_732(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_733(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_733(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_734(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_734(i2, i3, i5, i348, i360, env, static) -{0,0}> main_Load_704(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0

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

obtained
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0 && i348 <= i5
by chaining
main_GT_705(i2, i3, i5, i348, i349, env, static) -{0,0}> main_GT_707(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_GT_707(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_709(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_709(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_711(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_711(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0

obtained
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i360', env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5
by chaining
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_716(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_716(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Load_719(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Load_719(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_722(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_Load_722(i2, i3, i5, i348, i349, env, static) -{1,1}> main_LE_724(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_724(i2, i3, i5, i348, i349, env, static) -{0,0}> main_LE_726(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_LE_726(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_727(i2, i3, i5, i348, i349, env, static) :|: i348 <= i5
main_Load_727(i2, i3, i5, i348, i349, env, static) -{1,1}> main_Load_728(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_Load_728(i2, i3, i5, i349, i348, env, static) -{1,1}> main_LE_729(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0
main_LE_729(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_730(i2, i3, i5, i349, i348, env, static) :|: i5 < i349
main_LE_730(i2, i3, i5, i349, i348, env, static) -{1,1}> main_Inc_731(i2, i3, i5, i348, i349, env, static) :|: i5 < i349
main_Inc_731(i2, i3, i5, i348, i349, env, static) -{1,1}> main_JMP_732(i2, i3, i5, i348, i360, env, static) :|: i349 + -1 = i360
main_JMP_732(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_733(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_733(i2, i3, i5, i348, i360, env, static) -{1,1}> main_Load_734(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0
main_Load_734(i2, i3, i5, i348, i360, env, static) -{0,0}> main_Load_704(i2, i3, i5, i348, i360, env, static) :|: 0 >= 0

(22) Obligation:

IntTrs with 6 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(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0 && i348 <= i5
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_715(i2, i3, i5, i349, i348, env, static) :|: i349 <= i5
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i360', env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i356', i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348

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

Moved arithmethic from constraints to rhss.

main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i356', i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
was transformed to
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 + -1, i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348

main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i360', env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5
was transformed to
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 + -1, env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5

(24) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_715(i2, i3, i5, i349, i348, env, static) :|: i349 <= i5
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0 && i348 <= i5
main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, 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_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 + -1, i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 + -1, env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5

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

Simplified expressions.

main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 + -1, env, static) :|: 0 >= 0 && i5 < i349 && i349 + -1 = i360' && i348 <= i5
was transformed to
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 - 1, env, static) :|: i5 < i349 && i349 - 1 = i360' && i348 <= i5

main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 + -1, i349, env, static) :|: 0 >= 0 && i348 + -1 = i356' && i5 < i348
was transformed to
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 - 1, i349, env, static) :|: i348 - 1 = i356' && i5 < i348

main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: 0 >= 0 && i348 <= i5
was transformed to
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: i348 <= i5

main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, 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(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(26) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_715(i2, i3, i5, i349, i348, env, static) :|: i349 <= i5
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: i348 <= i5
main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 - 1, i349, env, static) :|: i348 - 1 = i356' && i5 < i348
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 - 1, env, static) :|: i5 < i349 && i349 - 1 = i360' && i348 <= i5

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

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

(28) Obligation:

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

(30) Obligation:

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

Moved arithmethic from constraints to rhss.

(32) Obligation:

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

Simplified expressions.

(34) Obligation:

IntTrs with 6 rules
Start term: main_Load_1(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_704(i2, i3, i5, i348, i349, env, static) -{1,1}> main_GT_705(i2, i3, i5, i348, i349, env, static) :|: 0 >= 0
main_LE_713(i2, i3, i5, i349, i348, env, static) -{0,0}> main_LE_715(i2, i3, i5, i349, i348, env, static) :|: i349 <= i5
main_GT_705(i2, i3, i5, i348, i349, env, static) -{3,3}> main_LE_713(i2, i3, i5, i349, i348, env, static) :|: i348 <= i5
main_Load_1(i2, i3, i5, env, static) -{16,16}> main_Load_704(i2, i3, i5, i2, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_705(i2, i3, i5, i348, i349, env, static) -{7,7}> main_Load_704(i2, i3, i5, i348 - 1, i349, env, static) :|: i348 - 1 = i356' && i5 < i348
main_LE_713(i2, i3, i5, i349, i348, env, static) -{10,10}> main_Load_704(i2, i3, i5, i348, i349 - 1, env, static) :|: i5 < i349 && i349 - 1 = i360' && i348 <= i5