time complexity proof of /tmp/tmpW1XB9m/PastaB18.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

↳25 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)), 15 ms)

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

    ↳33 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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 (⇔, 126 ms)

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

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

Constructed TerminationGraph.

(2) Obligation:

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

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) 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(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_48(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_48(i1, i3, env, static) -{1,1}> main_Load_56(i1, i3, env, static) :|: 0 >= 0
main_Load_56(i1, i3, env, static) -{0,0}> main_Load_58(i1, i3, env, static) :|: 0 >= 0
main_Load_58(i1, i3, env, static) -{0,0}> main_Load_60(i1, i3, env, static) :|: 0 <= static
main_Load_60(i1, i3, env, static) -{0,0}> main_Load_61(i1, i3, env, static) :|: 0 >= 0
main_Load_61(i1, i3, env, static) -{0,0}> main_Load_62(i1, i3, env, static) :|: 0 >= 0
main_Load_62(i1, i3, env, static) -{1,1}> main_LE_63(i1, i3, env, static) :|: 0 >= 0
main_LE_63(i1, i3, env, static) -{0,0}> main_LE_305(i1, i3, i3, env, static) :|: 0 >= 0
main_LE_305(i78, i79, i80, env, static) -{0,0}> main_LE_547(i78, i79, i78, i80, env, static) :|: 0 >= 0
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_LE_547(i157, i79, i167, i159, env, static) -{0,0}> main_LE_549(i157, i79, i167, i159, env, static) :|: 1 <= i167
main_LE_549(i157, i79, i167, i159, env, static) -{1,1}> main_Load_551(i157, i79, i167, i159, env, static) :|: 1 <= i167 && 0 < i167
main_Load_551(i157, i79, i167, i159, env, static) -{1,1}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{0,0}> main_LE_555(i157, i79, i173, i167, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_555(i157, i79, i173, i167, env, static) -{1,1}> main_Load_559(i157, i79, i167, i173, env, static) :|: 0 < i173 && 1 <= i167 && 1 <= i173
main_Load_559(i157, i79, i167, i173, env, static) -{1,1}> main_Load_562(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_Load_562(i157, i79, i167, i173, env, static) -{1,1}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_572(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_574(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i173 < i167
main_LE_572(i157, i79, i167, i173, env, static) -{1,1}> main_Load_580(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_LE_574(i157, i79, i167, i173, env, static) -{1,1}> main_Load_586(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173 && i173 < i167
main_Load_580(i157, i79, i167, i173, env, static) -{0,0}> main_Load_607(i157, i79, i167, i173, env, static) :|: 0 <= i173 && 1 <= i167 && 1 <= i173
main_Load_586(i157, i79, i167, i173, env, static) -{0,0}> main_Load_619(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_Load_619(i157, i79, i180, i173, env, static) -{0,0}> main_Load_668(i157, i79, i180, i173, env, static) :|: 1 <= i180 && 1 <= i173
main_LE_623(i157, i79, iconst_0, i167, env, static) -{0,0}> main_LE_627(i157, i79, iconst_0, i167, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{0,0}> main_LE_628(i157, i79, i189, i167, env, static) :|: 0 <= i189 && 1 <= i189 && 1 <= i167
main_LE_627(i157, i79, iconst_0, i167, env, static) -{1,1}> main_Load_633(i157, i79, i167, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0 && 1 <= i167
main_LE_628(i157, i79, i189, i167, env, static) -{1,1}> main_Inc_635(i157, i79, i167, i189, env, static) :|: 1 <= i189 && 0 < i189 && 1 <= i167
main_Load_633(i157, i79, i167, iconst_0, env, static) -{1,1}> main_LE_643(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167
main_Inc_635(i157, i79, i167, i189, env, static) -{1,1}> main_JMP_647(i157, i79, i167, i197, env, static) :|: 1 <= i189 && 1 <= i167 && 0 <= i197 && i189 + -1 = i197
main_LE_643(i157, i79, i167, iconst_0, env, static) -{0,0}> main_LE_547(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167
main_JMP_647(i157, i79, i167, i197, env, static) -{1,1}> main_Load_675(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_Load_675(i157, i79, i167, i197, env, static) -{0,0}> main_Load_607(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197
main_LE_678(i157, i79, i211, i173, env, static) -{0,0}> main_LE_680(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_678(i157, i79, i212, i173, env, static) -{0,0}> main_LE_681(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 1 <= i173
main_LE_680(i157, i79, i211, i173, env, static) -{1,1}> main_Load_685(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_681(i157, i79, i212, i173, env, static) -{1,1}> main_Inc_687(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 0 < i212 && 1 <= i173
main_Load_685(i157, i79, i211, i173, env, static) -{1,1}> main_LE_691(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_Inc_687(i157, i79, i212, i173, env, static) -{1,1}> main_JMP_694(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i212 && 1 <= i173 && i212 + -1 = i219
main_LE_691(i157, i79, i211, i173, env, static) -{0,0}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_JMP_694(i157, i79, i219, i173, env, static) -{1,1}> main_Load_699(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173
main_Load_699(i157, i79, i219, i173, env, static) -{0,0}> main_Load_668(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173

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

obtained
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_48(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_48(i1, i3, env, static) -{1,1}> main_Load_56(i1, i3, env, static) :|: 0 >= 0
main_Load_56(i1, i3, env, static) -{0,0}> main_Load_58(i1, i3, env, static) :|: 0 >= 0
main_Load_58(i1, i3, env, static) -{0,0}> main_Load_60(i1, i3, env, static) :|: 0 <= static
main_Load_60(i1, i3, env, static) -{0,0}> main_Load_61(i1, i3, env, static) :|: 0 >= 0
main_Load_61(i1, i3, env, static) -{0,0}> main_Load_62(i1, i3, env, static) :|: 0 >= 0
main_Load_62(i1, i3, env, static) -{1,1}> main_LE_63(i1, i3, env, static) :|: 0 >= 0
main_LE_63(i1, i3, env, static) -{0,0}> main_LE_305(i1, i3, i3, env, static) :|: 0 >= 0
main_LE_305(i78, i79, i80, env, static) -{0,0}> main_LE_547(i78, i79, i78, i80, env, static) :|: 0 >= 0

obtained
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
by chaining
main_LE_547(i157, i79, i167, i159, env, static) -{0,0}> main_LE_549(i157, i79, i167, i159, env, static) :|: 1 <= i167
main_LE_549(i157, i79, i167, i159, env, static) -{1,1}> main_Load_551(i157, i79, i167, i159, env, static) :|: 1 <= i167 && 0 < i167
main_Load_551(i157, i79, i167, i159, env, static) -{1,1}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167

obtained
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173
by chaining
main_LE_553(i157, i79, i173, i167, env, static) -{0,0}> main_LE_555(i157, i79, i173, i167, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_555(i157, i79, i173, i167, env, static) -{1,1}> main_Load_559(i157, i79, i167, i173, env, static) :|: 0 < i173 && 1 <= i167 && 1 <= i173
main_Load_559(i157, i79, i167, i173, env, static) -{1,1}> main_Load_562(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_Load_562(i157, i79, i167, i173, env, static) -{1,1}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173

obtained
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
by chaining
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_574(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i173 < i167
main_LE_574(i157, i79, i167, i173, env, static) -{1,1}> main_Load_586(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173 && i173 < i167
main_Load_586(i157, i79, i167, i173, env, static) -{0,0}> main_Load_619(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173
main_Load_619(i157, i79, i180, i173, env, static) -{0,0}> main_Load_668(i157, i79, i180, i173, env, static) :|: 1 <= i180 && 1 <= i173

obtained
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i219', i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
by chaining
main_LE_678(i157, i79, i212, i173, env, static) -{0,0}> main_LE_681(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 1 <= i173
main_LE_681(i157, i79, i212, i173, env, static) -{1,1}> main_Inc_687(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 0 < i212 && 1 <= i173
main_Inc_687(i157, i79, i212, i173, env, static) -{1,1}> main_JMP_694(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i212 && 1 <= i173 && i212 + -1 = i219
main_JMP_694(i157, i79, i219, i173, env, static) -{1,1}> main_Load_699(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173
main_Load_699(i157, i79, i219, i173, env, static) -{0,0}> main_Load_668(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173

obtained
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
by chaining
main_LE_678(i157, i79, i211, i173, env, static) -{0,0}> main_LE_680(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_680(i157, i79, i211, i173, env, static) -{1,1}> main_Load_685(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_Load_685(i157, i79, i211, i173, env, static) -{1,1}> main_LE_691(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_691(i157, i79, i211, i173, env, static) -{0,0}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173

obtained
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
by chaining
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_572(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_LE_572(i157, i79, i167, i173, env, static) -{1,1}> main_Load_580(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_Load_580(i157, i79, i167, i173, env, static) -{0,0}> main_Load_607(i157, i79, i167, i173, env, static) :|: 0 <= i173 && 1 <= i167 && 1 <= i173

obtained
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i197', env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
by chaining
main_LE_623(i157, i79, i189, i167, env, static) -{0,0}> main_LE_628(i157, i79, i189, i167, env, static) :|: 0 <= i189 && 1 <= i189 && 1 <= i167
main_LE_628(i157, i79, i189, i167, env, static) -{1,1}> main_Inc_635(i157, i79, i167, i189, env, static) :|: 1 <= i189 && 0 < i189 && 1 <= i167
main_Inc_635(i157, i79, i167, i189, env, static) -{1,1}> main_JMP_647(i157, i79, i167, i197, env, static) :|: 1 <= i189 && 1 <= i167 && 0 <= i197 && i189 + -1 = i197
main_JMP_647(i157, i79, i167, i197, env, static) -{1,1}> main_Load_675(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197
main_Load_675(i157, i79, i167, i197, env, static) -{0,0}> main_Load_607(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197

obtained
main_LE_623(i157, i79, 0, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167
by chaining
main_LE_623(i157, i79, iconst_0, i167, env, static) -{0,0}> main_LE_627(i157, i79, iconst_0, i167, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i167
main_LE_627(i157, i79, iconst_0, i167, env, static) -{1,1}> main_Load_633(i157, i79, i167, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0 && 1 <= i167
main_Load_633(i157, i79, i167, iconst_0, env, static) -{1,1}> main_LE_643(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167
main_LE_643(i157, i79, i167, iconst_0, env, static) -{0,0}> main_LE_547(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167

(8) Obligation:

IntTrs with 13 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, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i219', i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i197', env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_623(i157, i79, 0, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167

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

Moved arithmethic from lhss to constraints.

main_LE_623(i157, i79, 0, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167
was transformed to
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167 && x = 0

(10) Obligation:

IntTrs with 13 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i219', i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i197', env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167 && x = 0
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173

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

Moved arithmethic from constraints to rhss.

main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i219', i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
was transformed to
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 + -1, i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212

main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i197', env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
was transformed to
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 + -1, env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189

(12) Obligation:

IntTrs with 13 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 + -1, i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167 && x = 0
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 + -1, env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173

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

Simplified expressions.

main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 + -1, env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
was transformed to
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 - 1, env, static) :|: i189 - 1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189

main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 + -1, i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
was transformed to
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 - 1, i173, env, static) :|: i212 - 1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212

main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167 && x = 0
was transformed to
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 1 <= i167 && x = 0

(14) Obligation:

IntTrs with 13 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 - 1, i173, env, static) :|: i212 - 1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 - 1, env, static) :|: i189 - 1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 1 <= i167 && x = 0
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173

(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) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 13 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 + -1, i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167 && x = 0
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 + -1, env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173

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

Simplified expressions.

(24) Obligation:

IntTrs with 13 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_547(i157, i79, i166, i159, env, static) -{0,0}> main_LE_548(i157, i79, i166, i159, env, static) :|: i166 <= 0
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i212 - 1, i173, env, static) :|: i212 - 1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i189 - 1, env, static) :|: i189 - 1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_623(i157, i79, x, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 1 <= i167 && x = 0
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_547(i157, i79, i167, i159, env, static) -{2,2}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167 && 0 < i167
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_553(i157, i79, i172, i167, env, static) -{0,0}> main_LE_554(i157, i79, i172, i167, env, static) :|: i172 <= 0 && 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{3,3}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i173 && 1 <= i167 && 0 < i173

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

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

(26) Obligation:

Set of 60 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 60 jbc graph edges to a weighted ITS with 60 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 60 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, env, static) -{0,0}> main_Load_3(i1, i3, env, static) :|: 0 >= 0
main_Load_3(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_21(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_21(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_28(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_39(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_39(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_48(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_48(i1, i3, env, static) -{1,1}> main_Load_56(i1, i3, env, static) :|: 0 >= 0
main_Load_56(i1, i3, env, static) -{0,0}> main_Load_58(i1, i3, env, static) :|: 0 >= 0
main_Load_58(i1, i3, env, static) -{0,0}> main_Load_60(i1, i3, env, static) :|: 0 <= static
main_Load_60(i1, i3, env, static) -{0,0}> main_Load_61(i1, i3, env, static) :|: 0 >= 0
main_Load_61(i1, i3, env, static) -{0,0}> main_Load_62(i1, i3, env, static) :|: 0 >= 0
main_Load_62(i1, i3, env, static) -{1,1}> main_LE_63(i1, i3, env, static) :|: 0 >= 0
main_LE_63(i1, i3, env, static) -{0,0}> main_LE_305(i1, i3, i3, env, static) :|: 0 >= 0
main_LE_305(i78, i79, i80, env, static) -{0,0}> main_LE_547(i78, i79, i78, i80, env, static) :|: 0 >= 0
main_LE_547(i157, i79, i167, i159, env, static) -{0,0}> main_LE_549(i157, i79, i167, i159, env, static) :|: 1 <= i167
main_LE_549(i157, i79, i167, i159, env, static) -{1,1}> main_Load_551(i157, i79, i167, i159, env, static) :|: 1 <= i167 && 0 < i167
main_Load_551(i157, i79, i167, i159, env, static) -{1,1}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{0,0}> main_LE_555(i157, i79, i173, i167, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_555(i157, i79, i173, i167, env, static) -{1,1}> main_Load_559(i157, i79, i167, i173, env, static) :|: 0 < i173 && 1 <= i167 && 1 <= i173
main_Load_559(i157, i79, i167, i173, env, static) -{1,1}> main_Load_562(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_Load_562(i157, i79, i167, i173, env, static) -{1,1}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_572(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{0,0}> main_LE_574(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i173 < i167
main_LE_572(i157, i79, i167, i173, env, static) -{1,1}> main_Load_580(i157, i79, i167, i173, env, static) :|: i167 <= i173 && 1 <= i167 && 1 <= i173
main_LE_574(i157, i79, i167, i173, env, static) -{1,1}> main_Load_586(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173 && i173 < i167
main_Load_580(i157, i79, i167, i173, env, static) -{0,0}> main_Load_607(i157, i79, i167, i173, env, static) :|: 0 <= i173 && 1 <= i167 && 1 <= i173
main_Load_586(i157, i79, i167, i173, env, static) -{0,0}> main_Load_619(i157, i79, i167, i173, env, static) :|: 2 <= i167 && 1 <= i167 && 1 <= i173
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_Load_619(i157, i79, i180, i173, env, static) -{0,0}> main_Load_668(i157, i79, i180, i173, env, static) :|: 1 <= i180 && 1 <= i173
main_LE_623(i157, i79, iconst_0, i167, env, static) -{0,0}> main_LE_627(i157, i79, iconst_0, i167, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{0,0}> main_LE_628(i157, i79, i189, i167, env, static) :|: 0 <= i189 && 1 <= i189 && 1 <= i167
main_LE_627(i157, i79, iconst_0, i167, env, static) -{1,1}> main_Load_633(i157, i79, i167, iconst_0, env, static) :|: iconst_0 <= 0 && iconst_0 = 0 && 1 <= i167
main_LE_628(i157, i79, i189, i167, env, static) -{1,1}> main_Inc_635(i157, i79, i167, i189, env, static) :|: 1 <= i189 && 0 < i189 && 1 <= i167
main_Load_633(i157, i79, i167, iconst_0, env, static) -{1,1}> main_LE_643(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167
main_Inc_635(i157, i79, i167, i189, env, static) -{1,1}> main_JMP_647(i157, i79, i167, i197, env, static) :|: 1 <= i189 && 1 <= i167 && 0 <= i197 && i189 + -1 = i197
main_LE_643(i157, i79, i167, iconst_0, env, static) -{0,0}> main_LE_547(i157, i79, i167, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i167
main_JMP_647(i157, i79, i167, i197, env, static) -{1,1}> main_Load_675(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_Load_675(i157, i79, i167, i197, env, static) -{0,0}> main_Load_607(i157, i79, i167, i197, env, static) :|: 1 <= i167 && 0 <= i197
main_LE_678(i157, i79, i211, i173, env, static) -{0,0}> main_LE_680(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_678(i157, i79, i212, i173, env, static) -{0,0}> main_LE_681(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 1 <= i173
main_LE_680(i157, i79, i211, i173, env, static) -{1,1}> main_Load_685(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_681(i157, i79, i212, i173, env, static) -{1,1}> main_Inc_687(i157, i79, i212, i173, env, static) :|: 1 <= i212 && 0 < i212 && 1 <= i173
main_Load_685(i157, i79, i211, i173, env, static) -{1,1}> main_LE_691(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_Inc_687(i157, i79, i212, i173, env, static) -{1,1}> main_JMP_694(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i212 && 1 <= i173 && i212 + -1 = i219
main_LE_691(i157, i79, i211, i173, env, static) -{0,0}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_JMP_694(i157, i79, i219, i173, env, static) -{1,1}> main_Load_699(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173
main_Load_699(i157, i79, i219, i173, env, static) -{0,0}> main_Load_668(i157, i79, i219, i173, env, static) :|: 0 <= i219 && 1 <= i173

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

obtained
main_LE_547(i157, i79, i167, i159, env, static) -{5,5}> main_LE_565(i157, i79, i167, i159, env, static) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
by chaining
main_LE_547(i157, i79, i167, i159, env, static) -{0,0}> main_LE_549(i157, i79, i167, i159, env, static) :|: 1 <= i167
main_LE_549(i157, i79, i167, i159, env, static) -{1,1}> main_Load_551(i157, i79, i167, i159, env, static) :|: 1 <= i167 && 0 < i167
main_Load_551(i157, i79, i167, i159, env, static) -{1,1}> main_LE_553(i157, i79, i159, i167, env, static) :|: 1 <= i167
main_LE_553(i157, i79, i173, i167, env, static) -{0,0}> main_LE_555(i157, i79, i173, i167, env, static) :|: 1 <= i167 && 1 <= i173
main_LE_555(i157, i79, i173, i167, env, static) -{1,1}> main_Load_559(i157, i79, i167, i173, env, static) :|: 0 < i173 && 1 <= i167 && 1 <= i173
main_Load_559(i157, i79, i167, i173, env, static) -{1,1}> main_Load_562(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173
main_Load_562(i157, i79, i167, i173, env, static) -{1,1}> main_LE_565(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173

(30) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, env, static) -{16,16}> main_LE_547(i1, i3, i1, i3, 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_547(i157, i79, i167, i159, env, static) -{5,5}> main_LE_565(i157, i79, i167, i159, env, static) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_668(i157, i79, i167, i173, env, static) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_Load_668(i157, i79, i200, i173, env, static) -{1,1}> main_LE_678(i157, i79, i200, i173, env, static) :|: 1 <= i173
main_LE_678(i157, i79, i212, i173, env, static) -{3,3}> main_Load_668(i157, i79, i219', i173, env, static) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_LE_678(i157, i79, i211, i173, env, static) -{2,2}> main_LE_547(i157, i79, i211, i173, env, static) :|: i211 <= 0 && 1 <= i173
main_LE_565(i157, i79, i167, i173, env, static) -{1,1}> main_Load_607(i157, i79, i167, i173, env, static) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_Load_607(i157, i79, i167, i179, env, static) -{1,1}> main_LE_623(i157, i79, i179, i167, env, static) :|: 0 <= i179 && 1 <= i167
main_LE_623(i157, i79, i189, i167, env, static) -{3,3}> main_Load_607(i157, i79, i167, i197', env, static) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_623(i157, i79, 0, i167, env, static) -{2,2}> main_LE_547(i157, i79, i167, 0, env, static) :|: 0 <= 0 && 1 <= i167

(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_547(x1, x2, x3, x4, x5, x6) → main_LE_547(x3, x4)
main_LE_565(x1, x2, x3, x4, x5, x6) → main_LE_565(x3, x4)
main_Load_668(x1, x2, x3, x4, x5, x6) → main_Load_668(x3, x4)
main_LE_678(x1, x2, x3, x4, x5, x6) → main_LE_678(x3, x4)
main_Load_607(x1, x2, x3, x4, x5, x6) → main_Load_607(x3, x4)
main_LE_623(x1, x2, x3, x4, x5, x6) → main_LE_623(x3, x4)

(32) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i3, static) -{16,16}> main_LE_547(i1, i3) :|: 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_547(i167, i159) -{5,5}> main_LE_565(i167, i159) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
main_LE_565(i167, i173) -{1,1}> main_Load_668(i167, i173) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_Load_668(i200, i173) -{1,1}> main_LE_678(i200, i173) :|: 1 <= i173
main_LE_678(i212, i173) -{3,3}> main_Load_668(i219', i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_LE_678(i211, i173) -{2,2}> main_LE_547(i211, i173) :|: i211 <= 0 && 1 <= i173
main_LE_565(i167, i173) -{1,1}> main_Load_607(i167, i173) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_Load_607(i167, i179) -{1,1}> main_LE_623(i179, i167) :|: 0 <= i179 && 1 <= i167
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i197') :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_623(0, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167

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

Moved arithmethic from lhss to constraints.

main_LE_623(0, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167
was transformed to
main_LE_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167 && x = 0

(34) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i197') :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_678(i212, i173) -{3,3}> main_Load_668(i219', i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_668(i200, i173) -{1,1}> main_LE_678(i200, i173) :|: 1 <= i173
main_LE_547(i167, i159) -{5,5}> main_LE_565(i167, i159) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
main_Load_607(i167, i179) -{1,1}> main_LE_623(i179, i167) :|: 0 <= i179 && 1 <= i167
main_LE_565(i167, i173) -{1,1}> main_Load_607(i167, i173) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_678(i211, i173) -{2,2}> main_LE_547(i211, i173) :|: i211 <= 0 && 1 <= i173
main_LE_565(i167, i173) -{1,1}> main_Load_668(i167, i173) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_Load_2(i1, i3, static) -{16,16}> main_LE_547(i1, i3) :|: 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_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167 && x = 0

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

Moved arithmethic from constraints to rhss.

main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i197') :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
was transformed to
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i189 + -1) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189

main_LE_678(i212, i173) -{3,3}> main_Load_668(i219', i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
was transformed to
main_LE_678(i212, i173) -{3,3}> main_Load_668(i212 + -1, i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212

(36) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i189 + -1) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
main_LE_678(i212, i173) -{3,3}> main_Load_668(i212 + -1, i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_LE_547(i167, i159) -{5,5}> main_LE_565(i167, i159) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
main_Load_668(i200, i173) -{1,1}> main_LE_678(i200, i173) :|: 1 <= i173
main_LE_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167 && x = 0
main_LE_678(i211, i173) -{2,2}> main_LE_547(i211, i173) :|: i211 <= 0 && 1 <= i173
main_LE_565(i167, i173) -{1,1}> main_Load_607(i167, i173) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_Load_607(i167, i179) -{1,1}> main_LE_623(i179, i167) :|: 0 <= i179 && 1 <= i167
main_Load_2(i1, i3, static) -{16,16}> main_LE_547(i1, i3) :|: 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_565(i167, i173) -{1,1}> main_Load_668(i167, i173) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167

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

Simplified expressions.

main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i189 + -1) :|: i189 + -1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189 && 0 <= i189
was transformed to
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i189 - 1) :|: i189 - 1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189

main_LE_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 0 <= 0 && 1 <= i167 && x = 0
was transformed to
main_LE_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 1 <= i167 && x = 0

main_Load_2(i1, i3, static) -{16,16}> main_LE_547(i1, i3) :|: 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, i3, static) -{16,16}> main_LE_547(i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_678(i212, i173) -{3,3}> main_Load_668(i212 + -1, i173) :|: i212 + -1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
was transformed to
main_LE_678(i212, i173) -{3,3}> main_Load_668(i212 - 1, i173) :|: i212 - 1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212

(38) Obligation:

IntTrs with 10 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_623(x, i167) -{2,2}> main_LE_547(i167, 0) :|: 1 <= i167 && x = 0
main_LE_678(i212, i173) -{3,3}> main_Load_668(i212 - 1, i173) :|: i212 - 1 = i219' && 0 <= i219' && 1 <= i173 && 0 < i212 && 1 <= i212
main_Load_668(i200, i173) -{1,1}> main_LE_678(i200, i173) :|: 1 <= i173
main_LE_547(i167, i159) -{5,5}> main_LE_565(i167, i159) :|: 0 < i167 && 1 <= i167 && 1 <= i159 && 0 < i159
main_Load_2(i1, i3, static) -{16,16}> main_LE_547(i1, i3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_Load_607(i167, i179) -{1,1}> main_LE_623(i179, i167) :|: 0 <= i179 && 1 <= i167
main_LE_565(i167, i173) -{1,1}> main_Load_607(i167, i173) :|: 1 <= i167 && 1 <= i173 && i167 <= i173 && 0 <= i173
main_LE_678(i211, i173) -{2,2}> main_LE_547(i211, i173) :|: i211 <= 0 && 1 <= i173
main_LE_565(i167, i173) -{1,1}> main_Load_668(i167, i173) :|: i173 < i167 && 1 <= i167 && 1 <= i173 && 2 <= i167
main_LE_623(i189, i167) -{3,3}> main_Load_607(i167, i189 - 1) :|: i189 - 1 = i197' && 1 <= i167 && 0 <= i197' && 0 < i189 && 1 <= i189

(39) koat Proof (EQUIVALENT transformation)

YES(?, 8*ar_0 + 24*ar_1 + 32)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 2) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 3) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 1) main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: ?, Cost: 5) main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 2) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 2 <= ar_0 ]
(Comp: ?, Cost: 3) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_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: 2) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 3) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 1) main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: 1, Cost: 5) main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 2) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 2 <= ar_0 ]
(Comp: ?, Cost: 3) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_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_Load_668) = 1
Pol(main_LE_678) = 1
Pol(main_Load_607) = 1
Pol(main_LE_623) = 1
Pol(main_LE_547) = 0
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_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\\ 1 <= ar_1 /\\ 0 <= i197' /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\\ 1 <= ar_1 /\\ 0 <= i197' /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-1) = ar_1
S("main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\\ 1 <= ar_1 /\\ 0 <= i197' /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-2) = ?
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 2 <= ar_0 ]", 0-0) = ar_0
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 2 <= ar_0 ]", 0-1) = ar_1
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 2 <= ar_0 ]", 0-2) = ?
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\\ 1 <= ar_1 ]", 0-0) = ar_0
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\\ 1 <= ar_1 ]", 0-1) = ar_1
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\\ 1 <= ar_1 ]", 0-2) = ?
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ 1 <= ar_1 /\\ ar_0 <= ar_1 /\\ 0 <= ar_1 ]", 0-0) = ar_0
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ 1 <= ar_1 /\\ ar_0 <= ar_1 /\\ 0 <= ar_1 ]", 0-1) = ar_1
S("main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\\ 1 <= ar_1 /\\ ar_0 <= ar_1 /\\ 0 <= ar_1 ]", 0-2) = ?
S("main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\\ 1 <= ar_0 ]", 0-0) = ar_1
S("main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\\ 1 <= ar_0 ]", 0-1) = ar_0
S("main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\\ 1 <= ar_0 ]", 0-2) = ?
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-0) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-1) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\\ 0 <= static''' /\\ static''' <= ar_2 + 2 /\\ 0 <= ar_2 /\\ 0 <= static'1 ]", 0-2) = ?
S("main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_1 ]", 0-0) = ar_0
S("main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_1 ]", 0-1) = ar_1
S("main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 1 <= ar_1 /\\ 0 < ar_1 ]", 0-2) = ?
S("main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]", 0-0) = ar_0
S("main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]", 0-1) = ar_1
S("main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]", 0-2) = ?
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\\ 0 <= i219' /\\ 1 <= ar_1 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-0) = ar_0
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\\ 0 <= i219' /\\ 1 <= ar_1 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-1) = ar_1
S("main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\\ 0 <= i219' /\\ 1 <= ar_1 /\\ 0 < ar_0 /\\ 1 <= ar_0 ]", 0-2) = ?
S("main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\\ ar_0 = 0 ]", 0-0) = ar_0
S("main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\\ ar_0 = 0 ]", 0-1) = 0
S("main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\\ ar_0 = 0 ]", 0-2) = ?
orients the transitions
main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_0 ]
main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
weakly and the transitions
main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 2, Cost: 2) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 3) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 1) main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: 1, Cost: 5) main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 /\ 0 <= ar_1 ]
(Comp: 2, Cost: 2) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 2 <= ar_0 ]
(Comp: ?, Cost: 3) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_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_623) = 2*V_1 + V_2
Pol(main_LE_547) = V_1 + 3*V_2
Pol(main_LE_678) = V_1 + 3*V_2
Pol(main_Load_668) = V_1 + 3*V_2
Pol(main_LE_565) = V_1 + 3*V_2
Pol(main_Load_2) = V_1 + 3*V_2
Pol(main_Load_607) = V_1 + 2*V_2 + 1
Pol(koat_start) = V_1 + 3*V_2
orients all transitions weakly and the transitions
main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: 2, Cost: 2) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
(Comp: ar_0 + 3*ar_1, Cost: 3) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 1) main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: 1, Cost: 5) main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ar_0 + 3*ar_1, Cost: 1) main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 /\ 0 <= ar_1 ]
(Comp: 2, Cost: 2) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 2 <= ar_0 ]
(Comp: ar_0 + 3*ar_1, Cost: 3) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_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: 2, Cost: 2) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_1, 0, arityPad)) [ 1 <= ar_1 /\ ar_0 = 0 ]
(Comp: ar_0 + 3*ar_1, Cost: 3) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0 - 1, ar_1, arityPad)) [ ar_0 - 1 = i219' /\ 0 <= i219' /\ 1 <= ar_1 /\ 0 < ar_0 /\ 1 <= ar_0 ]
(Comp: ar_0 + 3*ar_1 + 1, Cost: 1) main_Load_668(ar_0, ar_1, ar_2) -> Com_1(main_LE_678(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: 1, Cost: 5) main_LE_547(ar_0, ar_1, ar_2) -> Com_1(main_LE_565(ar_0, ar_1, arityPad)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ar_0 + 3*ar_1, Cost: 1) main_Load_607(ar_0, ar_1, ar_2) -> Com_1(main_LE_623(ar_1, ar_0, arityPad)) [ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_0, ar_1, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 /\ 0 <= ar_1 ]
(Comp: 2, Cost: 2) main_LE_678(ar_0, ar_1, ar_2) -> Com_1(main_LE_547(ar_0, ar_1, arityPad)) [ ar_0 <= 0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 1) main_LE_565(ar_0, ar_1, ar_2) -> Com_1(main_Load_668(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 2 <= ar_0 ]
(Comp: ar_0 + 3*ar_1, Cost: 3) main_LE_623(ar_0, ar_1, ar_2) -> Com_1(main_Load_607(ar_1, ar_0 - 1, arityPad)) [ ar_0 - 1 = i197' /\ 1 <= ar_1 /\ 0 <= i197' /\ 0 < ar_0 /\ 1 <= ar_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 8*ar_0 + 24*ar_1 + 32

Time: 0.155 sec (SMT: 0.137 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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(3)) 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) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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, 32 + 8 * |#0| + 24 * |#1|)