time complexity proof of /tmp/tmpThKVoH/PastaB10.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 6 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), 50 ms)

    ↳14 WeightedIntTrs

        ↳15 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 8 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(2)), 5 ms)

↳22 JBCComplexityEdges

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

    ↳24 WeightedIntTrs

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

    ↳26 WeightedIntTrs

    ↳27 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 10 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 (⇔, 93 ms)

    ↳34 BOUNDS(CONSTANT, 24 + 12 * |#0| + 12 * |#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 PastaB10 {
    public static void main(int x, int y) {
        while (x + y > 0) {
            if (x > 0) {
                x--;
            } else if (y > 0) {
                y--;
            } else {
                continue;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 51 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 51 jbc graph edges to a weighted ITS with 51 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.

(6) Obligation:

IntTrs with 51 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_615(i1, i4, i4, env, static) :|: 0 >= 0
main_Load_615(i72, i73, i74, env, static) -{0,0}> main_Load_696(i72, i73, i72, i74, env, static) :|: 0 >= 0
main_Load_696(i226, i73, i227, i74, env, static) -{1,1}> main_IntArithmetic_719(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_IntArithmetic_719(i226, i73, i227, i74, env, static) -{1,1}> main_LE_725(i226, i73, i237, i227, i74, env, static) :|: i227 + i74 = i237
main_LE_725(i226, i73, i244, i227, i74, env, static) -{0,0}> main_LE_728(i226, i73, i244, i227, i74, env, static) :|: i244 <= 0
main_LE_725(i226, i73, i245, i227, i74, env, static) -{0,0}> main_LE_729(i226, i73, i245, i227, i74, env, static) :|: 1 <= i245
main_LE_729(i226, i73, i245, i227, i74, env, static) -{1,1}> main_Load_733(i226, i73, i227, i74, env, static) :|: 0 < i245 && 1 <= i245
main_Load_733(i226, i73, i227, i74, env, static) -{1,1}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_LE_737(i226, i73, i251, i74, env, static) -{0,0}> main_LE_740(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_LE_737(i226, i73, i252, i74, env, static) -{0,0}> main_LE_741(i226, i73, i252, i74, env, static) :|: 1 <= i252
main_LE_740(i226, i73, i251, i74, env, static) -{1,1}> main_Load_743(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_LE_741(i226, i73, i252, i74, env, static) -{1,1}> main_Inc_745(i226, i73, i252, i74, env, static) :|: 0 < i252 && 1 <= i252
main_Load_743(i226, i73, i251, i74, env, static) -{1,1}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
main_Inc_745(i226, i73, i252, i74, env, static) -{1,1}> main_JMP_751(i226, i73, i257, i74, env, static) :|: 0 <= i257 && i252 + -1 = i257 && 1 <= i252
main_LE_749(i226, i73, i258, i251, env, static) -{0,0}> main_LE_754(i226, i73, i258, i251, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{0,0}> main_LE_755(i226, i73, i259, i251, env, static) :|: i251 <= 0 && 1 <= i259
main_JMP_751(i226, i73, i257, i74, env, static) -{1,1}> main_Load_758(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_LE_754(i226, i73, i258, i251, env, static) -{1,1}> main_Load_762(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_755(i226, i73, i259, i251, env, static) -{1,1}> main_Inc_765(i226, i73, i251, i259, env, static) :|: 0 < i259 && i251 <= 0 && 1 <= i259
main_Load_758(i226, i73, i257, i74, env, static) -{1,1}> main_Load_772(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_762(i226, i73, i251, i258, env, static) -{1,1}> main_Load_777(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_Inc_765(i226, i73, i251, i259, env, static) -{1,1}> main_JMP_779(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0 && 1 <= i259 && i259 + -1 = i269
main_Load_772(i226, i73, i257, i74, env, static) -{0,0}> main_Load_696(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_777(i226, i73, i251, i258, env, static) -{0,0}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_JMP_779(i226, i73, i251, i269, env, static) -{1,1}> main_Load_788(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_788(i226, i73, i251, i269, env, static) -{1,1}> main_Load_794(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_794(i226, i73, i251, i269, env, static) -{0,0}> main_Load_696(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0

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

obtained
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_696(i1, i4, i1, i4, 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 && 0 < 2
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_615(i1, i4, i4, env, static) :|: 0 >= 0
main_Load_615(i72, i73, i74, env, static) -{0,0}> main_Load_696(i72, i73, i72, i74, env, static) :|: 0 >= 0

obtained
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i237', i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'
by chaining
main_Load_696(i226, i73, i227, i74, env, static) -{1,1}> main_IntArithmetic_719(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_IntArithmetic_719(i226, i73, i227, i74, env, static) -{1,1}> main_LE_725(i226, i73, i237, i227, i74, env, static) :|: i227 + i74 = i237

obtained
main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i245 && 0 < i245
by chaining
main_LE_725(i226, i73, i245, i227, i74, env, static) -{0,0}> main_LE_729(i226, i73, i245, i227, i74, env, static) :|: 1 <= i245
main_LE_729(i226, i73, i245, i227, i74, env, static) -{1,1}> main_Load_733(i226, i73, i227, i74, env, static) :|: 0 < i245 && 1 <= i245
main_Load_733(i226, i73, i227, i74, env, static) -{1,1}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0

obtained
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i257', i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
by chaining
main_LE_737(i226, i73, i252, i74, env, static) -{0,0}> main_LE_741(i226, i73, i252, i74, env, static) :|: 1 <= i252
main_LE_741(i226, i73, i252, i74, env, static) -{1,1}> main_Inc_745(i226, i73, i252, i74, env, static) :|: 0 < i252 && 1 <= i252
main_Inc_745(i226, i73, i252, i74, env, static) -{1,1}> main_JMP_751(i226, i73, i257, i74, env, static) :|: 0 <= i257 && i252 + -1 = i257 && 1 <= i252
main_JMP_751(i226, i73, i257, i74, env, static) -{1,1}> main_Load_758(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_758(i226, i73, i257, i74, env, static) -{1,1}> main_Load_772(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_772(i226, i73, i257, i74, env, static) -{0,0}> main_Load_696(i226, i73, i257, i74, env, static) :|: 0 <= i257

obtained
main_LE_737(i226, i73, i251, i74, env, static) -{2,2}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
by chaining
main_LE_737(i226, i73, i251, i74, env, static) -{0,0}> main_LE_740(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_LE_740(i226, i73, i251, i74, env, static) -{1,1}> main_Load_743(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_Load_743(i226, i73, i251, i74, env, static) -{1,1}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0

obtained
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i269', env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
by chaining
main_LE_749(i226, i73, i259, i251, env, static) -{0,0}> main_LE_755(i226, i73, i259, i251, env, static) :|: i251 <= 0 && 1 <= i259
main_LE_755(i226, i73, i259, i251, env, static) -{1,1}> main_Inc_765(i226, i73, i251, i259, env, static) :|: 0 < i259 && i251 <= 0 && 1 <= i259
main_Inc_765(i226, i73, i251, i259, env, static) -{1,1}> main_JMP_779(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0 && 1 <= i259 && i259 + -1 = i269
main_JMP_779(i226, i73, i251, i269, env, static) -{1,1}> main_Load_788(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_788(i226, i73, i251, i269, env, static) -{1,1}> main_Load_794(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_794(i226, i73, i251, i269, env, static) -{0,0}> main_Load_696(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0

obtained
main_LE_749(i226, i73, i258, i251, env, static) -{2,2}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
by chaining
main_LE_749(i226, i73, i258, i251, env, static) -{0,0}> main_LE_754(i226, i73, i258, i251, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_754(i226, i73, i258, i251, env, static) -{1,1}> main_Load_762(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_Load_762(i226, i73, i251, i258, env, static) -{1,1}> main_Load_777(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_Load_777(i226, i73, i251, i258, env, static) -{0,0}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0

(8) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_696(i1, i4, i1, i4, 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 && 0 < 2
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i237', i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'
main_LE_725(i226, i73, i244, i227, i74, env, static) -{0,0}> main_LE_728(i226, i73, i244, i227, i74, env, static) :|: i244 <= 0
main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i245 && 0 < i245
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i257', i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
main_LE_737(i226, i73, i251, i74, env, static) -{2,2}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i269', env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
main_LE_749(i226, i73, i258, i251, env, static) -{2,2}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0

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

Moved arithmethic from constraints to rhss.

main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i237', i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'
was transformed to
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i227 + i74, i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'

main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i257', i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
was transformed to
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i252 + -1, i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252

main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i269', env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
was transformed to
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i259 + -1, env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'

(10) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i227 + i74, i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_696(i1, i4, i1, i4, 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 && 0 < 2
main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i245 && 0 < i245
main_LE_749(i226, i73, i258, i251, env, static) -{2,2}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i252 + -1, i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
main_LE_725(i226, i73, i244, i227, i74, env, static) -{0,0}> main_LE_728(i226, i73, i244, i227, i74, env, static) :|: i244 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i259 + -1, env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
main_LE_737(i226, i73, i251, i74, env, static) -{2,2}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0

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

Simplified expressions.

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

main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i259 + -1, env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
was transformed to
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i259 - 1, env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 - 1 = i269'

main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i245 && 0 < i245
was transformed to
main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 1 <= i245 && 0 < i245

main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i227 + i74, i227, i74, env, static) :|: 0 >= 0 && i227 + i74 = i237'
was transformed to
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i227 + i74, i227, i74, env, static) :|: i227 + i74 = i237'

main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i252 + -1, i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
was transformed to
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i252 - 1, i74, env, static) :|: 0 <= i257' && i252 - 1 = i257' && 1 <= i252 && 0 < i252

(12) Obligation:

IntTrs with 8 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_749(i226, i73, i258, i251, env, static) -{2,2}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i252 - 1, i74, env, static) :|: 0 <= i257' && i252 - 1 = i257' && 1 <= i252 && 0 < i252
main_LE_725(i226, i73, i244, i227, i74, env, static) -{0,0}> main_LE_728(i226, i73, i244, i227, i74, env, static) :|: i244 <= 0
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_696(i1, i4, i1, i4, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_725(i226, i73, i245, i227, i74, env, static) -{2,2}> main_LE_737(i226, i73, i227, i74, env, static) :|: 1 <= i245 && 0 < i245
main_LE_737(i226, i73, i251, i74, env, static) -{2,2}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i259 - 1, env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 - 1 = i269'
main_Load_696(i226, i73, i227, i74, env, static) -{2,2}> main_LE_725(i226, i73, i227 + i74, i227, i74, env, static) :|: i227 + i74 = i237'

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

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

(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(2)) transformation)

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

(22) Obligation:

Set of 50 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 50 jbc graph edges to a weighted ITS with 50 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 50 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, env, static) -{1,1}> main_Load_41(i1, i4, env, static) :|: 0 >= 0
main_Load_41(i1, i4, env, static) -{0,0}> main_Load_42(i1, i4, env, static) :|: 0 >= 0
main_Load_42(i1, i4, env, static) -{0,0}> main_Load_44(i1, i4, env, static) :|: 0 <= static
main_Load_44(i1, i4, env, static) -{0,0}> main_Load_46(i1, i4, env, static) :|: 0 >= 0
main_Load_46(i1, i4, env, static) -{0,0}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{1,1}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_615(i1, i4, i4, env, static) :|: 0 >= 0
main_Load_615(i72, i73, i74, env, static) -{0,0}> main_Load_696(i72, i73, i72, i74, env, static) :|: 0 >= 0
main_Load_696(i226, i73, i227, i74, env, static) -{1,1}> main_IntArithmetic_719(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_IntArithmetic_719(i226, i73, i227, i74, env, static) -{1,1}> main_LE_725(i226, i73, i237, i227, i74, env, static) :|: i227 + i74 = i237
main_LE_725(i226, i73, i245, i227, i74, env, static) -{0,0}> main_LE_729(i226, i73, i245, i227, i74, env, static) :|: 1 <= i245
main_LE_729(i226, i73, i245, i227, i74, env, static) -{1,1}> main_Load_733(i226, i73, i227, i74, env, static) :|: 0 < i245 && 1 <= i245
main_Load_733(i226, i73, i227, i74, env, static) -{1,1}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_LE_737(i226, i73, i251, i74, env, static) -{0,0}> main_LE_740(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_LE_737(i226, i73, i252, i74, env, static) -{0,0}> main_LE_741(i226, i73, i252, i74, env, static) :|: 1 <= i252
main_LE_740(i226, i73, i251, i74, env, static) -{1,1}> main_Load_743(i226, i73, i251, i74, env, static) :|: i251 <= 0
main_LE_741(i226, i73, i252, i74, env, static) -{1,1}> main_Inc_745(i226, i73, i252, i74, env, static) :|: 0 < i252 && 1 <= i252
main_Load_743(i226, i73, i251, i74, env, static) -{1,1}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
main_Inc_745(i226, i73, i252, i74, env, static) -{1,1}> main_JMP_751(i226, i73, i257, i74, env, static) :|: 0 <= i257 && i252 + -1 = i257 && 1 <= i252
main_LE_749(i226, i73, i258, i251, env, static) -{0,0}> main_LE_754(i226, i73, i258, i251, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{0,0}> main_LE_755(i226, i73, i259, i251, env, static) :|: i251 <= 0 && 1 <= i259
main_JMP_751(i226, i73, i257, i74, env, static) -{1,1}> main_Load_758(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_LE_754(i226, i73, i258, i251, env, static) -{1,1}> main_Load_762(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_LE_755(i226, i73, i259, i251, env, static) -{1,1}> main_Inc_765(i226, i73, i251, i259, env, static) :|: 0 < i259 && i251 <= 0 && 1 <= i259
main_Load_758(i226, i73, i257, i74, env, static) -{1,1}> main_Load_772(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_762(i226, i73, i251, i258, env, static) -{1,1}> main_Load_777(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_Inc_765(i226, i73, i251, i259, env, static) -{1,1}> main_JMP_779(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0 && 1 <= i259 && i259 + -1 = i269
main_Load_772(i226, i73, i257, i74, env, static) -{0,0}> main_Load_696(i226, i73, i257, i74, env, static) :|: 0 <= i257
main_Load_777(i226, i73, i251, i258, env, static) -{0,0}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0
main_JMP_779(i226, i73, i251, i269, env, static) -{1,1}> main_Load_788(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_788(i226, i73, i251, i269, env, static) -{1,1}> main_Load_794(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0
main_Load_794(i226, i73, i251, i269, env, static) -{0,0}> main_Load_696(i226, i73, i251, i269, env, static) :|: 0 <= i269 && i251 <= 0

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

obtained
main_Load_696(i226, i73, i227, i74, env, static) -{4,4}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i237' && i227 + i74 = i237' && 0 < i237'
by chaining
main_Load_696(i226, i73, i227, i74, env, static) -{1,1}> main_IntArithmetic_719(i226, i73, i227, i74, env, static) :|: 0 >= 0
main_IntArithmetic_719(i226, i73, i227, i74, env, static) -{1,1}> main_LE_725(i226, i73, i237, i227, i74, env, static) :|: i227 + i74 = i237
main_LE_725(i226, i73, i245, i227, i74, env, static) -{0,0}> main_LE_729(i226, i73, i245, i227, i74, env, static) :|: 1 <= i245
main_LE_729(i226, i73, i245, i227, i74, env, static) -{1,1}> main_Load_733(i226, i73, i227, i74, env, static) :|: 0 < i245 && 1 <= i245
main_Load_733(i226, i73, i227, i74, env, static) -{1,1}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0

(26) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{16,16}> main_Load_696(i1, i4, i1, i4, 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 && 0 < 2
main_Load_696(i226, i73, i227, i74, env, static) -{4,4}> main_LE_737(i226, i73, i227, i74, env, static) :|: 0 >= 0 && 1 <= i237' && i227 + i74 = i237' && 0 < i237'
main_LE_737(i226, i73, i252, i74, env, static) -{4,4}> main_Load_696(i226, i73, i257', i74, env, static) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
main_LE_737(i226, i73, i251, i74, env, static) -{2,2}> main_LE_749(i226, i73, i74, i251, env, static) :|: i251 <= 0
main_LE_749(i226, i73, i259, i251, env, static) -{4,4}> main_Load_696(i226, i73, i251, i269', env, static) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
main_LE_749(i226, i73, i258, i251, env, static) -{2,2}> main_Load_696(i226, i73, i251, i258, env, static) :|: i258 <= 0 && i251 <= 0

(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) → main_Load_2(x1, x2, x4)
main_Load_696(x1, x2, x3, x4, x5, x6) → main_Load_696(x3, x4)
main_LE_737(x1, x2, x3, x4, x5, x6) → main_LE_737(x3, x4)
main_LE_749(x1, x2, x3, x4, x5, x6) → main_LE_749(x3, x4)

(28) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, static) -{16,16}> main_Load_696(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_Load_696(i227, i74) -{4,4}> main_LE_737(i227, i74) :|: 0 >= 0 && 1 <= i237' && i227 + i74 = i237' && 0 < i237'
main_LE_737(i252, i74) -{4,4}> main_Load_696(i257', i74) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
main_LE_737(i251, i74) -{2,2}> main_LE_749(i74, i251) :|: i251 <= 0
main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i269') :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
main_LE_749(i258, i251) -{2,2}> main_Load_696(i251, i258) :|: i258 <= 0 && i251 <= 0

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

Moved arithmethic from constraints to rhss.

main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i269') :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
was transformed to
main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i259 + -1) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'

main_LE_737(i252, i74) -{4,4}> main_Load_696(i257', i74) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
was transformed to
main_LE_737(i252, i74) -{4,4}> main_Load_696(i252 + -1, i74) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252

(30) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_696(i227, i74) -{4,4}> main_LE_737(i227, i74) :|: 0 >= 0 && 1 <= i237' && i227 + i74 = i237' && 0 < i237'
main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i259 + -1) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
main_LE_737(i251, i74) -{2,2}> main_LE_749(i74, i251) :|: i251 <= 0
main_LE_737(i252, i74) -{4,4}> main_Load_696(i252 + -1, i74) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
main_LE_749(i258, i251) -{2,2}> main_Load_696(i251, i258) :|: i258 <= 0 && i251 <= 0
main_Load_2(i1, i4, static) -{16,16}> main_Load_696(i1, i4) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2

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

Simplified expressions.

main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i259 + -1) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 + -1 = i269'
was transformed to
main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i259 - 1) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 - 1 = i269'

main_Load_696(i227, i74) -{4,4}> main_LE_737(i227, i74) :|: 0 >= 0 && 1 <= i237' && i227 + i74 = i237' && 0 < i237'
was transformed to
main_Load_696(i227, i74) -{4,4}> main_LE_737(i227, i74) :|: 1 <= i237' && i227 + i74 = i237' && 0 < i237'

main_LE_737(i252, i74) -{4,4}> main_Load_696(i252 + -1, i74) :|: 0 <= i257' && i252 + -1 = i257' && 1 <= i252 && 0 < i252
was transformed to
main_LE_737(i252, i74) -{4,4}> main_Load_696(i252 - 1, i74) :|: 0 <= i257' && i252 - 1 = i257' && 1 <= i252 && 0 < i252

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

(32) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_749(i259, i251) -{4,4}> main_Load_696(i251, i259 - 1) :|: 1 <= i259 && 0 <= i269' && i251 <= 0 && 0 < i259 && i259 - 1 = i269'
main_Load_2(i1, i4, static) -{16,16}> main_Load_696(i1, i4) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_737(i251, i74) -{2,2}> main_LE_749(i74, i251) :|: i251 <= 0
main_LE_737(i252, i74) -{4,4}> main_Load_696(i252 - 1, i74) :|: 0 <= i257' && i252 - 1 = i257' && 1 <= i252 && 0 < i252
main_Load_696(i227, i74) -{4,4}> main_LE_737(i227, i74) :|: 1 <= i237' && i227 + i74 = i237' && 0 < i237'
main_LE_749(i258, i251) -{2,2}> main_Load_696(i251, i258) :|: i258 <= 0 && i251 <= 0

(33) koat Proof (EQUIVALENT transformation)

YES(?, 12*ar_1 + 12*ar_0 + 24)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 4) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_LE_749(ar_1, ar_0, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 4) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_Load_696(ar_0, ar_1, ar_2) -> Com_1(main_LE_737(ar_0, ar_1, arityPad)) [ 1 <= i237' /\ ar_0 + ar_1 = i237' /\ 0 < i237' ]
(Comp: ?, Cost: 2) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0, arityPad)) [ ar_0 <= 0 /\ ar_1 <= 0 ]
(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 1 produces the following problem:
2: T:
(Comp: ?, Cost: 4) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_LE_749(ar_1, ar_0, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 4) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_Load_696(ar_0, ar_1, ar_2) -> Com_1(main_LE_737(ar_0, ar_1, arityPad)) [ 1 <= i237' /\ ar_0 + ar_1 = i237' /\ 0 < i237' ]
(Comp: ?, Cost: 2) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0, arityPad)) [ ar_0 <= 0 /\ ar_1 <= 0 ]
(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_LE_749) = V_1
Pol(main_Load_696) = V_2
Pol(main_Load_2) = V_2
Pol(main_LE_737) = V_2
Pol(koat_start) = V_2
orients all transitions weakly and the transition
main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
strictly and produces the following problem:
3: T:
(Comp: ar_1, Cost: 4) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_LE_749(ar_1, ar_0, arityPad)) [ ar_0 <= 0 ]
(Comp: ?, Cost: 4) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_Load_696(ar_0, ar_1, ar_2) -> Com_1(main_LE_737(ar_0, ar_1, arityPad)) [ 1 <= i237' /\ ar_0 + ar_1 = i237' /\ 0 < i237' ]
(Comp: ?, Cost: 2) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0, arityPad)) [ ar_0 <= 0 /\ ar_1 <= 0 ]
(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_LE_749) = V_2
Pol(main_Load_696) = V_1
Pol(main_Load_2) = V_1
Pol(main_LE_737) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: ar_1, Cost: 4) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 2) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_LE_749(ar_1, ar_0, arityPad)) [ ar_0 <= 0 ]
(Comp: ar_0, Cost: 4) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ?, Cost: 4) main_Load_696(ar_0, ar_1, ar_2) -> Com_1(main_LE_737(ar_0, ar_1, arityPad)) [ 1 <= i237' /\ ar_0 + ar_1 = i237' /\ 0 < i237' ]
(Comp: ?, Cost: 2) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0, arityPad)) [ ar_0 <= 0 /\ ar_1 <= 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5: T:
(Comp: ar_1, Cost: 4) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0 - 1, arityPad)) [ 1 <= ar_0 /\ 0 <= i269' /\ ar_1 <= 0 /\ 0 < ar_0 /\ ar_0 - 1 = i269' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ar_0 + ar_1 + 1, Cost: 2) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_LE_749(ar_1, ar_0, arityPad)) [ ar_0 <= 0 ]
(Comp: ar_0, Cost: 4) main_LE_737(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_0 - 1, ar_1, arityPad)) [ 0 <= i257' /\ ar_0 - 1 = i257' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: ar_0 + ar_1 + 1, Cost: 4) main_Load_696(ar_0, ar_1, ar_2) -> Com_1(main_LE_737(ar_0, ar_1, arityPad)) [ 1 <= i237' /\ ar_0 + ar_1 = i237' /\ 0 < i237' ]
(Comp: ar_0 + ar_1 + 1, Cost: 2) main_LE_749(ar_0, ar_1, ar_2) -> Com_1(main_Load_696(ar_1, ar_0, arityPad)) [ ar_0 <= 0 /\ ar_1 <= 0 ]
(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 12*ar_1 + 12*ar_0 + 24

Time: 0.238 sec (SMT: 0.210 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) 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(2)) 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, 24 + 12 * |#0| + 12 * |#1|)