time complexity proof of /tmp/tmplrlMNa/UnionFindIterative.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 34 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 koat Proof (⇔, 42 ms)

    ↳16 BOUNDS(CONSTANT, 34 + 51 * |#0|)

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

↳18 JBCComplexityEdges

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 135 ms)

    ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 5 ms)

        ↳26 WeightedIntTrs

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

    ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

        ↳33 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 1 ms)

        ↳34 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Based on union-find data structures with a self-loop as sentinel,
 * as presented on
 * http://en.wikipedia.org/w/index.php?title=Disjoint-set_data_structure&oldid=558948590
 *
 * Non-recursive version.
 */
public class UnionFindIterative {
    private UnionFindIterative parent;

    public UnionFindIterative(UnionFindIterative parent) {
        this.parent = parent;
    }

    public void makeSet() {
        this.parent = this;
    }

    /**
     * Here you need to know about this that the only panhandle list
     * you can possibly reach from this has a "pan" which is a self-loop.
     */
    public UnionFindIterative find() {
        UnionFindIterative candidate = this;
        while (candidate.parent != candidate) {
            candidate = candidate.parent;
        }
        return candidate;
    }

    public void union(UnionFindIterative y) {
        UnionFindIterative xRoot = this.find();
        UnionFindIterative yRoot = y.find();
        xRoot.parent = yRoot;
    }

    public static void main(int j) {
        UnionFindIterative y = new UnionFindIterative(null);
        y.makeSet();
        for (int i = 0; i < j; ++i) {
            UnionFindIterative x = new UnionFindIterative(null);
            x.makeSet();
            x.union(y);
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- UnionFindIterative: [parent]

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 98 rules
Start term: main_New_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, env, static) -{0,0}> main_New_4(i2, env, static) :|: 0 >= 0
main_New_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(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_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_New_45(i2, env, static) :|: 0 >= 0
main_New_45(i2, env, static) -{0,0}> main_New_47(i2, env, static) :|: 0 >= 0
main_New_47(i2, env, static) -{0,0}> main_New_50(i2, env, static) :|: 0 <= static
main_New_50(i2, env, static) -{0,0}> main_New_51(i2, env, static) :|: 0 >= 0
main_New_51(i2, env, static) -{0,0}> main_New_52(i2, env, static) :|: 0 >= 0
main_New_52(i2, env, static) -{1,1}> main_Duplicate_53(i2, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_53(i2, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_55(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_55(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_57(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_57(i2, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_59(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_59(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_63(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_63(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Return_70(i2, o4', NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(i2, o4, NULL, env, static) -{1,1}> main_Store_73(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_73(i2, o4, NULL, env, static) -{1,1}> main_Load_74(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_74(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_75(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_75(i2, o4, NULL, env, static) -{1,1}> makeSet_Load_76(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_76(o4, i2, NULL, env, static) -{1,1}> makeSet_Load_77(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_77(o4, i2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_FieldAccess_78(o4, i2, NULL, env, static) -{1,1}> makeSet_Return_80(i2, o4', env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
makeSet_Return_80(i2, o4, env, static) -{1,1}> main_ConstantStackPush_83(i2, o4, env, static) :|: 0 < o4
main_ConstantStackPush_83(i2, o4, env, static) -{1,1}> main_Store_84(i2, iconst_0, o4, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_84(i2, iconst_0, o4, env, static) -{1,1}> main_Load_85(i2, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_85(i2, o4, iconst_0, env, static) -{0,0}> main_Load_242(i2, o4, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0
main_Load_242(i13, o77, i14, env, static) -{0,0}> main_Load_368(i13, o77, i14, env, static) :|: 0 <= i14 && i14 <= 1 && i14 <= 2 && 0 < o77
main_Load_368(i22, o153, i23, env, static) -{0,0}> main_Load_521(i22, o153, i23, env, static) :|: i23 <= 2 && 0 < o153 && 0 <= i23
main_Load_521(i30, o230, i31, env, static) -{1,1}> main_Load_528(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_Load_528(i30, i31, o230, env, static) -{1,1}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_538(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30
main_GE_538(i30, i31, o230, env, static) -{1,1}> main_New_553(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30 && 1 <= i30
main_New_553(i30, o230, i31, env, static) -{1,1}> main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30 && o236 = 1
main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Return_574(i30, o236', o230, i31, NULL, env, static) :|: NULL = 0 && o236' <= o236 + NULL && 0 < o230 && 0 <= i31 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236 + NULL
langle_init_rangle_Return_574(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Store_576(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Store_576(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Load_578(i30, o230, i31, o236, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_578(i30, o230, i31, o236, NULL, env, static) -{1,1}> main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Return_600(i30, o230, i31, o236', env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && o236' <= o236 + o236 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236
makeSet_Return_600(i30, o230, i31, o236, env, static) -{1,1}> main_Load_602(i30, o230, i31, o236, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_602(i30, o230, i31, o236, env, static) -{1,1}> main_Load_604(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_604(i30, o236, o230, i31, env, static) -{1,1}> main_InvokeMethod_614(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_614(i30, o236, o230, i31, env, static) -{1,1}> union_Load_615(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_615(o236, o230, i30, i31, env, static) -{1,1}> union_InvokeMethod_617(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_617(o236, o230, i30, i31, env, static) -{1,1}> find_Load_618(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_618(o236, o230, i30, i31, env, static) -{1,1}> find_Store_619(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_619(o236, o230, i30, i31, env, static) -{1,1}> find_Load_620(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_620(o236, o230, i30, i31, env, static) -{1,1}> find_FieldAccess_621(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_621(o236, o230, i30, i31, env, static) -{1,1}> find_Load_622(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_622(o236, o230, i30, i31, env, static) -{1,1}> find_EQ_623(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_623(o236, o230, i30, i31, env, static) -{1,1}> find_Load_624(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_624(o236, o230, i30, i31, env, static) -{1,1}> find_Return_625(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_625(o236, o230, i30, i31, env, static) -{1,1}> union_Store_626(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_626(o236, o230, i30, i31, env, static) -{1,1}> union_Load_627(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_627(o230, o236, i30, i31, env, static) -{1,1}> union_InvokeMethod_628(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_628(o230, o236, i30, i31, env, static) -{1,1}> find_Load_629(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_629(o230, o236, i30, i31, env, static) -{1,1}> find_Store_674(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_674(o230, o236, i30, i31, env, static) -{1,1}> find_Load_688(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_688(o230, o236, i30, i31, env, static) -{1,1}> find_FieldAccess_689(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_689(o230, o236, i30, i31, env, static) -{1,1}> find_Load_690(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_690(o230, o236, i30, i31, env, static) -{1,1}> find_EQ_691(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_691(o230, o236, i30, i31, env, static) -{1,1}> find_Load_692(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_692(o230, o236, i30, i31, env, static) -{1,1}> find_Return_705(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_705(o230, o236, i30, i31, env, static) -{1,1}> union_Store_707(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_707(o230, o236, i30, i31, env, static) -{1,1}> union_Load_708(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_708(o236, o230, i30, i31, env, static) -{1,1}> union_Load_710(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_710(o236, o230, i30, i31, env, static) -{1,1}> union_FieldAccess_712(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_FieldAccess_712(o236, o230, i30, i31, env, static) -{1,1}> union_Return_713(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Return_713(i30, o230, i31, env, static) -{1,1}> main_Inc_715(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30
main_Inc_715(i30, o230, i31, env, static) -{1,1}> main_JMP_719(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30 && 1 <= i38 && i31 + 1 = i38
main_JMP_719(i30, o230, i38, env, static) -{1,1}> main_Load_730(i30, o230, i38, env, static) :|: 0 < o230 && 1 <= i30 && 1 <= i38
main_Load_730(i30, o230, i38, env, static) -{0,0}> main_Load_521(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i38 && 1 <= i30 && 1 <= i38

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

obtained
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, o4'1, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
by chaining
main_New_2(i2, env, static) -{0,0}> main_New_4(i2, env, static) :|: 0 >= 0
main_New_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(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_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_New_45(i2, env, static) :|: 0 >= 0
main_New_45(i2, env, static) -{0,0}> main_New_47(i2, env, static) :|: 0 >= 0
main_New_47(i2, env, static) -{0,0}> main_New_50(i2, env, static) :|: 0 <= static
main_New_50(i2, env, static) -{0,0}> main_New_51(i2, env, static) :|: 0 >= 0
main_New_51(i2, env, static) -{0,0}> main_New_52(i2, env, static) :|: 0 >= 0
main_New_52(i2, env, static) -{1,1}> main_Duplicate_53(i2, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_53(i2, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_55(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_55(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_57(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_57(i2, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_59(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_59(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_63(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_63(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Return_70(i2, o4', NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(i2, o4, NULL, env, static) -{1,1}> main_Store_73(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_73(i2, o4, NULL, env, static) -{1,1}> main_Load_74(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_74(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_75(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_75(i2, o4, NULL, env, static) -{1,1}> makeSet_Load_76(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_76(o4, i2, NULL, env, static) -{1,1}> makeSet_Load_77(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_77(o4, i2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_FieldAccess_78(o4, i2, NULL, env, static) -{1,1}> makeSet_Return_80(i2, o4', env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
makeSet_Return_80(i2, o4, env, static) -{1,1}> main_ConstantStackPush_83(i2, o4, env, static) :|: 0 < o4
main_ConstantStackPush_83(i2, o4, env, static) -{1,1}> main_Store_84(i2, iconst_0, o4, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_84(i2, iconst_0, o4, env, static) -{1,1}> main_Load_85(i2, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_85(i2, o4, iconst_0, env, static) -{0,0}> main_Load_242(i2, o4, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0
main_Load_242(i13, o77, i14, env, static) -{0,0}> main_Load_368(i13, o77, i14, env, static) :|: 0 <= i14 && i14 <= 1 && i14 <= 2 && 0 < o77
main_Load_368(i22, o153, i23, env, static) -{0,0}> main_Load_521(i22, o153, i23, env, static) :|: i23 <= 2 && 0 < o153 && 0 <= i23

obtained
main_Load_521(i30, o230, i31, env, static) -{51,51}> main_Load_521(i30, o230, i38', env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
by chaining
main_Load_521(i30, o230, i31, env, static) -{1,1}> main_Load_528(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_Load_528(i30, i31, o230, env, static) -{1,1}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_538(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30
main_GE_538(i30, i31, o230, env, static) -{1,1}> main_New_553(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30 && 1 <= i30
main_New_553(i30, o230, i31, env, static) -{1,1}> main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30 && o236 = 1
main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Return_574(i30, o236', o230, i31, NULL, env, static) :|: NULL = 0 && o236' <= o236 + NULL && 0 < o230 && 0 <= i31 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236 + NULL
langle_init_rangle_Return_574(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Store_576(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Store_576(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Load_578(i30, o230, i31, o236, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_578(i30, o230, i31, o236, NULL, env, static) -{1,1}> main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Return_600(i30, o230, i31, o236', env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && o236' <= o236 + o236 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236
makeSet_Return_600(i30, o230, i31, o236, env, static) -{1,1}> main_Load_602(i30, o230, i31, o236, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_602(i30, o230, i31, o236, env, static) -{1,1}> main_Load_604(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_604(i30, o236, o230, i31, env, static) -{1,1}> main_InvokeMethod_614(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_614(i30, o236, o230, i31, env, static) -{1,1}> union_Load_615(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_615(o236, o230, i30, i31, env, static) -{1,1}> union_InvokeMethod_617(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_617(o236, o230, i30, i31, env, static) -{1,1}> find_Load_618(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_618(o236, o230, i30, i31, env, static) -{1,1}> find_Store_619(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_619(o236, o230, i30, i31, env, static) -{1,1}> find_Load_620(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_620(o236, o230, i30, i31, env, static) -{1,1}> find_FieldAccess_621(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_621(o236, o230, i30, i31, env, static) -{1,1}> find_Load_622(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_622(o236, o230, i30, i31, env, static) -{1,1}> find_EQ_623(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_623(o236, o230, i30, i31, env, static) -{1,1}> find_Load_624(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_624(o236, o230, i30, i31, env, static) -{1,1}> find_Return_625(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_625(o236, o230, i30, i31, env, static) -{1,1}> union_Store_626(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_626(o236, o230, i30, i31, env, static) -{1,1}> union_Load_627(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_627(o230, o236, i30, i31, env, static) -{1,1}> union_InvokeMethod_628(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_628(o230, o236, i30, i31, env, static) -{1,1}> find_Load_629(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_629(o230, o236, i30, i31, env, static) -{1,1}> find_Store_674(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_674(o230, o236, i30, i31, env, static) -{1,1}> find_Load_688(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_688(o230, o236, i30, i31, env, static) -{1,1}> find_FieldAccess_689(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_689(o230, o236, i30, i31, env, static) -{1,1}> find_Load_690(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_690(o230, o236, i30, i31, env, static) -{1,1}> find_EQ_691(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_691(o230, o236, i30, i31, env, static) -{1,1}> find_Load_692(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_692(o230, o236, i30, i31, env, static) -{1,1}> find_Return_705(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_705(o230, o236, i30, i31, env, static) -{1,1}> union_Store_707(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_707(o230, o236, i30, i31, env, static) -{1,1}> union_Load_708(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_708(o236, o230, i30, i31, env, static) -{1,1}> union_Load_710(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_710(o236, o230, i30, i31, env, static) -{1,1}> union_FieldAccess_712(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_FieldAccess_712(o236, o230, i30, i31, env, static) -{1,1}> union_Return_713(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Return_713(i30, o230, i31, env, static) -{1,1}> main_Inc_715(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30
main_Inc_715(i30, o230, i31, env, static) -{1,1}> main_JMP_719(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30 && 1 <= i38 && i31 + 1 = i38
main_JMP_719(i30, o230, i38, env, static) -{1,1}> main_Load_730(i30, o230, i38, env, static) :|: 0 < o230 && 1 <= i30 && 1 <= i38
main_Load_730(i30, o230, i38, env, static) -{0,0}> main_Load_521(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i38 && 1 <= i30 && 1 <= i38

(8) Obligation:

IntTrs with 2 rules
Start term: main_New_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, o4'1, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{51,51}> main_Load_521(i30, o230, i38', env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30

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

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

main_New_2(x1, x2, x3) → main_New_2(x1, x3)
main_Load_521(x1, x2, x3, x4, x5) → main_Load_521(x1, x2, x3)

(10) Obligation:

IntTrs with 2 rules
Start term: main_New_2(#0, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, static) -{34,34}> main_Load_521(i2, o4'1, 0) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i38') :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30

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

Moved arithmethic from constraints to rhss.

main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i38') :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
was transformed to
main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i31 + 1) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30

main_New_2(i2, static) -{34,34}> main_Load_521(i2, o4'1, 0) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_2(i2, static) -{34,34}> main_Load_521(i2, 1 + 0, 0) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1

(12) Obligation:

IntTrs with 2 rules
Start term: main_New_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i31 + 1) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
main_New_2(i2, static) -{34,34}> main_Load_521(i2, 1 + 0, 0) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1

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

Simplified expressions.

main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i31 + 1) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
was transformed to
main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i31 + 1) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 && 1 <= i30 && o236'1 <= 2 * o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 <= i31 && i31 < i30

main_New_2(i2, static) -{34,34}> main_Load_521(i2, 1 + 0, 0) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_2(i2, static) -{34,34}> main_Load_521(i2, 1, 0) :|: 0 < o4'1 && 0 <= static'1 && o4'1 <= 2 * o4'1 && 0 <= static && o4'1 = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(14) Obligation:

IntTrs with 2 rules
Start term: main_New_2(#0, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, static) -{34,34}> main_Load_521(i2, 1, 0) :|: 0 < o4'1 && 0 <= static'1 && o4'1 <= 2 * o4'1 && 0 <= static && o4'1 = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_Load_521(i30, o230, i31) -{51,51}> main_Load_521(i30, o230, i31 + 1) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 && 1 <= i30 && o236'1 <= 2 * o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 <= i31 && i31 < i30

(15) koat Proof (EQUIVALENT transformation)

YES(?, 51*ar_0 + 34)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 34) main_New_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, 1, 0)) [ 0 < o4'1 /\ 0 <= static'1 /\ o4'1 <= 2*o4'1 /\ 0 <= ar_1 /\ o4'1 = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 51) main_Load_521(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i38' /\ 1 <= i38' /\ o236'1 = 1 /\ 1 <= ar_0 /\ o236'1 <= 2*o236'1 /\ 0 < ar_1 /\ 0 <= i38' /\ 0 < o236'1 /\ 0 <= ar_2 /\ ar_2 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_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: 1, Cost: 34) main_New_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, 1, 0)) [ 0 < o4'1 /\ 0 <= static'1 /\ o4'1 <= 2*o4'1 /\ 0 <= ar_1 /\ o4'1 = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 51) main_Load_521(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i38' /\ 1 <= i38' /\ o236'1 = 1 /\ 1 <= ar_0 /\ o236'1 <= 2*o236'1 /\ 0 < ar_1 /\ 0 <= i38' /\ 0 < o236'1 /\ 0 <= ar_2 /\ ar_2 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_New_2) = V_1
Pol(main_Load_521) = V_1 - V_3
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_Load_521(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i38' /\ 1 <= i38' /\ o236'1 = 1 /\ 1 <= ar_0 /\ o236'1 <= 2*o236'1 /\ 0 < ar_1 /\ 0 <= i38' /\ 0 < o236'1 /\ 0 <= ar_2 /\ ar_2 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 34) main_New_2(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, 1, 0)) [ 0 < o4'1 /\ 0 <= static'1 /\ o4'1 <= 2*o4'1 /\ 0 <= ar_1 /\ o4'1 = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_0, Cost: 51) main_Load_521(ar_0, ar_1, ar_2) -> Com_1(main_Load_521(ar_0, ar_1, ar_2 + 1)) [ ar_2 + 1 = i38' /\ 1 <= i38' /\ o236'1 = 1 /\ 1 <= ar_0 /\ o236'1 <= 2*o236'1 /\ 0 < ar_1 /\ 0 <= i38' /\ 0 < o236'1 /\ 0 <= ar_2 /\ ar_2 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 51*ar_0 + 34

Time: 0.113 sec (SMT: 0.106 sec)

(16) BOUNDS(CONSTANT, 34 + 51 * |#0|)

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

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

(18) Obligation:

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

Used field analysis yielded the following read fields:
- UnionFindIterative: [parent]

Considered paths: nonterm paths and paths from start to sinks

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

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

(20) Obligation:

IntTrs with 99 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{0,0}> main_New_4(i2, env, static) :|: 0 >= 0
main_New_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(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_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_New_45(i2, env, static) :|: 0 >= 0
main_New_45(i2, env, static) -{0,0}> main_New_47(i2, env, static) :|: 0 >= 0
main_New_47(i2, env, static) -{0,0}> main_New_50(i2, env, static) :|: 0 <= static
main_New_50(i2, env, static) -{0,0}> main_New_51(i2, env, static) :|: 0 >= 0
main_New_51(i2, env, static) -{0,0}> main_New_52(i2, env, static) :|: 0 >= 0
main_New_52(i2, env, static) -{1,1}> main_Duplicate_53(i2, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_53(i2, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_55(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_55(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_57(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_57(i2, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_59(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_59(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_61(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_63(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_63(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_64(o4, NULL, i2, env, static) -{1,1}> langle_init_rangle_Return_70(i2, o4', NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 0 < o4 && o4' <= o4 + NULL && 0 < o4'
langle_init_rangle_Return_70(i2, o4, NULL, env, static) -{1,1}> main_Store_73(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_73(i2, o4, NULL, env, static) -{1,1}> main_Load_74(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_74(i2, o4, NULL, env, static) -{1,1}> main_InvokeMethod_75(i2, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_75(i2, o4, NULL, env, static) -{1,1}> makeSet_Load_76(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_76(o4, i2, NULL, env, static) -{1,1}> makeSet_Load_77(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_Load_77(o4, i2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o4, i2, NULL, env, static) :|: NULL = 0 && 0 < o4
makeSet_FieldAccess_78(o4, i2, NULL, env, static) -{1,1}> makeSet_Return_80(i2, o4', env, static) :|: NULL = 0 && 0 < o4 && o4' <= o4 + o4 && o4' = o4 && 0 < o4'
makeSet_Return_80(i2, o4, env, static) -{1,1}> main_ConstantStackPush_83(i2, o4, env, static) :|: 0 < o4
main_ConstantStackPush_83(i2, o4, env, static) -{1,1}> main_Store_84(i2, iconst_0, o4, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_84(i2, iconst_0, o4, env, static) -{1,1}> main_Load_85(i2, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_85(i2, o4, iconst_0, env, static) -{0,0}> main_Load_242(i2, o4, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o4 && iconst_0 <= 1 && iconst_0 = 0
main_Load_242(i13, o77, i14, env, static) -{0,0}> main_Load_368(i13, o77, i14, env, static) :|: 0 <= i14 && i14 <= 1 && i14 <= 2 && 0 < o77
main_Load_368(i22, o153, i23, env, static) -{0,0}> main_Load_521(i22, o153, i23, env, static) :|: i23 <= 2 && 0 < o153 && 0 <= i23
main_Load_521(i30, o230, i31, env, static) -{1,1}> main_Load_528(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_Load_528(i30, i31, o230, env, static) -{1,1}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_538(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30
main_GE_538(i30, i31, o230, env, static) -{1,1}> main_New_553(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30 && 1 <= i30
main_New_553(i30, o230, i31, env, static) -{1,1}> main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30 && o236 = 1
main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Return_574(i30, o236', o230, i31, NULL, env, static) :|: NULL = 0 && o236' <= o236 + NULL && 0 < o230 && 0 <= i31 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236 + NULL
langle_init_rangle_Return_574(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Store_576(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Store_576(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Load_578(i30, o230, i31, o236, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_578(i30, o230, i31, o236, NULL, env, static) -{1,1}> main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Return_600(i30, o230, i31, o236', env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && o236' <= o236 + o236 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236
makeSet_Return_600(i30, o230, i31, o236, env, static) -{1,1}> main_Load_602(i30, o230, i31, o236, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_602(i30, o230, i31, o236, env, static) -{1,1}> main_Load_604(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_604(i30, o236, o230, i31, env, static) -{1,1}> main_InvokeMethod_614(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_614(i30, o236, o230, i31, env, static) -{1,1}> union_Load_615(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_615(o236, o230, i30, i31, env, static) -{1,1}> union_InvokeMethod_617(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_617(o236, o230, i30, i31, env, static) -{1,1}> find_Load_618(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_618(o236, o230, i30, i31, env, static) -{1,1}> find_Store_619(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_619(o236, o230, i30, i31, env, static) -{1,1}> find_Load_620(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_620(o236, o230, i30, i31, env, static) -{1,1}> find_FieldAccess_621(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_621(o236, o230, i30, i31, env, static) -{1,1}> find_Load_622(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_622(o236, o230, i30, i31, env, static) -{1,1}> find_EQ_623(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_623(o236, o230, i30, i31, env, static) -{1,1}> find_Load_624(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_624(o236, o230, i30, i31, env, static) -{1,1}> find_Return_625(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_625(o236, o230, i30, i31, env, static) -{1,1}> union_Store_626(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_626(o236, o230, i30, i31, env, static) -{1,1}> union_Load_627(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_627(o230, o236, i30, i31, env, static) -{1,1}> union_InvokeMethod_628(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_628(o230, o236, i30, i31, env, static) -{1,1}> find_Load_629(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_629(o230, o236, i30, i31, env, static) -{1,1}> find_Store_674(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_674(o230, o236, i30, i31, env, static) -{1,1}> find_Load_688(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_688(o230, o236, i30, i31, env, static) -{1,1}> find_FieldAccess_689(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_689(o230, o236, i30, i31, env, static) -{1,1}> find_Load_690(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_690(o230, o236, i30, i31, env, static) -{1,1}> find_EQ_691(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_691(o230, o236, i30, i31, env, static) -{1,1}> find_Load_692(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_692(o230, o236, i30, i31, env, static) -{1,1}> find_Return_705(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_705(o230, o236, i30, i31, env, static) -{1,1}> union_Store_707(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_707(o230, o236, i30, i31, env, static) -{1,1}> union_Load_708(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_708(o236, o230, i30, i31, env, static) -{1,1}> union_Load_710(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_710(o236, o230, i30, i31, env, static) -{1,1}> union_FieldAccess_712(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_FieldAccess_712(o236, o230, i30, i31, env, static) -{1,1}> union_Return_713(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Return_713(i30, o230, i31, env, static) -{1,1}> main_Inc_715(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30
main_Inc_715(i30, o230, i31, env, static) -{1,1}> main_JMP_719(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30 && 1 <= i38 && i31 + 1 = i38
main_JMP_719(i30, o230, i38, env, static) -{1,1}> main_Load_730(i30, o230, i38, env, static) :|: 0 < o230 && 1 <= i30 && 1 <= i38
main_Load_730(i30, o230, i38, env, static) -{0,0}> main_Load_521(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i38 && 1 <= i30 && 1 <= i38

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

obtained
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
by chaining
main_Load_521(i30, o230, i31, env, static) -{1,1}> main_Load_528(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_Load_528(i30, i31, o230, env, static) -{1,1}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31

obtained
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i38', env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
by chaining
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_538(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30
main_GE_538(i30, i31, o230, env, static) -{1,1}> main_New_553(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && i31 < i30 && 1 <= i30
main_New_553(i30, o230, i31, env, static) -{1,1}> main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30 && o236 = 1
main_Duplicate_555(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_ConstantStackPush_556(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_557(i30, o236, NULL, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_558(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_InvokeMethod_559(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_560(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_Load_561(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
langle_init_rangle_FieldAccess_572(o236, NULL, i30, o230, i31, env, static) -{1,1}> langle_init_rangle_Return_574(i30, o236', o230, i31, NULL, env, static) :|: NULL = 0 && o236' <= o236 + NULL && 0 < o230 && 0 <= i31 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236 + NULL
langle_init_rangle_Return_574(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Store_576(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Store_576(i30, o236, o230, i31, NULL, env, static) -{1,1}> main_Load_578(i30, o230, i31, o236, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_578(i30, o230, i31, o236, NULL, env, static) -{1,1}> main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_580(i30, o236, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_582(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_Load_588(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
makeSet_FieldAccess_593(o236, i30, o230, i31, NULL, env, static) -{1,1}> makeSet_Return_600(i30, o230, i31, o236', env, static) :|: NULL = 0 && 0 < o230 && 0 <= i31 && o236' <= o236 + o236 && 0 < o236 && 0 < o236' && 1 <= i30 && o236' = o236
makeSet_Return_600(i30, o230, i31, o236, env, static) -{1,1}> main_Load_602(i30, o230, i31, o236, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_602(i30, o230, i31, o236, env, static) -{1,1}> main_Load_604(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_Load_604(i30, o236, o230, i31, env, static) -{1,1}> main_InvokeMethod_614(i30, o236, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
main_InvokeMethod_614(i30, o236, o230, i31, env, static) -{1,1}> union_Load_615(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_615(o236, o230, i30, i31, env, static) -{1,1}> union_InvokeMethod_617(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_617(o236, o230, i30, i31, env, static) -{1,1}> find_Load_618(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_618(o236, o230, i30, i31, env, static) -{1,1}> find_Store_619(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_619(o236, o230, i30, i31, env, static) -{1,1}> find_Load_620(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_620(o236, o230, i30, i31, env, static) -{1,1}> find_FieldAccess_621(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_621(o236, o230, i30, i31, env, static) -{1,1}> find_Load_622(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_622(o236, o230, i30, i31, env, static) -{1,1}> find_EQ_623(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_623(o236, o230, i30, i31, env, static) -{1,1}> find_Load_624(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_624(o236, o230, i30, i31, env, static) -{1,1}> find_Return_625(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_625(o236, o230, i30, i31, env, static) -{1,1}> union_Store_626(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_626(o236, o230, i30, i31, env, static) -{1,1}> union_Load_627(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_627(o230, o236, i30, i31, env, static) -{1,1}> union_InvokeMethod_628(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_InvokeMethod_628(o230, o236, i30, i31, env, static) -{1,1}> find_Load_629(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_629(o230, o236, i30, i31, env, static) -{1,1}> find_Store_674(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Store_674(o230, o236, i30, i31, env, static) -{1,1}> find_Load_688(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_688(o230, o236, i30, i31, env, static) -{1,1}> find_FieldAccess_689(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_FieldAccess_689(o230, o236, i30, i31, env, static) -{1,1}> find_Load_690(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_690(o230, o236, i30, i31, env, static) -{1,1}> find_EQ_691(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_EQ_691(o230, o236, i30, i31, env, static) -{1,1}> find_Load_692(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Load_692(o230, o236, i30, i31, env, static) -{1,1}> find_Return_705(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
find_Return_705(o230, o236, i30, i31, env, static) -{1,1}> union_Store_707(o230, o236, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Store_707(o230, o236, i30, i31, env, static) -{1,1}> union_Load_708(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_708(o236, o230, i30, i31, env, static) -{1,1}> union_Load_710(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Load_710(o236, o230, i30, i31, env, static) -{1,1}> union_FieldAccess_712(o236, o230, i30, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_FieldAccess_712(o236, o230, i30, i31, env, static) -{1,1}> union_Return_713(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 0 < o236 && 1 <= i30
union_Return_713(i30, o230, i31, env, static) -{1,1}> main_Inc_715(i30, o230, i31, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30
main_Inc_715(i30, o230, i31, env, static) -{1,1}> main_JMP_719(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i31 && 1 <= i30 && 1 <= i38 && i31 + 1 = i38
main_JMP_719(i30, o230, i38, env, static) -{1,1}> main_Load_730(i30, o230, i38, env, static) :|: 0 < o230 && 1 <= i30 && 1 <= i38
main_Load_730(i30, o230, i38, env, static) -{0,0}> main_Load_521(i30, o230, i38, env, static) :|: 0 < o230 && 0 <= i38 && 1 <= i30 && 1 <= i38

(22) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, o4'1, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i38', env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30

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

Moved arithmethic from constraints to rhss.

main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, o4'1, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1 + 0, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1

main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i38', env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
was transformed to
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30

(24) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1 + 0, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31

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

Simplified expressions.

main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1 + 0, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1, 0, env, static'1) :|: 0 < o4'1 && 0 <= static'1 && o4'1 <= 2 * o4'1 && 0 <= static && o4'1 = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
was transformed to
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 && 1 <= i30 && o236'1 <= 2 * o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 <= i31 && i31 < i30

(26) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1, 0, env, static'1) :|: 0 < o4'1 && 0 <= static'1 && o4'1 <= 2 * o4'1 && 0 <= static && o4'1 = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 && 1 <= i30 && o236'1 <= 2 * o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 <= i31 && i31 < i30
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31

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

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

(28) Obligation:

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

(30) Obligation:

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

Moved arithmethic from constraints to rhss.

(32) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1 + 0, 0, env, static'1) :|: 0 >= 0 && 0 <= 0 && 0 < 2 && 0 <= 2 && 0 < o4'1 && 0 <= static'1 && o4'1 <= o4'1 + o4'1 && 0 <= static && o4'1 = 1 + 0 && static''' <= static + 2 && 0 < 1 && 0 <= static''' && 0 <= 1 && o4'1 <= 1 + 0 && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 + 0 && 1 <= i30 && o236'1 <= o236'1 + o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 < 1 && 0 <= i31 && o236'1 <= 1 + 0 && i31 < i30
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31

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

Simplified expressions.

(34) Obligation:

IntTrs with 4 rules
Start term: main_New_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, env, static) -{34,34}> main_Load_521(i2, 1, 0, env, static'1) :|: 0 < o4'1 && 0 <= static'1 && o4'1 <= 2 * o4'1 && 0 <= static && o4'1 = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_Load_521(i30, o230, i31, env, static) -{2,2}> main_GE_536(i30, i31, o230, env, static) :|: 0 < o230 && 0 <= i31
main_GE_536(i30, i31, o230, env, static) -{49,49}> main_Load_521(i30, o230, i31 + 1, env, static) :|: i31 + 1 = i38' && 1 <= i38' && o236'1 = 1 && 1 <= i30 && o236'1 <= 2 * o236'1 && 0 < o230 && 0 <= i38' && 0 < o236'1 && 0 <= i31 && i31 < i30
main_GE_536(i30, i31, o230, env, static) -{0,0}> main_GE_537(i30, i31, o230, env, static) :|: i30 <= i31 && 0 < o230 && 0 <= i31