time complexity proof of /tmp/tmp3VnqTg/PastaB11.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

        ↳11 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

↳30 JBCComplexityEdges

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

    ↳45 koat Proof (⇔, 53 ms)

    ↳46 BOUNDS(CONSTANT, 16 + 20 * |#0| + 20 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

public class PastaB11 {
    public static void main(int x, int y) {
        while (x + y > 0) {
            if (x > y) {
                x--;
            } else if (x == y) {
                x--;
            } else {
                y--;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 54 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 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.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 54 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_1124(i1, i4, i1, i4, env, static) :|: 0 >= 0
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{1,1}> main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1126(i1211, i4, i1274, i1265, i1266, env, static) :|: i1265 + i1266 = i1274
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{0,0}> main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) :|: 1 <= i1280
main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) -{1,1}> main_Load_1130(i1211, i4, i1265, i1266, env, static) :|: 1 <= i1280 && 0 < i1280
main_Load_1130(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1132(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Load_1132(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1134(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1135(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_LE_1134(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1136(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_LE_1135(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1137(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_Load_1136(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1138(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Inc_1137(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1139(i1211, i4, i1281, i1266, env, static) :|: i1265 + -1 = i1281
main_Load_1138(i1211, i4, i1265, i1266, env, static) -{1,1}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_JMP_1139(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1141(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1142(i1211, i4, i1265, i1266, env, static) :|: !(i1265 = i1266)
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1143(i1211, i4, i1266, env, static) :|: i1265 = i1266
main_Load_1141(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1144(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_NE_1142(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1145(i1211, i4, i1265, i1266, env, static) :|: i1265 < i1266
main_NE_1143(i1211, i4, i1266, env, static) -{1,1}> main_Inc_1146(i1211, i4, i1266, env, static) :|: i1266 = i1266
main_Load_1144(i1211, i4, i1281, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_Inc_1145(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1147(i1211, i4, i1265, i1286, env, static) :|: i1266 + -1 = i1286
main_Inc_1146(i1211, i4, i1266, env, static) -{1,1}> main_JMP_1148(i1211, i4, i1287, i1266, env, static) :|: i1266 + -1 = i1287
main_JMP_1147(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1149(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_JMP_1148(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1150(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1149(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1151(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1150(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1152(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1151(i1211, i4, i1265, i1286, env, static) -{0,0}> main_Load_1124(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1152(i1211, i4, i1287, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_1124(i1, i4, i1, i4, env, static) :|: 0 >= 0

obtained
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1274', i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
by chaining
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{1,1}> main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1126(i1211, i4, i1274, i1265, i1266, env, static) :|: i1265 + i1266 = i1274

obtained
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
by chaining
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{0,0}> main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) :|: 1 <= i1280
main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) -{1,1}> main_Load_1130(i1211, i4, i1265, i1266, env, static) :|: 1 <= i1280 && 0 < i1280
main_Load_1130(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1132(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Load_1132(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0

obtained
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
by chaining
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1135(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_LE_1135(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1137(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_Inc_1137(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1139(i1211, i4, i1281, i1266, env, static) :|: i1265 + -1 = i1281
main_JMP_1139(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1141(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_Load_1141(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1144(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_Load_1144(i1211, i4, i1281, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0

obtained
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
by chaining
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1134(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_LE_1134(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1136(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_Load_1136(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1138(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Load_1138(i1211, i4, i1265, i1266, env, static) -{1,1}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0

obtained
main_NE_1140(i1211, i4, i1265, i1265, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287'
by chaining
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1143(i1211, i4, i1266, env, static) :|: i1265 = i1266
main_NE_1143(i1211, i4, i1266, env, static) -{1,1}> main_Inc_1146(i1211, i4, i1266, env, static) :|: i1266 = i1266
main_Inc_1146(i1211, i4, i1266, env, static) -{1,1}> main_JMP_1148(i1211, i4, i1287, i1266, env, static) :|: i1266 + -1 = i1287
main_JMP_1148(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1150(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1150(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1152(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1152(i1211, i4, i1287, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0

obtained
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)
by chaining
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1142(i1211, i4, i1265, i1266, env, static) :|: !(i1265 = i1266)
main_NE_1142(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1145(i1211, i4, i1265, i1266, env, static) :|: i1265 < i1266
main_Inc_1145(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1147(i1211, i4, i1265, i1286, env, static) :|: i1266 + -1 = i1286
main_JMP_1147(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1149(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1149(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1151(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1151(i1211, i4, i1265, i1286, env, static) -{0,0}> main_Load_1124(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1274', i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1211, i4, i1265, i1265, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)

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

Linearized lhss.

main_NE_1140(i1211, i4, i1265, i1265, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287'
was transformed to
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265

(10) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1274', i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Removed div and mod.

main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)
was transformed to
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1274', i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266

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

Moved arithmethic from constraints to rhss.

main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1274', i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
was transformed to
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'

main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
was transformed to
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266

main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
was transformed to
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266

main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
was transformed to
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'

main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
was transformed to
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265

(14) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
was transformed to
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 < i1280 && 1 <= i1280

main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
was transformed to
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 - 1, env, static) :|: i1266 - 1 = i1286' && i1265 < i1266

main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
was transformed to
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 - 1, env, static) :|: i1265 < i1266 && i1266 - 1 = i1286' && i1266 < i1265

main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
was transformed to
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 - 1, i1265, env, static) :|: i1265 - 1 = i1287' && x = i1265

main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
was transformed to
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: i1265 + i1266 = i1274'

main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
was transformed to
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 - 1, i1266, env, static) :|: i1266 < i1265 && i1265 - 1 = i1281'

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

main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
was transformed to
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266

(16) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 < i1280 && 1 <= i1280
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 - 1, env, static) :|: i1266 - 1 = i1286' && i1265 < i1266
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: i1265 + i1266 = i1274'
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 - 1, i1265, env, static) :|: i1265 - 1 = i1287' && x = i1265
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 - 1, i1266, env, static) :|: i1266 < i1265 && i1265 - 1 = i1281'
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 - 1, env, static) :|: i1265 < i1266 && i1266 - 1 = i1286' && i1266 < i1265

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

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

(18) Obligation:

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

(20) Obligation:

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

Linearized lhss.

(22) Obligation:

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

Removed div and mod.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{2,2}> main_LE_1126(i1211, i4, i1265 + i1266, i1265, i1266, env, static) :|: 0 >= 0 && i1265 + i1266 = i1274'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1266 + -1, env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{3,3}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 0 < i1280 && 1 <= i1280
main_NE_1140(i1211, i4, i1265, x, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265 + -1, i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1126(i1211, i4, i1279, i1265, i1266, env, static) -{0,0}> main_LE_1127(i1211, i4, i1279, i1265, i1266, env, static) :|: i1279 <= 0
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

(28) Obligation:

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

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

(30) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 53 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_4(i1, i4, env, static) :|: 0 >= 0
main_Load_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_10(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_12(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_1124(i1, i4, i1, i4, env, static) :|: 0 >= 0
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{1,1}> main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1126(i1211, i4, i1274, i1265, i1266, env, static) :|: i1265 + i1266 = i1274
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{0,0}> main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) :|: 1 <= i1280
main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) -{1,1}> main_Load_1130(i1211, i4, i1265, i1266, env, static) :|: 1 <= i1280 && 0 < i1280
main_Load_1130(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1132(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Load_1132(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1134(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{0,0}> main_LE_1135(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_LE_1134(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1136(i1211, i4, i1265, i1266, env, static) :|: i1265 <= i1266
main_LE_1135(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1137(i1211, i4, i1265, i1266, env, static) :|: i1266 < i1265
main_Load_1136(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1138(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Inc_1137(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1139(i1211, i4, i1281, i1266, env, static) :|: i1265 + -1 = i1281
main_Load_1138(i1211, i4, i1265, i1266, env, static) -{1,1}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_JMP_1139(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1141(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1142(i1211, i4, i1265, i1266, env, static) :|: !(i1265 = i1266)
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{0,0}> main_NE_1143(i1211, i4, i1266, env, static) :|: i1265 = i1266
main_Load_1141(i1211, i4, i1281, i1266, env, static) -{1,1}> main_Load_1144(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_NE_1142(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Inc_1145(i1211, i4, i1265, i1266, env, static) :|: i1265 < i1266
main_NE_1143(i1211, i4, i1266, env, static) -{1,1}> main_Inc_1146(i1211, i4, i1266, env, static) :|: i1266 = i1266
main_Load_1144(i1211, i4, i1281, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1281, i1266, env, static) :|: 0 >= 0
main_Inc_1145(i1211, i4, i1265, i1266, env, static) -{1,1}> main_JMP_1147(i1211, i4, i1265, i1286, env, static) :|: i1266 + -1 = i1286
main_Inc_1146(i1211, i4, i1266, env, static) -{1,1}> main_JMP_1148(i1211, i4, i1287, i1266, env, static) :|: i1266 + -1 = i1287
main_JMP_1147(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1149(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_JMP_1148(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1150(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1149(i1211, i4, i1265, i1286, env, static) -{1,1}> main_Load_1151(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1150(i1211, i4, i1287, i1266, env, static) -{1,1}> main_Load_1152(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0
main_Load_1151(i1211, i4, i1265, i1286, env, static) -{0,0}> main_Load_1124(i1211, i4, i1265, i1286, env, static) :|: 0 >= 0
main_Load_1152(i1211, i4, i1287, i1266, env, static) -{0,0}> main_Load_1124(i1211, i4, i1287, i1266, env, static) :|: 0 >= 0

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

obtained
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{5,5}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
by chaining
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{1,1}> main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_IntArithmetic_1125(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1126(i1211, i4, i1274, i1265, i1266, env, static) :|: i1265 + i1266 = i1274
main_LE_1126(i1211, i4, i1280, i1265, i1266, env, static) -{0,0}> main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) :|: 1 <= i1280
main_LE_1128(i1211, i4, i1280, i1265, i1266, env, static) -{1,1}> main_Load_1130(i1211, i4, i1265, i1266, env, static) :|: 1 <= i1280 && 0 < i1280
main_Load_1130(i1211, i4, i1265, i1266, env, static) -{1,1}> main_Load_1132(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0
main_Load_1132(i1211, i4, i1265, i1266, env, static) -{1,1}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0

(34) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_1124(i1, i4, i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_1124(i1211, i4, i1265, i1266, env, static) -{5,5}> main_LE_1133(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1281', i1266, env, static) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1133(i1211, i4, i1265, i1266, env, static) -{3,3}> main_NE_1140(i1211, i4, i1265, i1266, env, static) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1211, i4, i1265, i1265, env, static) -{4,4}> main_Load_1124(i1211, i4, i1287', i1265, env, static) :|: 0 >= 0 && i1265 + -1 = i1287'
main_NE_1140(i1211, i4, i1265, i1266, env, static) -{4,4}> main_Load_1124(i1211, i4, i1265, i1286', env, static) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_Load_1124(x1, x2, x3, x4, x5, x6) → main_Load_1124(x3, x4)
main_LE_1133(x1, x2, x3, x4, x5, x6) → main_LE_1133(x3, x4)
main_NE_1140(x1, x2, x3, x4, x5, x6) → main_NE_1140(x3, x4)

(36) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, static) -{16,16}> main_Load_1124(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1281', i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1265, i1265) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287'
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)

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

Linearized lhss.

main_NE_1140(i1265, i1265) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287'
was transformed to
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265

(38) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1281', i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_Load_2(i1, i4, static) -{16,16}> main_Load_1124(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Removed div and mod.

main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && !(i1265 = i1266)
was transformed to
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266

(40) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1281', i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
main_Load_2(i1, i4, static) -{16,16}> main_Load_1124(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1

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

Moved arithmethic from constraints to rhss.

main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
was transformed to
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266

main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1287', i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
was transformed to
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1265 + -1, i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265

main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1281', i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
was transformed to
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1265 + -1, i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'

main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1286') :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
was transformed to
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266

(42) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: 0 >= 0 && i1265 <= i1266
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1265 + -1, i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1265 + -1, i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
main_Load_2(i1, i4, static) -{16,16}> main_Load_1124(i1, i4) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266

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

Simplified expressions.

main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: 0 >= 0 && i1265 <= i1266
was transformed to
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: i1265 <= i1266

main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 0 >= 0 && 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
was transformed to
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'

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

main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1265 + -1, i1266) :|: 0 >= 0 && i1266 < i1265 && i1265 + -1 = i1281'
was transformed to
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1265 - 1, i1266) :|: i1266 < i1265 && i1265 - 1 = i1281'

main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 > i1266
was transformed to
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 - 1) :|: i1265 < i1266 && i1266 - 1 = i1286' && i1266 < i1265

main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 + -1) :|: 0 >= 0 && i1265 < i1266 && i1266 + -1 = i1286' && i1265 < i1266
was transformed to
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 - 1) :|: i1266 - 1 = i1286' && i1265 < i1266

main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1265 + -1, i1265) :|: 0 >= 0 && i1265 + -1 = i1287' && x = i1265
was transformed to
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1265 - 1, i1265) :|: i1265 - 1 = i1287' && x = i1265

(44) Obligation:

IntTrs with 7 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 - 1) :|: i1265 < i1266 && i1266 - 1 = i1286' && i1266 < i1265
main_NE_1140(i1265, i1266) -{4,4}> main_Load_1124(i1265, i1266 - 1) :|: i1266 - 1 = i1286' && i1265 < i1266
main_Load_2(i1, i4, static) -{16,16}> main_Load_1124(i1, i4) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_Load_1124(i1265, i1266) -{5,5}> main_LE_1133(i1265, i1266) :|: 1 <= i1274' && i1265 + i1266 = i1274' && 0 < i1274'
main_LE_1133(i1265, i1266) -{4,4}> main_Load_1124(i1265 - 1, i1266) :|: i1266 < i1265 && i1265 - 1 = i1281'
main_NE_1140(i1265, x) -{4,4}> main_Load_1124(i1265 - 1, i1265) :|: i1265 - 1 = i1287' && x = i1265
main_LE_1133(i1265, i1266) -{3,3}> main_NE_1140(i1265, i1266) :|: i1265 <= i1266

(45) koat Proof (EQUIVALENT transformation)

YES(?, 20*ar_0 + 20*ar_1 + 16)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i1286' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i1286' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 5) main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
(Comp: ?, Cost: 4) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 1 = i1281' ]
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_0, arityPad)) [ ar_0 - 1 = i1287' /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_NE_1140(ar_0, ar_1, arityPad)) [ ar_0 <= ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_0 < ar_1 /\ ar_1 - 1 = i1286' /\ ar_1 < ar_0 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_0, arityPad)) [ ar_0 - 1 = i1287' /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i1286' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 3) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_NE_1140(ar_0, ar_1, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 4) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 1 = i1281' ]
(Comp: ?, Cost: 5) main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_0, arityPad)) [ ar_0 - 1 = i1287' /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i1286' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 3) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_NE_1140(ar_0, ar_1, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 4) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 1 = i1281' ]
(Comp: ?, Cost: 5) main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_NE_1140) = V_1 + V_2 - 1
Pol(main_Load_1124) = V_1 + V_2
Pol(main_LE_1133) = V_1 + V_2 - 1
Pol(main_Load_2) = V_1 + V_2
Pol(koat_start) = V_1 + V_2
orients all transitions weakly and the transition
main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
strictly and produces the following problem:
4: T:
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_0, arityPad)) [ ar_0 - 1 = i1287' /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i1286' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 3) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_NE_1140(ar_0, ar_1, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ?, Cost: 4) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 1 = i1281' ]
(Comp: ar_0 + ar_1, Cost: 5) main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 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_1, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_0, arityPad)) [ ar_0 - 1 = i1287' /\ ar_1 = ar_0 ]
(Comp: ar_0 + ar_1, Cost: 4) main_NE_1140(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1 - 1, arityPad)) [ ar_1 - 1 = i1286' /\ ar_0 < ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_NE_1140(ar_0, ar_1, arityPad)) [ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 4) main_LE_1133(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0 - 1, ar_1, arityPad)) [ ar_1 < ar_0 /\ ar_0 - 1 = i1281' ]
(Comp: ar_0 + ar_1, Cost: 5) main_Load_1124(ar_0, ar_1, ar_2) -> Com_1(main_LE_1133(ar_0, ar_1, arityPad)) [ 1 <= i1274' /\ ar_0 + ar_1 = i1274' /\ 0 < i1274' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_1124(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 20*ar_0 + 20*ar_1 + 16

Time: 0.096 sec (SMT: 0.087 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

(45) koat Proof (EQUIVALENT transformation)

(46) BOUNDS(CONSTANT, 16 + 20 * |#0| + 20 * |#1|)