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

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 274 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(7)), 0 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 74 ms)
    ↳6 WeightedIntTrs
        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 19 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), 0 ms)
        ↳14 WeightedIntTrs
    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 75 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 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)
        ↳22 WeightedIntTrs
        ↳23 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳24 WeightedIntTrs
        ↳25 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳26 WeightedIntTrs
↳27 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(7)), 0 ms)
↳28 JBCComplexityEdges
    ↳29 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 69 ms)
    ↳30 WeightedIntTrs
    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 18 ms)
    ↳32 WeightedIntTrs
    ↳33 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 25 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 (⇔, 73 ms)
    ↳40 BOUNDS(CONSTANT, 24 + 8 * |#0|)

(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 PastaB5 {
    public static void main(int x) {
        while (x > 0 && (x % 2) == 0) {
            x--;
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaB5.main(I)V: Graph of 56 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 49 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 49 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i12 < iconst_2
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i35 <= 1 && i35 < iconst_2 && iconst_2 = 2
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

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

obtained
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0

obtained
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i12' < 2 && i12' <= 1 && 0 <= i12'
by chaining
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i12 < iconst_2

obtained
main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
by chaining
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10

obtained
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
by chaining
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i35 <= 1 && i35 < iconst_2 && iconst_2 = 2

obtained
main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'
by chaining
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i12' < 2 && i12' <= 1 && 0 <= i12'
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'

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

Moved arithmethic from lhss to constraints.

main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0

main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i12' < 2 && i12' <= 1 && 0 <= i12'
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

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

Moved arithmethic from constraints to rhss.

main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0

main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1

main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0

main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1

main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
was transformed to
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i12' < 2 && i12' <= 1 && 0 <= i12'
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

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

Simplified expressions.

main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 - 1, env, static) :|: 0 <= i14' && 1 <= i10 && i10 - 1 = i14' && x = 0

main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
was transformed to
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'

main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 - 1, env, static) :|: 1 <= i25 && 0 <= i46' && 2 <= i26 && 1 <= i26 && i25 - 1 = i46' && x = 0

main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && 0 <= iconst_1 && iconst_1 = 1

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

main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_1 && iconst_1 = 1

(14) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i12' < 2 && i12' <= 1 && 0 <= i12'
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 - 1, env, static) :|: 0 <= i14' && 1 <= i10 && i10 - 1 = i14' && x = 0
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_1 && iconst_1 = 1
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 2 <= i26 && i35' < 2 && 1 <= i25 && i35' <= 1 && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && 0 <= iconst_1 && iconst_1 = 1
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 - 1, env, static) :|: 1 <= i25 && 0 <= i46' && 2 <= i26 && 1 <= i26 && i25 - 1 = i46' && x = 0

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

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

(16) Obligation:

IntTrs with 49 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i10 % iconst_2 = i12
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i25 % iconst_2 = i35 && i35 <= 1 && iconst_2 = 2
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

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

obtained
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0

obtained
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i10 % 2 = i12' && i12' <= 1 && 0 <= i12'
by chaining
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i10 % iconst_2 = i12

obtained
main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
by chaining
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10

obtained
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 % 2 = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
by chaining
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i25 % iconst_2 = i35 && i35 <= 1 && iconst_2 = 2

obtained
main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'
by chaining
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

(18) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i10 % 2 = i12' && i12' <= 1 && 0 <= i12'
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 % 2 = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'

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

Moved arithmethic from lhss to constraints.

main_NE_145(i26, 0, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46'
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0

main_NE_68(i10, 0, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14'
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0

(20) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i10 % 2 = i12' && i12' <= 1 && 0 <= i12'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 % 2 = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

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

Removed div and mod.

main_LE_52(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: 1 <= i10 && 0 < i10 && i10 % 2 = i12' && i12' <= 1 && 0 <= i12'
was transformed to
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'

main_LE_88(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 % 2 = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
was transformed to
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'

(22) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

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

Moved arithmethic from constraints to rhss.

main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i35', i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
was transformed to
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i25 - 2 * div, i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'

main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i46', env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0

main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, iconst_1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1

main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i12', env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
was transformed to
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i10 - 2 * div, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'

main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, iconst_1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1

main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i14', env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0

main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
was transformed to
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

(24) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i25 - 2 * div, i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i10 - 2 * div, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, 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_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0

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

Simplified expressions.

main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i10 - 2 * div, env, static) :|: i10 - 2 * div < 2 && i10 - 2 * div + 2 > 0 && 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
was transformed to
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i10 + -2 * div, env, static) :|: i10 + -2 * div < 2 && 0 < i10 + -2 * div + 2 && 1 <= i10 && 0 < i10 && i10 + -2 * div = i12' && i12' <= 1 && 0 <= i12'

main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 + -1, env, static) :|: 0 <= 0 && 0 <= i14' && 1 <= i10 && 0 <= 1 && i10 + -1 = i14' && x = 0
was transformed to
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 - 1, env, static) :|: 0 <= i14' && 1 <= i10 && i10 - 1 = i14' && x = 0

main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 + -1, env, static) :|: 1 <= i25 && 0 <= i46' && 0 <= 1 && 2 <= i26 && 1 <= i26 && 0 <= 0 && i25 + -1 = i46' && x = 0
was transformed to
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 - 1, env, static) :|: 1 <= i25 && 0 <= i46' && 2 <= i26 && 1 <= i26 && i25 - 1 = i46' && x = 0

main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 - 2 * div = i12' && i12' <= 1 && 0 <= i12'
was transformed to
main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 + -2 * div = i12' && i12' <= 1 && 0 <= i12'

main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
was transformed to
main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 + -2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'

main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i25 - 2 * div, i25, env, static) :|: i25 - 2 * div < 2 && i25 - 2 * div + 2 > 0 && 0 <= i25 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 - 2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
was transformed to
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i25 + -2 * div, i25, env, static) :|: i25 + -2 * div < 2 && 0 < i25 + -2 * div + 2 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 + -2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'

main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && 0 <= iconst_1 && iconst_1 = 1

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

main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1
was transformed to
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_1 && iconst_1 = 1

(26) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_88(i10, iconst_0, env, static) -{0,0}> main_LE_90(i10, 0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 = 0
main_LE_88'(i26, i25, env, static) -{4,4}> main_NE_145(i26, i25 + -2 * div, i25, env, static) :|: i25 + -2 * div < 2 && 0 < i25 + -2 * div + 2 && 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 + -2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_LE_52'(i10, env, static) -{4,4}> main_NE_68(i10, i10 + -2 * div, env, static) :|: i10 + -2 * div < 2 && 0 < i10 + -2 * div + 2 && 1 <= i10 && 0 < i10 && i10 + -2 * div = i12' && i12' <= 1 && 0 <= i12'
main_NE_68(i10, x, env, static) -{4,4}> main_LE_88(i10, i10 - 1, env, static) :|: 0 <= i14' && 1 <= i10 && i10 - 1 = i14' && x = 0
main_LE_52(i10, env, static) -{4,4}> main_LE_52'(i10, env, static) :|: 1 <= i10 && 0 < i10 && i10 + -2 * div = i12' && i12' <= 1 && 0 <= i12'
main_NE_145(i26, iconst_1, i25, env, static) -{0,0}> main_NE_147(i26, 1, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_1 && iconst_1 = 1
main_LE_88(i26, i25, env, static) -{4,4}> main_LE_88'(i26, i25, env, static) :|: 2 <= i26 && i35' <= 1 && 1 <= i25 && i25 + -2 * div = i35' && 0 < i25 && 1 <= i26 && 0 <= i35'
main_NE_68(i10, iconst_1, env, static) -{0,0}> main_NE_70(i10, 1, env, static) :|: 1 <= i10 && 0 <= iconst_1 && iconst_1 = 1
main_Load_2(i2, env, static) -{16,16}> main_LE_52(i2, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_52(i9, env, static) -{0,0}> main_LE_54(i9, env, static) :|: i9 <= 0
main_NE_145(i26, x, i25, env, static) -{4,4}> main_LE_88(i26, i25 - 1, env, static) :|: 1 <= i25 && 0 <= i46' && 2 <= i26 && 1 <= i26 && i25 - 1 = i46' && x = 0

(27) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(7)) transformation)

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

(28) Obligation:

Set of 45 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 45 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i12 < iconst_2
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i35 <= 1 && i35 < iconst_2 && iconst_2 = 2
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

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

obtained
main_Load_2(i2, env, static) -{24,24}> main_LE_88(i2, i14', env, static'1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_41(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i2, env, static) -{1,1}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 <= static
main_Load_47(i2, env, static) -{0,0}> main_Load_50(i2, env, static) :|: 0 >= 0
main_Load_50(i2, env, static) -{0,0}> main_Load_51(i2, env, static) :|: 0 >= 0
main_Load_51(i2, env, static) -{1,1}> main_LE_52(i2, env, static) :|: 0 >= 0
main_LE_52(i10, env, static) -{0,0}> main_LE_55(i10, env, static) :|: 1 <= i10
main_LE_55(i10, env, static) -{1,1}> main_Load_59(i10, env, static) :|: 1 <= i10 && 0 < i10
main_Load_59(i10, env, static) -{1,1}> main_ConstantStackPush_63(i10, env, static) :|: 1 <= i10
main_ConstantStackPush_63(i10, env, static) -{1,1}> main_IntArithmetic_64(i10, iconst_2, env, static) :|: 1 <= i10 && iconst_2 = 2
main_IntArithmetic_64(i10, iconst_2, env, static) -{1,1}> main_NE_68(i10, i12, env, static) :|: 1 <= i10 && 0 <= i12 && iconst_2 = 2 && i12 <= 1 && i12 < iconst_2
main_NE_68(i10, iconst_0, env, static) -{0,0}> main_NE_71(i10, iconst_0, env, static) :|: 1 <= i10 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_71(i10, iconst_0, env, static) -{1,1}> main_Inc_77(i10, env, static) :|: 1 <= i10 && iconst_0 = 0
main_Inc_77(i10, env, static) -{1,1}> main_JMP_79(i10, i14, env, static) :|: 0 <= i14 && i10 + -1 = i14 && 1 <= i10
main_JMP_79(i10, i14, env, static) -{1,1}> main_Load_80(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10
main_Load_80(i10, i14, env, static) -{1,1}> main_LE_88(i10, i14, env, static) :|: 0 <= i14 && 1 <= i10

obtained
main_LE_88(i26, i25, env, static) -{8,8}> main_LE_88(i26, i46', env, static) :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'
by chaining
main_LE_88(i26, i25, env, static) -{0,0}> main_LE_91(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i25 && 1 <= i26
main_LE_91(i26, i25, env, static) -{1,1}> main_Load_126(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 < i25
main_Load_126(i26, i25, env, static) -{1,1}> main_ConstantStackPush_131(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26
main_ConstantStackPush_131(i26, i25, env, static) -{1,1}> main_IntArithmetic_135(i26, i25, iconst_2, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_2 = 2
main_IntArithmetic_135(i26, i25, iconst_2, env, static) -{1,1}> main_NE_145(i26, i35, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i35 && i35 <= 1 && i35 < iconst_2 && iconst_2 = 2
main_NE_145(i26, iconst_0, i25, env, static) -{0,0}> main_NE_148(i26, iconst_0, i25, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_NE_148(i26, iconst_0, i25, env, static) -{1,1}> main_Inc_158(i26, i25, env, static) :|: 1 <= i25 && 2 <= i26 && iconst_0 = 0
main_Inc_158(i26, i25, env, static) -{1,1}> main_JMP_164(i26, i46, env, static) :|: 1 <= i25 && 2 <= i26 && 0 <= i46 && i25 + -1 = i46
main_JMP_164(i26, i46, env, static) -{1,1}> main_Load_168(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_Load_168(i26, i46, env, static) -{1,1}> main_LE_681(i26, i46, env, static) :|: 2 <= i26 && 0 <= i46
main_LE_681(i26, i46, env, static) -{0,0}> main_LE_88(i26, i46, env, static) :|: 2 <= i26 && 1 <= i26 && 0 <= i46

(32) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, env, static) -{24,24}> main_LE_88(i2, i14', env, static'1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_88(i26, i25, env, static) -{8,8}> main_LE_88(i26, i46', env, static) :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'

(33) 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) → main_Load_2(x1, x3)
main_LE_88(x1, x2, x3, x4) → main_LE_88(x1, x2)

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i14') :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i46') :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'

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

Moved arithmethic from constraints to rhss.

main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i14') :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i2 + -1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2

main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i46') :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'
was transformed to
main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i25 + -1) :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i2 + -1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i25 + -1) :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'

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

Simplified expressions.

main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i2 + -1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 + -1 = i14' && 0 >= 0 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i2 - 1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 - 1 = i14' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i25 + -1) :|: 0 < 2 && 0 <= i46' && 0 <= i25 && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && 0 <= 1 && 0 <= 0 && i25 + -1 = i46'
was transformed to
main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i25 - 1) :|: 0 <= i46' && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && i25 - 1 = i46'

(38) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_LE_88(i26, i25) -{8,8}> main_LE_88(i26, i25 - 1) :|: 0 <= i46' && 2 <= i26 && 1 <= i26 && 0 < i25 && 1 <= i25 && i25 - 1 = i46'
main_Load_2(i2, static) -{24,24}> main_LE_88(i2, i2 - 1) :|: 0 < i2 && 0 <= i14' && 1 <= i2 && static'1 <= static''' + 1 && i2 - 1 = i14' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(39) koat Proof (EQUIVALENT transformation)

YES(?, 8*ar_0 + 24)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) main_LE_88(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_1 - 1)) [ 0 <= i46' /\ 2 <= ar_0 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ ar_1 - 1 = i46' ]
(Comp: ?, Cost: 24) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_0 - 1)) [ 0 < ar_0 /\ 0 <= i14' /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i14' /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 8) main_LE_88(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_1 - 1)) [ 0 <= i46' /\ 2 <= ar_0 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ ar_1 - 1 = i46' ]
(Comp: 1, Cost: 24) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_0 - 1)) [ 0 < ar_0 /\ 0 <= i14' /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i14' /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_LE_88) = V_2
Pol(main_Load_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_LE_88(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_1 - 1)) [ 0 <= i46' /\ 2 <= ar_0 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ ar_1 - 1 = i46' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0, Cost: 8) main_LE_88(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_1 - 1)) [ 0 <= i46' /\ 2 <= ar_0 /\ 1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_1 /\ ar_1 - 1 = i46' ]
(Comp: 1, Cost: 24) main_Load_2(ar_0, ar_1) -> Com_1(main_LE_88(ar_0, ar_0 - 1)) [ 0 < ar_0 /\ 0 <= i14' /\ 1 <= ar_0 /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i14' /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1) -> Com_1(main_Load_2(ar_0, ar_1)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 8*ar_0 + 24

Time: 0.116 sec (SMT: 0.111 sec)

(40) BOUNDS(CONSTANT, 24 + 8 * |#0|)