time complexity proof of /tmp/tmpwRbRIX/PastaC3.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 11 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

↳21 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 8 ms)

↳22 JBCComplexityEdges

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

    ↳24 WeightedIntTrs

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

    ↳26 WeightedIntTrs

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

    ↳33 koat Proof (⇔, 162 ms)

    ↳34 BOUNDS(CONSTANT, 20 + 8 * |#0| + 16 * |#1| + 8 * |#2|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

public class PastaC3 {
    public static void main(int x, int y, int z) {
        while (x < y) {
            if (x < z) {
                x++;
            } else {
                z++;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

(6) Obligation:

IntTrs with 49 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, i6, env, static) -{0,0}> main_Load_4(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, i6, env, static) -{1,1}> main_Load_46(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i2, i4, i6, env, static) -{0,0}> main_Load_47(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i2, i4, i6, env, static) -{0,0}> main_Load_48(i2, i4, i6, env, static) :|: 0 <= static
main_Load_48(i2, i4, i6, env, static) -{0,0}> main_Load_49(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i2, i4, i6, env, static) -{0,0}> main_Load_50(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i2, i4, i6, env, static) -{1,1}> main_Load_51(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i2, i4, i6, env, static) -{1,1}> main_GE_55(i2, i4, i6, env, static) :|: 0 >= 0
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_56(i2, i4, i6, env, static) :|: i4 <= i2
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_57(i2, i4, i6, env, static) :|: i2 < i4
main_GE_57(i2, i4, i6, env, static) -{1,1}> main_Load_63(i2, i4, i6, env, static) :|: i2 < i4
main_Load_63(i2, i4, i6, env, static) -{0,0}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: 0 >= 0
main_Load_607(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Load_611(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_Load_611(i2, i4, i6, i221, i222, env, static) -{1,1}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_618(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_619(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_GE_618(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_621(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_GE_619(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_627(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_Inc_621(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_628(i2, i4, i6, i221, i231, env, static) :|: i222 + 1 = i231
main_Inc_627(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_629(i2, i4, i6, i232, i222, env, static) :|: i221 + 1 = i232
main_JMP_628(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_631(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_JMP_629(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_636(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_631(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_638(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_636(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_643(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_638(i2, i4, i6, i221, i231, env, static) -{1,1}> main_GE_649(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_643(i2, i4, i6, i232, i222, env, static) -{1,1}> main_GE_663(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_GE_649(i2, i4, i6, i221, i231, env, static) -{0,0}> main_GE_664(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_GE_663(i2, i4, i6, i232, i222, env, static) -{0,0}> main_GE_664(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_665(i2, i4, i6, i257, i258, env, static) :|: i4 <= i257
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_666(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_GE_666(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_668(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_Load_668(i2, i4, i6, i257, i258, env, static) -{0,0}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, i6, env, static) -{17,17}> main_GE_55(i2, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, i4, i6, env, static) -{0,0}> main_Load_4(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, i6, env, static) -{1,1}> main_Load_46(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i2, i4, i6, env, static) -{0,0}> main_Load_47(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i2, i4, i6, env, static) -{0,0}> main_Load_48(i2, i4, i6, env, static) :|: 0 <= static
main_Load_48(i2, i4, i6, env, static) -{0,0}> main_Load_49(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i2, i4, i6, env, static) -{0,0}> main_Load_50(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i2, i4, i6, env, static) -{1,1}> main_Load_51(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i2, i4, i6, env, static) -{1,1}> main_GE_55(i2, i4, i6, env, static) :|: 0 >= 0

obtained
main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4 && 0 >= 0
by chaining
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_57(i2, i4, i6, env, static) :|: i2 < i4
main_GE_57(i2, i4, i6, env, static) -{1,1}> main_Load_63(i2, i4, i6, env, static) :|: i2 < i4
main_Load_63(i2, i4, i6, env, static) -{0,0}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: 0 >= 0

obtained
main_Load_607(i2, i4, i6, i221, i222, env, static) -{2,2}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
by chaining
main_Load_607(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Load_611(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_Load_611(i2, i4, i6, i221, i222, env, static) -{1,1}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0

obtained
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i232', i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
by chaining
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_619(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_GE_619(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_627(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_Inc_627(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_629(i2, i4, i6, i232, i222, env, static) :|: i221 + 1 = i232
main_JMP_629(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_636(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_636(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_643(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_643(i2, i4, i6, i232, i222, env, static) -{1,1}> main_GE_663(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_GE_663(i2, i4, i6, i232, i222, env, static) -{0,0}> main_GE_664(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0

obtained
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4 && 0 >= 0
by chaining
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_666(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_GE_666(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_668(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_Load_668(i2, i4, i6, i257, i258, env, static) -{0,0}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: 0 >= 0

obtained
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i231', env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
by chaining
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_618(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_GE_618(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_621(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_Inc_621(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_628(i2, i4, i6, i221, i231, env, static) :|: i222 + 1 = i231
main_JMP_628(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_631(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_631(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_638(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_638(i2, i4, i6, i221, i231, env, static) -{1,1}> main_GE_649(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_GE_649(i2, i4, i6, i221, i231, env, static) -{0,0}> main_GE_664(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, i6, env, static) -{17,17}> main_GE_55(i2, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_56(i2, i4, i6, env, static) :|: i4 <= i2
main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4 && 0 >= 0
main_Load_607(i2, i4, i6, i221, i222, env, static) -{2,2}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i232', i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_665(i2, i4, i6, i257, i258, env, static) :|: i4 <= i257
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4 && 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i231', env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221

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

Moved arithmethic from constraints to rhss.

main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i231', env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
was transformed to
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i222 + 1, env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221

main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i232', i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
was transformed to
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221 + 1, i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222

(10) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4 && 0 >= 0
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_665(i2, i4, i6, i257, i258, env, static) :|: i4 <= i257
main_Load_607(i2, i4, i6, i221, i222, env, static) -{2,2}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_Load_2(i2, i4, i6, env, static) -{17,17}> main_GE_55(i2, i4, i6, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_56(i2, i4, i6, env, static) :|: i4 <= i2
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i222 + 1, env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4 && 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221 + 1, i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222

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

Simplified expressions.

main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4 && 0 >= 0
was transformed to
main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4

main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221 + 1, i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
was transformed to
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221 + 1, i222, env, static) :|: i221 + 1 = i232' && i221 < i222

main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i222 + 1, env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
was transformed to
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i222 + 1, env, static) :|: i222 + 1 = i231' && i222 <= i221

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

main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4 && 0 >= 0
was transformed to
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4

(12) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_665(i2, i4, i6, i257, i258, env, static) :|: i4 <= i257
main_Load_607(i2, i4, i6, i221, i222, env, static) -{2,2}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_GE_55(i2, i4, i6, env, static) -{1,1}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: i2 < i4
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_56(i2, i4, i6, env, static) :|: i4 <= i2
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i222 + 1, env, static) :|: i222 + 1 = i231' && i222 <= i221
main_Load_2(i2, i4, i6, env, static) -{17,17}> main_GE_55(i2, i4, i6, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221 + 1, i222, env, static) :|: i221 + 1 = i232' && i221 < i222

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

Transformed 49 jbc graph edges to a weighted ITS with 49 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(14) Obligation:

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

(16) Obligation:

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

Moved arithmethic from constraints to rhss.

(18) Obligation:

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

Simplified expressions.

(20) Obligation:

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

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

(22) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 47 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, i6, env, static) -{0,0}> main_Load_4(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, i6, env, static) -{1,1}> main_Load_46(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i2, i4, i6, env, static) -{0,0}> main_Load_47(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i2, i4, i6, env, static) -{0,0}> main_Load_48(i2, i4, i6, env, static) :|: 0 <= static
main_Load_48(i2, i4, i6, env, static) -{0,0}> main_Load_49(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i2, i4, i6, env, static) -{0,0}> main_Load_50(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i2, i4, i6, env, static) -{1,1}> main_Load_51(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i2, i4, i6, env, static) -{1,1}> main_GE_55(i2, i4, i6, env, static) :|: 0 >= 0
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_57(i2, i4, i6, env, static) :|: i2 < i4
main_GE_57(i2, i4, i6, env, static) -{1,1}> main_Load_63(i2, i4, i6, env, static) :|: i2 < i4
main_Load_63(i2, i4, i6, env, static) -{0,0}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: 0 >= 0
main_Load_607(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Load_611(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_Load_611(i2, i4, i6, i221, i222, env, static) -{1,1}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_618(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_GE_615(i2, i4, i6, i221, i222, env, static) -{0,0}> main_GE_619(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_GE_618(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_621(i2, i4, i6, i221, i222, env, static) :|: i222 <= i221
main_GE_619(i2, i4, i6, i221, i222, env, static) -{1,1}> main_Inc_627(i2, i4, i6, i221, i222, env, static) :|: i221 < i222
main_Inc_621(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_628(i2, i4, i6, i221, i231, env, static) :|: i222 + 1 = i231
main_Inc_627(i2, i4, i6, i221, i222, env, static) -{1,1}> main_JMP_629(i2, i4, i6, i232, i222, env, static) :|: i221 + 1 = i232
main_JMP_628(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_631(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_JMP_629(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_636(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_631(i2, i4, i6, i221, i231, env, static) -{1,1}> main_Load_638(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_636(i2, i4, i6, i232, i222, env, static) -{1,1}> main_Load_643(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_Load_638(i2, i4, i6, i221, i231, env, static) -{1,1}> main_GE_649(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_Load_643(i2, i4, i6, i232, i222, env, static) -{1,1}> main_GE_663(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_GE_649(i2, i4, i6, i221, i231, env, static) -{0,0}> main_GE_664(i2, i4, i6, i221, i231, env, static) :|: 0 >= 0
main_GE_663(i2, i4, i6, i232, i222, env, static) -{0,0}> main_GE_664(i2, i4, i6, i232, i222, env, static) :|: 0 >= 0
main_GE_664(i2, i4, i6, i257, i258, env, static) -{0,0}> main_GE_666(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_GE_666(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_668(i2, i4, i6, i257, i258, env, static) :|: i257 < i4
main_Load_668(i2, i4, i6, i257, i258, env, static) -{0,0}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, i6, env, static) -{18,18}> main_Load_607(i2, i4, i6, i2, i6, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i2 < i4 && 0 < 2
by chaining
main_Load_2(i2, i4, i6, env, static) -{0,0}> main_Load_4(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_4(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, i6, env, static) -{1,1}> main_Load_46(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_46(i2, i4, i6, env, static) -{0,0}> main_Load_47(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_47(i2, i4, i6, env, static) -{0,0}> main_Load_48(i2, i4, i6, env, static) :|: 0 <= static
main_Load_48(i2, i4, i6, env, static) -{0,0}> main_Load_49(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i2, i4, i6, env, static) -{0,0}> main_Load_50(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_50(i2, i4, i6, env, static) -{1,1}> main_Load_51(i2, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i2, i4, i6, env, static) -{1,1}> main_GE_55(i2, i4, i6, env, static) :|: 0 >= 0
main_GE_55(i2, i4, i6, env, static) -{0,0}> main_GE_57(i2, i4, i6, env, static) :|: i2 < i4
main_GE_57(i2, i4, i6, env, static) -{1,1}> main_Load_63(i2, i4, i6, env, static) :|: i2 < i4
main_Load_63(i2, i4, i6, env, static) -{0,0}> main_Load_607(i2, i4, i6, i2, i6, env, static) :|: 0 >= 0

(26) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, i6, env, static) -{18,18}> main_Load_607(i2, i4, i6, i2, i6, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i2 < i4 && 0 < 2
main_Load_607(i2, i4, i6, i221, i222, env, static) -{2,2}> main_GE_615(i2, i4, i6, i221, i222, env, static) :|: 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i232', i222, env, static) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
main_GE_664(i2, i4, i6, i257, i258, env, static) -{1,1}> main_Load_607(i2, i4, i6, i257, i258, env, static) :|: i257 < i4 && 0 >= 0
main_GE_615(i2, i4, i6, i221, i222, env, static) -{5,5}> main_GE_664(i2, i4, i6, i221, i231', env, static) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221

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

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

main_Load_2(x1, x2, x3, x4, x5) → main_Load_2(x1, x2, x3, x5)
main_GE_615(x1, x2, x3, x4, x5, x6, x7) → main_GE_615(x2, x4, x5)
main_GE_664(x1, x2, x3, x4, x5, x6, x7) → main_GE_664(x2, x4, x5)
main_Load_607(x1, x2, x3, x4, x5, x6, x7) → main_Load_607(x2, x4, x5)

(28) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, i6, static) -{18,18}> main_Load_607(i4, i2, i6) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i2 < i4 && 0 < 2
main_Load_607(i4, i221, i222) -{2,2}> main_GE_615(i4, i221, i222) :|: 0 >= 0
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i232', i222) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
main_GE_664(i4, i257, i258) -{1,1}> main_Load_607(i4, i257, i258) :|: i257 < i4 && 0 >= 0
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i231') :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221

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

Moved arithmethic from constraints to rhss.

main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i231') :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
was transformed to
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i222 + 1) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221

main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i232', i222) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
was transformed to
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221 + 1, i222) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i222 + 1) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221 + 1, i222) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
main_Load_2(i2, i4, i6, static) -{18,18}> main_Load_607(i4, i2, i6) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i2 < i4 && 0 < 2
main_GE_664(i4, i257, i258) -{1,1}> main_Load_607(i4, i257, i258) :|: i257 < i4 && 0 >= 0
main_Load_607(i4, i221, i222) -{2,2}> main_GE_615(i4, i221, i222) :|: 0 >= 0

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

Simplified expressions.

main_Load_2(i2, i4, i6, static) -{18,18}> main_Load_607(i4, i2, i6) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i2 < i4 && 0 < 2
was transformed to
main_Load_2(i2, i4, i6, static) -{18,18}> main_Load_607(i4, i2, i6) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i2 < i4

main_GE_664(i4, i257, i258) -{1,1}> main_Load_607(i4, i257, i258) :|: i257 < i4 && 0 >= 0
was transformed to
main_GE_664(i4, i257, i258) -{1,1}> main_Load_607(i4, i257, i258) :|: i257 < i4

main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i222 + 1) :|: 0 >= 0 && i222 + 1 = i231' && i222 <= i221
was transformed to
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i222 + 1) :|: i222 + 1 = i231' && i222 <= i221

main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221 + 1, i222) :|: 0 >= 0 && i221 + 1 = i232' && i221 < i222
was transformed to
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221 + 1, i222) :|: i221 + 1 = i232' && i221 < i222

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221 + 1, i222) :|: i221 + 1 = i232' && i221 < i222
main_Load_2(i2, i4, i6, static) -{18,18}> main_Load_607(i4, i2, i6) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i2 < i4
main_GE_615(i4, i221, i222) -{5,5}> main_GE_664(i4, i221, i222 + 1) :|: i222 + 1 = i231' && i222 <= i221
main_GE_664(i4, i257, i258) -{1,1}> main_Load_607(i4, i257, i258) :|: i257 < i4
main_Load_607(i4, i221, i222) -{2,2}> main_GE_615(i4, i221, i222) :|: 0 >= 0

(33) koat Proof (EQUIVALENT transformation)

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

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
(Comp: ?, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: ?, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(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: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
(Comp: 1, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: ?, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_1 < ar_0 ]
(Comp: ?, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ 0 >= 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Applied AI with 'oct' on problem 2 to obtain the following invariants:
For symbol main_GE_615: X_1 - X_2 - 1 >= 0
For symbol main_GE_664: X_1 - X_2 >= 0
For symbol main_Load_607: X_1 - X_2 - 1 >= 0

This yielded the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 >= 0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: 1, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = V_2 - V_3
Pol(main_Load_2) = V_2 - V_3
Pol(main_Load_607) = V_1 - V_3
Pol(main_GE_615) = V_1 - V_3
Pol(main_GE_664) = V_1 - V_3
orients all transitions weakly and the transition
main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 >= 0 /\ ar_1 < ar_0 ]
(Comp: ar_1 + ar_2, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: 1, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = -V_1 + V_2
Pol(main_Load_2) = -V_1 + V_2
Pol(main_Load_607) = V_1 - V_2
Pol(main_GE_615) = V_1 - V_2
Pol(main_GE_664) = V_1 - V_2
orients all transitions weakly and the transition
main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ 0 >= 0 ]
(Comp: ?, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 >= 0 /\ ar_1 < ar_0 ]
(Comp: ar_1 + ar_2, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: 1, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ar_0 + ar_1, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ar_0 + 2*ar_1 + ar_2 + 1, Cost: 2) main_Load_607(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_615(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ 0 >= 0 ]
(Comp: ar_0 + 2*ar_1 + ar_2, Cost: 1) main_GE_664(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_0, ar_1, ar_2, arityPad)) [ ar_0 - ar_1 >= 0 /\ ar_1 < ar_0 ]
(Comp: ar_1 + ar_2, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1, ar_2 + 1, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_2 + 1 = i231' /\ ar_2 <= ar_1 ]
(Comp: 1, Cost: 18) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_607(ar_1, ar_0, ar_2, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_0 < ar_1 ]
(Comp: ar_0 + ar_1, Cost: 5) main_GE_615(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_GE_664(ar_0, ar_1 + 1, ar_2, arityPad)) [ ar_0 - ar_1 - 1 >= 0 /\ ar_1 + 1 = i232' /\ ar_1 < ar_2 ]
start location: koat_start
leaf cost: 0

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

Time: 0.204 sec (SMT: 0.170 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) koat Proof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 20 + 8 * |#0| + 16 * |#1| + 8 * |#2|)