time complexity proof of /tmp/tmplGCfUG/PastaA10.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 96 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

↳25 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 0 ms)

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 28 ms)

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 64 ms)

    ↳40 BOUNDS(CONSTANT, 76 + 32 * |#0| + 32 * |#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 PastaA10 {
    public static void main(int x, int y) {
        while (x != y) {
            if (x > y) {
                y++;
            } else {
                x++;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 62 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 62 jbc graph edges to a weighted ITS with 62 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 62 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_13(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_14(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_22(o1, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_22(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Load_25(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_27(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_27(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_29(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_29(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_33(i2, i4, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_33(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_48(i2, i4, env, static) :|: 0 >= 0
main_Load_48(i2, i4, env, static) -{1,1}> main_Load_50(i2, i4, env, static) :|: 0 >= 0
main_Load_50(i2, i4, env, static) -{1,1}> main_EQ_52(i2, i4, env, static) :|: 0 >= 0
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_57(i2, i4, env, static) :|: !(i2 = i4)
main_EQ_57(i2, i4, env, static) -{1,1}> main_Load_60(i2, i4, env, static) :|: !(i2 = i4)
main_Load_60(i2, i4, env, static) -{1,1}> main_Load_62(i2, i4, env, static) :|: 0 >= 0
main_Load_62(i2, i4, env, static) -{1,1}> main_LE_68(i2, i4, env, static) :|: 0 >= 0
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_72(i2, i4, env, static) :|: i2 <= i4
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_73(i2, i4, env, static) :|: i4 < i2
main_LE_72(i2, i4, env, static) -{1,1}> main_Inc_76(i2, i4, env, static) :|: i2 < i4
main_LE_73(i2, i4, env, static) -{1,1}> main_Inc_77(i2, i4, env, static) :|: i4 < i2
main_Inc_76(i2, i4, env, static) -{1,1}> main_JMP_78(i2, i4, i7, env, static) :|: i2 + 1 = i7
main_Inc_77(i2, i4, env, static) -{1,1}> main_JMP_79(i2, i4, i8, env, static) :|: i4 + 1 = i8
main_JMP_78(i2, i4, i7, env, static) -{0,0}> main_JMP_253(i2, i4, i7, env, static) :|: 0 >= 0
main_JMP_79(i2, i4, i8, env, static) -{0,0}> main_JMP_254(i2, i4, i8, env, static) :|: 0 >= 0
main_JMP_253(i2, i4, i64, env, static) -{1,1}> main_Load_256(i2, i4, i64, env, static) :|: 0 >= 0
main_JMP_254(i2, i4, i66, env, static) -{1,1}> main_Load_259(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_256(i2, i4, i64, env, static) -{1,1}> main_Load_260(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_259(i2, i4, i66, env, static) -{1,1}> main_Load_270(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_260(i2, i4, i64, env, static) -{1,1}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_270(i2, i4, i66, env, static) -{1,1}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_307(i2, i4, i64, env, static) :|: !(i64 = i4)
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_317(i2, i4, i66, env, static) :|: !(i2 = i66)
main_EQ_307(i2, i4, i64, env, static) -{1,1}> main_Load_319(i2, i4, i64, env, static) :|: i64 < i4
main_EQ_317(i2, i4, i66, env, static) -{1,1}> main_Load_334(i2, i4, i66, env, static) :|: i66 < i2
main_Load_319(i2, i4, i64, env, static) -{1,1}> main_Load_341(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_334(i2, i4, i66, env, static) -{1,1}> main_Load_352(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_341(i2, i4, i64, env, static) -{1,1}> main_LE_387(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_352(i2, i4, i66, env, static) -{1,1}> main_LE_412(i2, i4, i66, env, static) :|: 0 >= 0
main_LE_387(i2, i4, i64, env, static) -{0,0}> main_LE_417(i2, i4, i64, env, static) :|: i64 <= i4
main_LE_412(i2, i4, i66, env, static) -{0,0}> main_LE_418(i2, i4, i66, env, static) :|: i66 < i2
main_LE_417(i2, i4, i64, env, static) -{1,1}> main_Inc_433(i2, i4, i64, env, static) :|: i64 < i4
main_LE_418(i2, i4, i66, env, static) -{1,1}> main_Inc_436(i2, i4, i66, env, static) :|: i66 < i2
main_Inc_433(i2, i4, i64, env, static) -{1,1}> main_JMP_449(i2, i4, i127, env, static) :|: i64 + 1 = i127
main_Inc_436(i2, i4, i66, env, static) -{1,1}> main_JMP_454(i2, i4, i129, env, static) :|: i66 + 1 = i129
main_JMP_449(i2, i4, i127, env, static) -{0,0}> main_JMP_253(i2, i4, i127, env, static) :|: 0 >= 0
main_JMP_454(i2, i4, i129, env, static) -{0,0}> main_JMP_254(i2, i4, i129, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
by chaining
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_13(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_14(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_22(o1, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_22(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Load_25(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_27(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_27(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_29(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_29(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_33(i2, i4, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_33(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_48(i2, i4, env, static) :|: 0 >= 0
main_Load_48(i2, i4, env, static) -{1,1}> main_Load_50(i2, i4, env, static) :|: 0 >= 0
main_Load_50(i2, i4, env, static) -{1,1}> main_EQ_52(i2, i4, env, static) :|: 0 >= 0

obtained
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && !(i2 = i4)
by chaining
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_57(i2, i4, env, static) :|: !(i2 = i4)
main_EQ_57(i2, i4, env, static) -{1,1}> main_Load_60(i2, i4, env, static) :|: !(i2 = i4)
main_Load_60(i2, i4, env, static) -{1,1}> main_Load_62(i2, i4, env, static) :|: 0 >= 0
main_Load_62(i2, i4, env, static) -{1,1}> main_LE_68(i2, i4, env, static) :|: 0 >= 0

obtained
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i8', env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
by chaining
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_73(i2, i4, env, static) :|: i4 < i2
main_LE_73(i2, i4, env, static) -{1,1}> main_Inc_77(i2, i4, env, static) :|: i4 < i2
main_Inc_77(i2, i4, env, static) -{1,1}> main_JMP_79(i2, i4, i8, env, static) :|: i4 + 1 = i8
main_JMP_79(i2, i4, i8, env, static) -{0,0}> main_JMP_254(i2, i4, i8, env, static) :|: 0 >= 0

obtained
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
by chaining
main_JMP_254(i2, i4, i66, env, static) -{1,1}> main_Load_259(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_259(i2, i4, i66, env, static) -{1,1}> main_Load_270(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_270(i2, i4, i66, env, static) -{1,1}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0

obtained
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
by chaining
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_317(i2, i4, i66, env, static) :|: !(i2 = i66)
main_EQ_317(i2, i4, i66, env, static) -{1,1}> main_Load_334(i2, i4, i66, env, static) :|: i66 < i2
main_Load_334(i2, i4, i66, env, static) -{1,1}> main_Load_352(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_352(i2, i4, i66, env, static) -{1,1}> main_LE_412(i2, i4, i66, env, static) :|: 0 >= 0
main_LE_412(i2, i4, i66, env, static) -{0,0}> main_LE_418(i2, i4, i66, env, static) :|: i66 < i2
main_LE_418(i2, i4, i66, env, static) -{1,1}> main_Inc_436(i2, i4, i66, env, static) :|: i66 < i2
main_Inc_436(i2, i4, i66, env, static) -{1,1}> main_JMP_454(i2, i4, i129, env, static) :|: i66 + 1 = i129
main_JMP_454(i2, i4, i129, env, static) -{0,0}> main_JMP_254(i2, i4, i129, env, static) :|: 0 >= 0

obtained
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i7', env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
by chaining
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_72(i2, i4, env, static) :|: i2 <= i4
main_LE_72(i2, i4, env, static) -{1,1}> main_Inc_76(i2, i4, env, static) :|: i2 < i4
main_Inc_76(i2, i4, env, static) -{1,1}> main_JMP_78(i2, i4, i7, env, static) :|: i2 + 1 = i7
main_JMP_78(i2, i4, i7, env, static) -{0,0}> main_JMP_253(i2, i4, i7, env, static) :|: 0 >= 0

obtained
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
by chaining
main_JMP_253(i2, i4, i64, env, static) -{1,1}> main_Load_256(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_256(i2, i4, i64, env, static) -{1,1}> main_Load_260(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_260(i2, i4, i64, env, static) -{1,1}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0

obtained
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)
by chaining
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_307(i2, i4, i64, env, static) :|: !(i64 = i4)
main_EQ_307(i2, i4, i64, env, static) -{1,1}> main_Load_319(i2, i4, i64, env, static) :|: i64 < i4
main_Load_319(i2, i4, i64, env, static) -{1,1}> main_Load_341(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_341(i2, i4, i64, env, static) -{1,1}> main_LE_387(i2, i4, i64, env, static) :|: 0 >= 0
main_LE_387(i2, i4, i64, env, static) -{0,0}> main_LE_417(i2, i4, i64, env, static) :|: i64 <= i4
main_LE_417(i2, i4, i64, env, static) -{1,1}> main_Inc_433(i2, i4, i64, env, static) :|: i64 < i4
main_Inc_433(i2, i4, i64, env, static) -{1,1}> main_JMP_449(i2, i4, i127, env, static) :|: i64 + 1 = i127
main_JMP_449(i2, i4, i127, env, static) -{0,0}> main_JMP_253(i2, i4, i127, env, static) :|: 0 >= 0

(8) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && !(i2 = i4)
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i8', env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i7', env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)

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

Removed div and mod.

main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)
was transformed to
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4

main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && !(i2 = i4)
was transformed to
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4

main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
was transformed to
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66

(10) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i8', env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i7', env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4

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

Moved arithmethic from constraints to rhss.

main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i8', env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
was transformed to
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'

main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
was transformed to
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66

main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
was transformed to
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66

main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
was transformed to
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4

main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
was transformed to
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4

main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i7', env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
was transformed to
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4

(12) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4

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

Simplified expressions.

main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
was transformed to
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: i4 < i2 && i4 + 1 = i8'

main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
was transformed to
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i2 < i4

main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
was transformed to
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: i64 + 1 = i127' && i64 < i4

main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
was transformed to
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: i66 + 1 = i129' && i66 < i2

main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
was transformed to
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: i2 < i4 && i2 + 1 = i7'

main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
was transformed to
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: i66 < i2 && i66 + 1 = i129' && i2 < i66

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

main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4
was transformed to
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i4 < i2

main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
was transformed to
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: i64 < i4 && i64 + 1 = i127' && i4 < i64

(14) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: i66 < i2 && i66 + 1 = i129' && i2 < i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: i66 + 1 = i129' && i66 < i2
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static'''
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: i4 < i2 && i4 + 1 = i8'
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: i64 + 1 = i127' && i64 < i4
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: i64 < i4 && i64 + 1 = i127' && i4 < i64
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: i2 < i4 && i2 + 1 = i7'
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i2 < i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i4 < i2

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

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

(16) Obligation:

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

(18) Obligation:

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

Removed div and mod.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_56(i4, env, static) :|: i2 = i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i4 + 1, env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_306(i2, i4, env, static) :|: i64 = i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
main_JMP_253(i2, i4, i64, env, static) -{3,3}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_316(i66, i4, env, static) :|: i2 = i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_EQ_305(i2, i4, i66, env, static) -{5,5}> main_JMP_254(i2, i4, i66 + 1, env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_Load_2(i2, i4, env, static) -{17,17}> main_EQ_52(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_JMP_254(i2, i4, i66, env, static) -{3,3}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
main_EQ_297(i2, i4, i64, env, static) -{5,5}> main_JMP_253(i2, i4, i64 + 1, env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i2 + 1, env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4

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

Simplified expressions.

main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 < i4
was transformed to
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i2 < i4

main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: 0 >= 0 && i2 > i4
was transformed to
main_EQ_52(i2, i4, env, static) -{3,3}> main_LE_68(i2, i4, env, static) :|: i4 < i2

(24) Obligation:

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

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 59 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_13(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_14(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_22(o1, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_22(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Load_25(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_27(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_27(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_29(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_29(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_33(i2, i4, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_33(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_48(i2, i4, env, static) :|: 0 >= 0
main_Load_48(i2, i4, env, static) -{1,1}> main_Load_50(i2, i4, env, static) :|: 0 >= 0
main_Load_50(i2, i4, env, static) -{1,1}> main_EQ_52(i2, i4, env, static) :|: 0 >= 0
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_57(i2, i4, env, static) :|: !(i2 = i4)
main_EQ_57(i2, i4, env, static) -{1,1}> main_Load_60(i2, i4, env, static) :|: !(i2 = i4)
main_Load_60(i2, i4, env, static) -{1,1}> main_Load_62(i2, i4, env, static) :|: 0 >= 0
main_Load_62(i2, i4, env, static) -{1,1}> main_LE_68(i2, i4, env, static) :|: 0 >= 0
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_72(i2, i4, env, static) :|: i2 <= i4
main_LE_68(i2, i4, env, static) -{0,0}> main_LE_73(i2, i4, env, static) :|: i4 < i2
main_LE_72(i2, i4, env, static) -{1,1}> main_Inc_76(i2, i4, env, static) :|: i2 < i4
main_LE_73(i2, i4, env, static) -{1,1}> main_Inc_77(i2, i4, env, static) :|: i4 < i2
main_Inc_76(i2, i4, env, static) -{1,1}> main_JMP_78(i2, i4, i7, env, static) :|: i2 + 1 = i7
main_Inc_77(i2, i4, env, static) -{1,1}> main_JMP_79(i2, i4, i8, env, static) :|: i4 + 1 = i8
main_JMP_78(i2, i4, i7, env, static) -{0,0}> main_JMP_253(i2, i4, i7, env, static) :|: 0 >= 0
main_JMP_79(i2, i4, i8, env, static) -{0,0}> main_JMP_254(i2, i4, i8, env, static) :|: 0 >= 0
main_JMP_253(i2, i4, i64, env, static) -{1,1}> main_Load_256(i2, i4, i64, env, static) :|: 0 >= 0
main_JMP_254(i2, i4, i66, env, static) -{1,1}> main_Load_259(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_256(i2, i4, i64, env, static) -{1,1}> main_Load_260(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_259(i2, i4, i66, env, static) -{1,1}> main_Load_270(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_260(i2, i4, i64, env, static) -{1,1}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_270(i2, i4, i66, env, static) -{1,1}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_307(i2, i4, i64, env, static) :|: !(i64 = i4)
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_317(i2, i4, i66, env, static) :|: !(i2 = i66)
main_EQ_307(i2, i4, i64, env, static) -{1,1}> main_Load_319(i2, i4, i64, env, static) :|: i64 < i4
main_EQ_317(i2, i4, i66, env, static) -{1,1}> main_Load_334(i2, i4, i66, env, static) :|: i66 < i2
main_Load_319(i2, i4, i64, env, static) -{1,1}> main_Load_341(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_334(i2, i4, i66, env, static) -{1,1}> main_Load_352(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_341(i2, i4, i64, env, static) -{1,1}> main_LE_387(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_352(i2, i4, i66, env, static) -{1,1}> main_LE_412(i2, i4, i66, env, static) :|: 0 >= 0
main_LE_387(i2, i4, i64, env, static) -{0,0}> main_LE_417(i2, i4, i64, env, static) :|: i64 <= i4
main_LE_412(i2, i4, i66, env, static) -{0,0}> main_LE_418(i2, i4, i66, env, static) :|: i66 < i2
main_LE_417(i2, i4, i64, env, static) -{1,1}> main_Inc_433(i2, i4, i64, env, static) :|: i64 < i4
main_LE_418(i2, i4, i66, env, static) -{1,1}> main_Inc_436(i2, i4, i66, env, static) :|: i66 < i2
main_Inc_433(i2, i4, i64, env, static) -{1,1}> main_JMP_449(i2, i4, i127, env, static) :|: i64 + 1 = i127
main_Inc_436(i2, i4, i66, env, static) -{1,1}> main_JMP_454(i2, i4, i129, env, static) :|: i66 + 1 = i129
main_JMP_449(i2, i4, i127, env, static) -{0,0}> main_JMP_253(i2, i4, i127, env, static) :|: 0 >= 0
main_JMP_454(i2, i4, i129, env, static) -{0,0}> main_JMP_254(i2, i4, i129, env, static) :|: 0 >= 0

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

obtained
main_Load_2(i2, i4, env, static) -{20,20}> main_LE_68(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && !(i2 = i4) && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
by chaining
main_Load_2(i2, i4, env, static) -{0,0}> main_Load_4(i2, i4, env, static) :|: 0 >= 0
main_Load_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_13(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_13(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_14(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_16(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_17(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_20(o1, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_22(o1, i2, i4, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_22(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_24(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Load_25(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_27(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_27(o1, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_29(o1, i2, i4, env, static) :|: 0 < o1
langle_init_rangle_Return_29(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_31(o1, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_33(i2, i4, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_33(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{0,0}> main_Load_48(i2, i4, env, static) :|: 0 >= 0
main_Load_48(i2, i4, env, static) -{1,1}> main_Load_50(i2, i4, env, static) :|: 0 >= 0
main_Load_50(i2, i4, env, static) -{1,1}> main_EQ_52(i2, i4, env, static) :|: 0 >= 0
main_EQ_52(i2, i4, env, static) -{0,0}> main_EQ_57(i2, i4, env, static) :|: !(i2 = i4)
main_EQ_57(i2, i4, env, static) -{1,1}> main_Load_60(i2, i4, env, static) :|: !(i2 = i4)
main_Load_60(i2, i4, env, static) -{1,1}> main_Load_62(i2, i4, env, static) :|: 0 >= 0
main_Load_62(i2, i4, env, static) -{1,1}> main_LE_68(i2, i4, env, static) :|: 0 >= 0

obtained
main_JMP_254(i2, i4, i66, env, static) -{8,8}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
by chaining
main_JMP_254(i2, i4, i66, env, static) -{1,1}> main_Load_259(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_259(i2, i4, i66, env, static) -{1,1}> main_Load_270(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_270(i2, i4, i66, env, static) -{1,1}> main_EQ_305(i2, i4, i66, env, static) :|: 0 >= 0
main_EQ_305(i2, i4, i66, env, static) -{0,0}> main_EQ_317(i2, i4, i66, env, static) :|: !(i2 = i66)
main_EQ_317(i2, i4, i66, env, static) -{1,1}> main_Load_334(i2, i4, i66, env, static) :|: i66 < i2
main_Load_334(i2, i4, i66, env, static) -{1,1}> main_Load_352(i2, i4, i66, env, static) :|: 0 >= 0
main_Load_352(i2, i4, i66, env, static) -{1,1}> main_LE_412(i2, i4, i66, env, static) :|: 0 >= 0
main_LE_412(i2, i4, i66, env, static) -{0,0}> main_LE_418(i2, i4, i66, env, static) :|: i66 < i2
main_LE_418(i2, i4, i66, env, static) -{1,1}> main_Inc_436(i2, i4, i66, env, static) :|: i66 < i2
main_Inc_436(i2, i4, i66, env, static) -{1,1}> main_JMP_454(i2, i4, i129, env, static) :|: i66 + 1 = i129
main_JMP_454(i2, i4, i129, env, static) -{0,0}> main_JMP_254(i2, i4, i129, env, static) :|: 0 >= 0

obtained
main_JMP_253(i2, i4, i64, env, static) -{8,8}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)
by chaining
main_JMP_253(i2, i4, i64, env, static) -{1,1}> main_Load_256(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_256(i2, i4, i64, env, static) -{1,1}> main_Load_260(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_260(i2, i4, i64, env, static) -{1,1}> main_EQ_297(i2, i4, i64, env, static) :|: 0 >= 0
main_EQ_297(i2, i4, i64, env, static) -{0,0}> main_EQ_307(i2, i4, i64, env, static) :|: !(i64 = i4)
main_EQ_307(i2, i4, i64, env, static) -{1,1}> main_Load_319(i2, i4, i64, env, static) :|: i64 < i4
main_Load_319(i2, i4, i64, env, static) -{1,1}> main_Load_341(i2, i4, i64, env, static) :|: 0 >= 0
main_Load_341(i2, i4, i64, env, static) -{1,1}> main_LE_387(i2, i4, i64, env, static) :|: 0 >= 0
main_LE_387(i2, i4, i64, env, static) -{0,0}> main_LE_417(i2, i4, i64, env, static) :|: i64 <= i4
main_LE_417(i2, i4, i64, env, static) -{1,1}> main_Inc_433(i2, i4, i64, env, static) :|: i64 < i4
main_Inc_433(i2, i4, i64, env, static) -{1,1}> main_JMP_449(i2, i4, i127, env, static) :|: i64 + 1 = i127
main_JMP_449(i2, i4, i127, env, static) -{0,0}> main_JMP_253(i2, i4, i127, env, static) :|: 0 >= 0

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, env, static) -{20,20}> main_LE_68(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && !(i2 = i4) && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_254(i2, i4, i8', env, static) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_JMP_254(i2, i4, i66, env, static) -{8,8}> main_JMP_254(i2, i4, i129', env, static) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
main_LE_68(i2, i4, env, static) -{2,2}> main_JMP_253(i2, i4, i7', env, static) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
main_JMP_253(i2, i4, i64, env, static) -{8,8}> main_JMP_253(i2, i4, i127', env, static) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)

(31) 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_LE_68(x1, x2, x3, x4) → main_LE_68(x1, x2)
main_JMP_254(x1, x2, x3, x4, x5) → main_JMP_254(x1, x3)
main_JMP_253(x1, x2, x3, x4, x5) → main_JMP_253(x2, x3)

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: 0 >= 0 && 0 < 2 && !(i2 = i4) && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i8') :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i7') :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)

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

Removed div and mod.

main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && !(i64 = i4)
was transformed to
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4

main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && !(i2 = i66)
was transformed to
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66

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

(34) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: 0 >= 0 && 0 < 2 && i2 > i4 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i7') :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i8') :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: 0 >= 0 && 0 < 2 && i2 < i4 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1

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

Moved arithmethic from constraints to rhss.

main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
was transformed to
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66

main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i129') :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
was transformed to
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66

main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
was transformed to
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4

main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i127') :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
was transformed to
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4

main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i7') :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
was transformed to
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i2 + 1) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4

main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i8') :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
was transformed to
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'

(36) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: 0 >= 0 && 0 < 2 && i2 > i4 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i2 + 1) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: 0 >= 0 && 0 < 2 && i2 < i4 && 0 <= static'1 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'

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

Simplified expressions.

main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 < i4
was transformed to
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: i64 + 1 = i127' && i64 < i4

main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 > i66
was transformed to
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: i66 + 1 = i129' && i66 < i2

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

main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i2 + 1) :|: 0 >= 0 && i2 < i4 && i2 + 1 = i7' && i2 <= i4
was transformed to
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i2 + 1) :|: i2 < i4 && i2 + 1 = i7'

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

main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: 0 >= 0 && i64 < i4 && i64 <= i4 && i64 + 1 = i127' && i64 > i4
was transformed to
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: i64 < i4 && i64 + 1 = i127' && i4 < i64

main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: 0 >= 0 && i66 < i2 && i66 + 1 = i129' && i2 < i66
was transformed to
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: i66 < i2 && i66 + 1 = i129' && i2 < i66

main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i4 + 1) :|: 0 >= 0 && i4 < i2 && i4 + 1 = i8'
was transformed to
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i4 + 1) :|: i4 < i2 && i4 + 1 = i8'

(38) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_68(i2, i4) -{2,2}> main_JMP_253(i4, i2 + 1) :|: i2 < i4 && i2 + 1 = i7'
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: i66 < i2 && i66 + 1 = i129' && i2 < i66
main_LE_68(i2, i4) -{2,2}> main_JMP_254(i2, i4 + 1) :|: i4 < i2 && i4 + 1 = i8'
main_JMP_254(i2, i66) -{8,8}> main_JMP_254(i2, i66 + 1) :|: i66 + 1 = i129' && i66 < i2
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: i64 + 1 = i127' && i64 < i4
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: i4 < i2 && 0 <= static'1 && 0 <= static && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static'''
main_Load_2(i2, i4, static) -{20,20}> main_LE_68(i2, i4) :|: i2 < i4 && 0 <= static'1 && 0 <= static && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static'''
main_JMP_253(i4, i64) -{8,8}> main_JMP_253(i4, i64 + 1) :|: i64 < i4 && i64 + 1 = i127' && i4 < i64

(39) koat Proof (EQUIVALENT transformation)

YES(?, 32*ar_0 + 32*ar_1 + 76)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\ ar_0 + 1 = i7' ]
(Comp: ?, Cost: 8) main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i129' /\ ar_0 < ar_1 ]
(Comp: ?, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i8' ]
(Comp: ?, Cost: 8) main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 8) main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(Comp: ?, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(Comp: ?, Cost: 8) main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i127' /\ 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 transitions from problem 1:
main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i129' /\ ar_0 < ar_1 ]
main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i127' /\ ar_0 < ar_1 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 8) main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 8) main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\ ar_0 + 1 = i7' ]
(Comp: ?, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i8' ]
(Comp: ?, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(Comp: ?, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(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: 8) main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 8) main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\ ar_0 + 1 = i7' ]
(Comp: 1, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i8' ]
(Comp: 1, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(Comp: 1, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(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_JMP_254) = V_1 - V_2
Pol(main_JMP_253) = V_1 - V_2
and size complexities
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]", 0-2) = ar_2
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-1) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-2) = ?
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-1) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static'1 <= static''' + 1 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' ]", 0-2) = ?
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\\ ar_1 + 1 = i8' ]", 0-0) = ar_0
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\\ ar_1 + 1 = i8' ]", 0-1) = ar_1 + 1
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\\ ar_1 + 1 = i8' ]", 0-2) = ?
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\\ ar_0 + 1 = i7' ]", 0-0) = ar_1
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\\ ar_0 + 1 = i7' ]", 0-1) = ar_0 + 1
S("main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\\ ar_0 + 1 = i7' ]", 0-2) = ?
S("main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\\ ar_1 < ar_0 ]", 0-0) = ar_1
S("main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\\ ar_1 < ar_0 ]", 0-1) = ?
S("main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\\ ar_1 < ar_0 ]", 0-2) = ?
S("main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\\ ar_1 < ar_0 ]", 0-0) = ar_0
S("main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\\ ar_1 < ar_0 ]", 0-1) = ?
S("main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\\ ar_1 < ar_0 ]", 0-2) = ?
orients the transitions
main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
weakly and the transitions
main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: 2*ar_0 + 2*ar_1 + 2, Cost: 8) main_JMP_254(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i129' /\ ar_1 < ar_0 ]
(Comp: 2*ar_0 + 2*ar_1 + 2, Cost: 8) main_JMP_253(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_0, ar_1 + 1, arityPad)) [ ar_1 + 1 = i127' /\ ar_1 < ar_0 ]
(Comp: 1, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_253(ar_1, ar_0 + 1, arityPad)) [ ar_0 < ar_1 /\ ar_0 + 1 = i7' ]
(Comp: 1, Cost: 2) main_LE_68(ar_0, ar_1, ar_2) -> Com_1(main_JMP_254(ar_0, ar_1 + 1, arityPad)) [ ar_1 < ar_0 /\ ar_1 + 1 = i8' ]
(Comp: 1, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(Comp: 1, Cost: 20) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_68(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static'1 <= static''' + 1 /\ static''' <= ar_2 + 2 /\ 0 <= static''' ]
(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 32*ar_0 + 32*ar_1 + 76

Time: 0.156 sec (SMT: 0.143 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 76 + 32 * |#0| + 32 * |#1|)