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

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 79 + 54 * |args|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 174 ms)

    ↳18 WeightedIntTrs

        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 56 ms)

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(45)), 0 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 201 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 67 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

    ↳41 koat Proof (⇔, 14 ms)

    ↳42 BOUNDS(CONSTANT, 34 + 54 * |args|)

(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(String[] args) {
        UnionFindIterative y = new UnionFindIterative(null);
        y.makeSet();
        for (int i = 0; i < args[0].length(); ++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([Ljava/lang/String;)V: Graph of 153 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 107 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

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

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

(6) Obligation:

IntTrs with 107 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(o2, env, static) -{0,0}> main_New_5(o2, env, static) :|: 0 < o2
main_New_5(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_21(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_21(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_30(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_30(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_New_50(o2, env, static) :|: 0 < o2
main_New_50(o2, env, static) -{0,0}> main_New_51(o2, env, static) :|: 0 < o2
main_New_51(o2, env, static) -{0,0}> main_New_54(o2, env, static) :|: 0 < o2 && 0 <= static
main_New_54(o2, env, static) -{0,0}> main_New_55(o2, env, static) :|: 0 < o2
main_New_55(o2, env, static) -{0,0}> main_New_56(o2, env, static) :|: 0 < o2
main_New_56(o2, env, static) -{1,1}> main_Duplicate_57(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6 && o6 = 1
main_Duplicate_57(o2, o6, NULL, env, static) -{1,1}> main_ConstantStackPush_58(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_ConstantStackPush_58(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_59(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_59(o2, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_60(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
langle_init_rangle_Load_60(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_65(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_65(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_67(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_67(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Return_71(o2, o6', NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && o6' <= o6 + NULL && o6' = o6 + NULL && 0 < o6'
langle_init_rangle_Return_71(o2, o6, NULL, env, static) -{1,1}> main_Store_73(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Store_73(o2, o6, NULL, env, static) -{1,1}> main_Load_74(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Load_74(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_75(o2, o6, NULL, env, static) -{1,1}> makeSet_Load_76(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
makeSet_Load_76(o6, o2, NULL, env, static) -{1,1}> makeSet_Load_77(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_Load_77(o6, o2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_FieldAccess_78(o6, o2, NULL, env, static) -{1,1}> makeSet_Return_80(o2, o6', env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && 0 < o6' && o6' <= o6 + o6 && o6' = o6
makeSet_Return_80(o2, o6, env, static) -{1,1}> main_ConstantStackPush_82(o2, o6, env, static) :|: 0 < o2 && 0 < o6
main_ConstantStackPush_82(o2, o6, env, static) -{1,1}> main_Store_85(o2, iconst_0, o6, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Store_85(o2, iconst_0, o6, env, static) -{1,1}> main_Load_87(o2, o6, iconst_0, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Load_87(o2, o6, iconst_0, env, static) -{0,0}> main_Load_369(o2, o6, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && 0 < o6 && iconst_0 <= 1 && iconst_0 = 0
main_Load_369(o111, o112, i16, env, static) -{0,0}> main_Load_745(o111, o112, i16, env, static) :|: i16 <= 1 && 0 < o112 && 0 <= i16 && 0 < o111 && i16 <= 2
main_Load_745(o233, o234, i36, env, static) -{0,0}> main_Load_967(o233, o234, i36, env, static) :|: i36 <= 2 && 0 < o234 && 0 < o233 && 0 <= i36
main_Load_967(o349, o350, i47, env, static) -{1,1}> main_Load_968(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_Load_968(o349, i47, o350, env, static) -{1,1}> main_ConstantStackPush_970(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_ConstantStackPush_970(o349, i47, o350, env, static) -{1,1}> main_ArrayAccess_973(o349, i47, iconst_0, o350, env, static) :|: 0 <= i47 && iconst_0 = 0 && 0 < o349 && 0 < o350
main_ArrayAccess_973(a186, i47, iconst_0, o350, env, static) -{0,0}> main_ArrayAccess_975(a186, i47, iconst_0, o350, i51, env, static) :|: 0 <= i51 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && i51 < a186 && 0 < o350
main_ArrayAccess_975(a186, i47, iconst_0, o350, iconst_0, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_975(a186, i47, iconst_0, o350, i52, env, static) -{0,0}> main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) :|: 0 <= i52 && 1 <= i52 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358, o350, i52, env, static) :|: 1 <= i52 && iconst_0 < i52 && 0 < a186 && o358 < a186 && 0 <= i47 && iconst_0 = 0 && 0 <= o358 && 0 < o350
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{0,0}> main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= o361 && 0 < o361 && 0 < o350
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, NULL, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53, o350, i52, env, static) :|: i53 <= o361 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o361 && 0 < o350 && 0 <= i53
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1007(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_GE_1007(a186, i47, i53, o350, i52, env, static) -{1,1}> main_New_1018(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_New_1018(a186, o350, i47, i52, env, static) -{1,1}> main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363 = 1 && 0 < o350
main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Return_1056(a186, o363', o350, i47, i52, NULL, env, static) :|: NULL = 0 && o363' <= o363 + NULL && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363' = o363 + NULL && 0 < o363' && 0 < o350
langle_init_rangle_Return_1056(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Return_1083(a186, o350, i47, o363', i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && o363' = o363 && o363' <= o363 + o363 && 0 <= i47 && 0 < o363' && 0 < o350
makeSet_Return_1083(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1086(a186, o350, i47, o363, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1086(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1089(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1089(a186, o363, o350, i47, i52, env, static) -{1,1}> main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) -{1,1}> union_Load_1098(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1098(o363, o350, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1104(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1104(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Store_1106(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1106(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1108(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1108(o363, o350, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1111(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1111(o363, o350, a186, i47, i52, env, static) -{1,1}> find_EQ_1113(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1113(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1115(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1115(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Return_1117(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1117(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Store_1119(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1119(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1120(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1120(o350, o363, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1123(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1123(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Store_1128(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1128(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1133(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1133(o350, o363, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1139(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1139(o350, o363, a186, i47, i52, env, static) -{1,1}> find_EQ_1142(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1142(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1143(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1143(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Return_1145(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1145(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Store_1146(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1146(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Load_1147(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1147(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1148(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1148(o363, o350, a186, i47, i52, env, static) -{1,1}> union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Return_1153(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Return_1153(a186, o350, i47, i52, env, static) -{1,1}> main_Inc_1154(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o350
main_Inc_1154(a186, o350, i47, i52, env, static) -{1,1}> main_JMP_1156(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i47 && i47 + 1 = i57 && 0 < o350
main_JMP_1156(a186, o350, i57, i52, env, static) -{1,1}> main_Load_1158(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 < o350
main_Load_1158(a186, o350, i57, i52, env, static) -{0,0}> main_Load_967(a186, o350, i57, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i57 && 0 < o350

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

obtained
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
by chaining
main_New_1(o2, env, static) -{0,0}> main_New_5(o2, env, static) :|: 0 < o2
main_New_5(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_21(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_21(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_30(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_30(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_New_50(o2, env, static) :|: 0 < o2
main_New_50(o2, env, static) -{0,0}> main_New_51(o2, env, static) :|: 0 < o2
main_New_51(o2, env, static) -{0,0}> main_New_54(o2, env, static) :|: 0 < o2 && 0 <= static
main_New_54(o2, env, static) -{0,0}> main_New_55(o2, env, static) :|: 0 < o2
main_New_55(o2, env, static) -{0,0}> main_New_56(o2, env, static) :|: 0 < o2
main_New_56(o2, env, static) -{1,1}> main_Duplicate_57(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6 && o6 = 1
main_Duplicate_57(o2, o6, NULL, env, static) -{1,1}> main_ConstantStackPush_58(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_ConstantStackPush_58(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_59(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_59(o2, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_60(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
langle_init_rangle_Load_60(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_65(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_65(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_67(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_67(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Return_71(o2, o6', NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && o6' <= o6 + NULL && o6' = o6 + NULL && 0 < o6'
langle_init_rangle_Return_71(o2, o6, NULL, env, static) -{1,1}> main_Store_73(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Store_73(o2, o6, NULL, env, static) -{1,1}> main_Load_74(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Load_74(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_75(o2, o6, NULL, env, static) -{1,1}> makeSet_Load_76(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
makeSet_Load_76(o6, o2, NULL, env, static) -{1,1}> makeSet_Load_77(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_Load_77(o6, o2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_FieldAccess_78(o6, o2, NULL, env, static) -{1,1}> makeSet_Return_80(o2, o6', env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && 0 < o6' && o6' <= o6 + o6 && o6' = o6
makeSet_Return_80(o2, o6, env, static) -{1,1}> main_ConstantStackPush_82(o2, o6, env, static) :|: 0 < o2 && 0 < o6
main_ConstantStackPush_82(o2, o6, env, static) -{1,1}> main_Store_85(o2, iconst_0, o6, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Store_85(o2, iconst_0, o6, env, static) -{1,1}> main_Load_87(o2, o6, iconst_0, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Load_87(o2, o6, iconst_0, env, static) -{0,0}> main_Load_369(o2, o6, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && 0 < o6 && iconst_0 <= 1 && iconst_0 = 0
main_Load_369(o111, o112, i16, env, static) -{0,0}> main_Load_745(o111, o112, i16, env, static) :|: i16 <= 1 && 0 < o112 && 0 <= i16 && 0 < o111 && i16 <= 2
main_Load_745(o233, o234, i36, env, static) -{0,0}> main_Load_967(o233, o234, i36, env, static) :|: i36 <= 2 && 0 < o234 && 0 < o233 && 0 <= i36

obtained
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
by chaining
main_Load_967(o349, o350, i47, env, static) -{1,1}> main_Load_968(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_Load_968(o349, i47, o350, env, static) -{1,1}> main_ConstantStackPush_970(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_ConstantStackPush_970(o349, i47, o350, env, static) -{1,1}> main_ArrayAccess_973(o349, i47, iconst_0, o350, env, static) :|: 0 <= i47 && iconst_0 = 0 && 0 < o349 && 0 < o350
main_ArrayAccess_973(a186, i47, iconst_0, o350, env, static) -{0,0}> main_ArrayAccess_975(a186, i47, iconst_0, o350, i51, env, static) :|: 0 <= i51 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && i51 < a186 && 0 < o350

obtained
main_ArrayAccess_975(a186, i47, 0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52
by chaining
main_ArrayAccess_975(a186, i47, iconst_0, o350, i52, env, static) -{0,0}> main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) :|: 0 <= i52 && 1 <= i52 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358, o350, i52, env, static) :|: 1 <= i52 && iconst_0 < i52 && 0 < a186 && o358 < a186 && 0 <= i47 && iconst_0 = 0 && 0 <= o358 && 0 < o350

obtained
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
by chaining
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{0,0}> main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= o361 && 0 < o361 && 0 < o350
main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53, o350, i52, env, static) :|: i53 <= o361 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o361 && 0 < o350 && 0 <= i53

obtained
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i57', env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
by chaining
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1007(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_GE_1007(a186, i47, i53, o350, i52, env, static) -{1,1}> main_New_1018(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_New_1018(a186, o350, i47, i52, env, static) -{1,1}> main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363 = 1 && 0 < o350
main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Return_1056(a186, o363', o350, i47, i52, NULL, env, static) :|: NULL = 0 && o363' <= o363 + NULL && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363' = o363 + NULL && 0 < o363' && 0 < o350
langle_init_rangle_Return_1056(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Return_1083(a186, o350, i47, o363', i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && o363' = o363 && o363' <= o363 + o363 && 0 <= i47 && 0 < o363' && 0 < o350
makeSet_Return_1083(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1086(a186, o350, i47, o363, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1086(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1089(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1089(a186, o363, o350, i47, i52, env, static) -{1,1}> main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) -{1,1}> union_Load_1098(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1098(o363, o350, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1104(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1104(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Store_1106(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1106(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1108(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1108(o363, o350, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1111(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1111(o363, o350, a186, i47, i52, env, static) -{1,1}> find_EQ_1113(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1113(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1115(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1115(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Return_1117(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1117(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Store_1119(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1119(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1120(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1120(o350, o363, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1123(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1123(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Store_1128(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1128(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1133(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1133(o350, o363, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1139(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1139(o350, o363, a186, i47, i52, env, static) -{1,1}> find_EQ_1142(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1142(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1143(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1143(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Return_1145(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1145(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Store_1146(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1146(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Load_1147(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1147(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1148(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1148(o363, o350, a186, i47, i52, env, static) -{1,1}> union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Return_1153(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Return_1153(a186, o350, i47, i52, env, static) -{1,1}> main_Inc_1154(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o350
main_Inc_1154(a186, o350, i47, i52, env, static) -{1,1}> main_JMP_1156(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i47 && i47 + 1 = i57 && 0 < o350
main_JMP_1156(a186, o350, i57, i52, env, static) -{1,1}> main_Load_1158(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 < o350
main_Load_1158(a186, o350, i57, i52, env, static) -{0,0}> main_Load_967(a186, o350, i57, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i57 && 0 < o350

(8) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_ArrayAccess_975(a186, i47, iconst_0, o350, iconst_0, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_975(a186, i47, 0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, NULL, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i57', env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0

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

Moved arithmethic from lhss to constraints.

main_ArrayAccess_975(a186, i47, 0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52
was transformed to
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0

(10) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i57', env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
main_ArrayAccess_975(a186, i47, iconst_0, o350, iconst_0, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, NULL, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350

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

Linearized lhss.

main_ArrayAccess_975(a186, i47, iconst_0, o350, iconst_0, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
was transformed to
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0

(12) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i57', env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, NULL, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53

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

Moved arithmethic from constraints to rhss.

main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i57', env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
was transformed to
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0

main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, iconst_0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
was transformed to
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, 0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0

main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1 + 0, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1

main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, NULL, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
was transformed to
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, 0, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350

(14) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, 0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1 + 0, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, 0, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350

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

Simplified expressions.

main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
was transformed to
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= 2 * o363'1 && 0 <= i53

main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
was transformed to
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0

main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
was transformed to
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361

main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1 + 0, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 < o2 && o6'1 <= 2 * o6'1 && 0 < o6'1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && o6'1 = 1 && static'1 <= static''' + 1

(16) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= 2 * o363'1 && 0 <= i53
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, 0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, 0, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 < o2 && o6'1 <= 2 * o6'1 && 0 < o6'1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && o6'1 = 1 && static'1 <= static''' + 1
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53

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

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

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Linearized lhss.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 + 0 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= o363'1 + o363'1 && 0 < 1 && 0 <= i53 && o363'1 <= 1 + 0
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 0 <= i52 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, 0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1 + 0, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, 0, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350

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

Simplified expressions.

(28) Obligation:

IntTrs with 8 rules
Start term: main_New_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_997(a186, i47, i53, o350, i52, env, static) -{49,49}> main_Load_967(a186, o350, i47 + 1, env, static) :|: i47 < i53 && 0 < o350 && o363'1 = 1 && 0 <= i57' && i47 + 1 = i57' && 0 < a186 && 0 < o363'1 && 1 <= i52 && 1 <= i57' && 0 <= i47 && o363'1 <= 2 * o363'1 && 0 <= i53
main_ArrayAccess_975(a186, i47, iconst_0, o350, x, env, static) -{0,0}> main_ArrayAccess_977(a186, i47, 0, o350, env, static) :|: 0 <= iconst_0 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350 && x = iconst_0
main_InvokeMethod_985(a186, i47, NULL, o350, i52, env, static) -{0,0}> main_InvokeMethod_988(a186, i47, 0, o350, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= NULL && 0 < o350
main_ArrayAccess_975(a186, i47, x, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358', o350, i52, env, static) :|: 0 < o350 && 0 <= o358' && 0 <= i47 && 0 < a186 && 1 <= i52 && o358' < a186 && 0 < i52 && x = 0
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53', o350, i52, env, static) :|: 0 < o350 && 0 <= i53' && 0 < o361 && 0 <= i47 && 1 <= i52 && 0 < a186 && i53' <= o361
main_Load_967(o349, o350, i47, env, static) -{3,3}> main_ArrayAccess_975(o349, i47, 0, o350, i51', env, static) :|: 0 <= i47 && 0 < o350 && 0 < o349 && i51' < o349 && 0 <= i51'
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, 1, 0, env, static'1) :|: 0 <= static'1 && 0 < o2 && o6'1 <= 2 * o6'1 && 0 < o6'1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && o6'1 = 1 && static'1 <= static''' + 1
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1006(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && i53 <= i47 && 0 < a186 && 0 <= i47 && 0 < o350 && 0 <= i53

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(45)) transformation)

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

(30) Obligation:

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

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

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 104 rules
Start term: main_New_1(args, env, static)
Considered paths: all paths from start
Rules:
main_New_1(o2, env, static) -{0,0}> main_New_5(o2, env, static) :|: 0 < o2
main_New_5(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_21(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_21(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_23(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_25(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_28(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_30(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_30(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_35(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_42(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_New_50(o2, env, static) :|: 0 < o2
main_New_50(o2, env, static) -{0,0}> main_New_51(o2, env, static) :|: 0 < o2
main_New_51(o2, env, static) -{0,0}> main_New_54(o2, env, static) :|: 0 < o2 && 0 <= static
main_New_54(o2, env, static) -{0,0}> main_New_55(o2, env, static) :|: 0 < o2
main_New_55(o2, env, static) -{0,0}> main_New_56(o2, env, static) :|: 0 < o2
main_New_56(o2, env, static) -{1,1}> main_Duplicate_57(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6 && o6 = 1
main_Duplicate_57(o2, o6, NULL, env, static) -{1,1}> main_ConstantStackPush_58(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_ConstantStackPush_58(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_59(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_59(o2, o6, NULL, env, static) -{1,1}> langle_init_rangle_Load_60(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
langle_init_rangle_Load_60(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_InvokeMethod_62(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_65(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_65(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_67(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_Load_67(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
langle_init_rangle_FieldAccess_69(o6, NULL, o2, env, static) -{1,1}> langle_init_rangle_Return_71(o2, o6', NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && o6' <= o6 + NULL && o6' = o6 + NULL && 0 < o6'
langle_init_rangle_Return_71(o2, o6, NULL, env, static) -{1,1}> main_Store_73(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Store_73(o2, o6, NULL, env, static) -{1,1}> main_Load_74(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_Load_74(o2, o6, NULL, env, static) -{1,1}> main_InvokeMethod_75(o2, o6, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
main_InvokeMethod_75(o2, o6, NULL, env, static) -{1,1}> makeSet_Load_76(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o2 && 0 < o6
makeSet_Load_76(o6, o2, NULL, env, static) -{1,1}> makeSet_Load_77(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_Load_77(o6, o2, NULL, env, static) -{1,1}> makeSet_FieldAccess_78(o6, o2, NULL, env, static) :|: NULL = 0 && 0 < o6 && 0 < o2
makeSet_FieldAccess_78(o6, o2, NULL, env, static) -{1,1}> makeSet_Return_80(o2, o6', env, static) :|: NULL = 0 && 0 < o6 && 0 < o2 && 0 < o6' && o6' <= o6 + o6 && o6' = o6
makeSet_Return_80(o2, o6, env, static) -{1,1}> main_ConstantStackPush_82(o2, o6, env, static) :|: 0 < o2 && 0 < o6
main_ConstantStackPush_82(o2, o6, env, static) -{1,1}> main_Store_85(o2, iconst_0, o6, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Store_85(o2, iconst_0, o6, env, static) -{1,1}> main_Load_87(o2, o6, iconst_0, env, static) :|: 0 < o2 && 0 < o6 && iconst_0 = 0
main_Load_87(o2, o6, iconst_0, env, static) -{0,0}> main_Load_369(o2, o6, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && 0 < o6 && iconst_0 <= 1 && iconst_0 = 0
main_Load_369(o111, o112, i16, env, static) -{0,0}> main_Load_745(o111, o112, i16, env, static) :|: i16 <= 1 && 0 < o112 && 0 <= i16 && 0 < o111 && i16 <= 2
main_Load_745(o233, o234, i36, env, static) -{0,0}> main_Load_967(o233, o234, i36, env, static) :|: i36 <= 2 && 0 < o234 && 0 < o233 && 0 <= i36
main_Load_967(o349, o350, i47, env, static) -{1,1}> main_Load_968(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_Load_968(o349, i47, o350, env, static) -{1,1}> main_ConstantStackPush_970(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_ConstantStackPush_970(o349, i47, o350, env, static) -{1,1}> main_ArrayAccess_973(o349, i47, iconst_0, o350, env, static) :|: 0 <= i47 && iconst_0 = 0 && 0 < o349 && 0 < o350
main_ArrayAccess_973(a186, i47, iconst_0, o350, env, static) -{0,0}> main_ArrayAccess_975(a186, i47, iconst_0, o350, i51, env, static) :|: 0 <= i51 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && i51 < a186 && 0 < o350
main_ArrayAccess_975(a186, i47, iconst_0, o350, i52, env, static) -{0,0}> main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) :|: 0 <= i52 && 1 <= i52 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358, o350, i52, env, static) :|: 1 <= i52 && iconst_0 < i52 && 0 < a186 && o358 < a186 && 0 <= i47 && iconst_0 = 0 && 0 <= o358 && 0 < o350
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{0,0}> main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= o361 && 0 < o361 && 0 < o350
main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53, o350, i52, env, static) :|: i53 <= o361 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o361 && 0 < o350 && 0 <= i53
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1007(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_GE_1007(a186, i47, i53, o350, i52, env, static) -{1,1}> main_New_1018(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_New_1018(a186, o350, i47, i52, env, static) -{1,1}> main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363 = 1 && 0 < o350
main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Return_1056(a186, o363', o350, i47, i52, NULL, env, static) :|: NULL = 0 && o363' <= o363 + NULL && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363' = o363 + NULL && 0 < o363' && 0 < o350
langle_init_rangle_Return_1056(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Return_1083(a186, o350, i47, o363', i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && o363' = o363 && o363' <= o363 + o363 && 0 <= i47 && 0 < o363' && 0 < o350
makeSet_Return_1083(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1086(a186, o350, i47, o363, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1086(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1089(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1089(a186, o363, o350, i47, i52, env, static) -{1,1}> main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) -{1,1}> union_Load_1098(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1098(o363, o350, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1104(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1104(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Store_1106(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1106(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1108(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1108(o363, o350, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1111(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1111(o363, o350, a186, i47, i52, env, static) -{1,1}> find_EQ_1113(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1113(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1115(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1115(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Return_1117(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1117(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Store_1119(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1119(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1120(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1120(o350, o363, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1123(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1123(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Store_1128(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1128(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1133(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1133(o350, o363, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1139(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1139(o350, o363, a186, i47, i52, env, static) -{1,1}> find_EQ_1142(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1142(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1143(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1143(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Return_1145(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1145(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Store_1146(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1146(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Load_1147(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1147(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1148(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1148(o363, o350, a186, i47, i52, env, static) -{1,1}> union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Return_1153(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Return_1153(a186, o350, i47, i52, env, static) -{1,1}> main_Inc_1154(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o350
main_Inc_1154(a186, o350, i47, i52, env, static) -{1,1}> main_JMP_1156(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i47 && i47 + 1 = i57 && 0 < o350
main_JMP_1156(a186, o350, i57, i52, env, static) -{1,1}> main_Load_1158(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 < o350
main_Load_1158(a186, o350, i57, i52, env, static) -{0,0}> main_Load_967(a186, o350, i57, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i57 && 0 < o350

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

obtained
main_Load_967(o349, o350, i47, env, static) -{54,54}> main_Load_967(o349, o350, i57', env, static) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'
by chaining
main_Load_967(o349, o350, i47, env, static) -{1,1}> main_Load_968(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_Load_968(o349, i47, o350, env, static) -{1,1}> main_ConstantStackPush_970(o349, i47, o350, env, static) :|: 0 <= i47 && 0 < o349 && 0 < o350
main_ConstantStackPush_970(o349, i47, o350, env, static) -{1,1}> main_ArrayAccess_973(o349, i47, iconst_0, o350, env, static) :|: 0 <= i47 && iconst_0 = 0 && 0 < o349 && 0 < o350
main_ArrayAccess_973(a186, i47, iconst_0, o350, env, static) -{0,0}> main_ArrayAccess_975(a186, i47, iconst_0, o350, i51, env, static) :|: 0 <= i51 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && i51 < a186 && 0 < o350
main_ArrayAccess_975(a186, i47, iconst_0, o350, i52, env, static) -{0,0}> main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) :|: 0 <= i52 && 1 <= i52 && 0 < a186 && 0 <= i47 && iconst_0 = 0 && 0 < o350
main_ArrayAccess_978(a186, i47, iconst_0, o350, i52, env, static) -{1,1}> main_InvokeMethod_985(a186, i47, o358, o350, i52, env, static) :|: 1 <= i52 && iconst_0 < i52 && 0 < a186 && o358 < a186 && 0 <= i47 && iconst_0 = 0 && 0 <= o358 && 0 < o350
main_InvokeMethod_985(a186, i47, o361, o350, i52, env, static) -{0,0}> main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 <= o361 && 0 < o361 && 0 < o350
main_InvokeMethod_987(a186, i47, o361, o350, i52, env, static) -{1,1}> main_GE_997(a186, i47, i53, o350, i52, env, static) :|: i53 <= o361 && 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o361 && 0 < o350 && 0 <= i53
main_GE_997(a186, i47, i53, o350, i52, env, static) -{0,0}> main_GE_1007(a186, i47, i53, o350, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_GE_1007(a186, i47, i53, o350, i52, env, static) -{1,1}> main_New_1018(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && i47 < i53 && 0 < o350 && 0 <= i53
main_New_1018(a186, o350, i47, i52, env, static) -{1,1}> main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363 = 1 && 0 < o350
main_Duplicate_1023(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_ConstantStackPush_1029(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1033(a186, o363, NULL, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1035(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_InvokeMethod_1044(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1046(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_Load_1051(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
langle_init_rangle_FieldAccess_1054(o363, NULL, a186, o350, i47, i52, env, static) -{1,1}> langle_init_rangle_Return_1056(a186, o363', o350, i47, i52, NULL, env, static) :|: NULL = 0 && o363' <= o363 + NULL && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && o363' = o363 + NULL && 0 < o363' && 0 < o350
langle_init_rangle_Return_1056(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Store_1059(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1063(a186, o350, i47, o363, i52, NULL, env, static) -{1,1}> main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1066(a186, o363, o350, i47, i52, NULL, env, static) -{1,1}> makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1069(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_Load_1074(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
makeSet_FieldAccess_1078(o363, a186, o350, i47, NULL, i52, env, static) -{1,1}> makeSet_Return_1083(a186, o350, i47, o363', i52, env, static) :|: NULL = 0 && 1 <= i52 && 0 < o363 && 0 < a186 && o363' = o363 && o363' <= o363 + o363 && 0 <= i47 && 0 < o363' && 0 < o350
makeSet_Return_1083(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1086(a186, o350, i47, o363, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1086(a186, o350, i47, o363, i52, env, static) -{1,1}> main_Load_1089(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_Load_1089(a186, o363, o350, i47, i52, env, static) -{1,1}> main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
main_InvokeMethod_1093(a186, o363, o350, i47, i52, env, static) -{1,1}> union_Load_1098(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1098(o363, o350, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1103(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1104(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1104(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Store_1106(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1106(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1108(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1108(o363, o350, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1109(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1111(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1111(o363, o350, a186, i47, i52, env, static) -{1,1}> find_EQ_1113(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1113(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Load_1115(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1115(o363, o350, a186, i47, i52, env, static) -{1,1}> find_Return_1117(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1117(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Store_1119(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1119(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1120(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1120(o350, o363, a186, i47, i52, env, static) -{1,1}> union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_InvokeMethod_1122(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1123(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1123(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Store_1128(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Store_1128(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1133(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1133(o350, o363, a186, i47, i52, env, static) -{1,1}> find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_FieldAccess_1135(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1139(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1139(o350, o363, a186, i47, i52, env, static) -{1,1}> find_EQ_1142(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_EQ_1142(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Load_1143(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Load_1143(o350, o363, a186, i47, i52, env, static) -{1,1}> find_Return_1145(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
find_Return_1145(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Store_1146(o350, o363, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Store_1146(o350, o363, a186, i47, i52, env, static) -{1,1}> union_Load_1147(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1147(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Load_1148(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Load_1148(o363, o350, a186, i47, i52, env, static) -{1,1}> union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_FieldAccess_1149(o363, o350, a186, i47, i52, env, static) -{1,1}> union_Return_1153(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < o363 && 0 < a186 && 0 <= i47 && 0 < o350
union_Return_1153(a186, o350, i47, i52, env, static) -{1,1}> main_Inc_1154(a186, o350, i47, i52, env, static) :|: 1 <= i52 && 0 < a186 && 0 <= i47 && 0 < o350
main_Inc_1154(a186, o350, i47, i52, env, static) -{1,1}> main_JMP_1156(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i47 && i47 + 1 = i57 && 0 < o350
main_JMP_1156(a186, o350, i57, i52, env, static) -{1,1}> main_Load_1158(a186, o350, i57, i52, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 < o350
main_Load_1158(a186, o350, i57, i52, env, static) -{0,0}> main_Load_967(a186, o350, i57, env, static) :|: 1 <= i52 && 1 <= i57 && 0 < a186 && 0 <= i57 && 0 < o350

(34) Obligation:

IntTrs with 2 rules
Start term: main_New_1(args, env, static)
Considered paths: all paths from start
Rules:
main_New_1(o2, env, static) -{34,34}> main_Load_967(o2, o6'1, 0, env, static'1) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47, env, static) -{54,54}> main_Load_967(o349, o350, i57', env, static) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'

(35) 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_1(x1, x2, x3) → main_New_1(x1, x3)
main_Load_967(x1, x2, x3, x4, x5) → main_Load_967(x1, x2, x3)

(36) Obligation:

IntTrs with 2 rules
Start term: main_New_1(args, static)
Considered paths: all paths from start
Rules:
main_New_1(o2, static) -{34,34}> main_Load_967(o2, o6'1, 0) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i57') :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'

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

Moved arithmethic from constraints to rhss.

main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i57') :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'
was transformed to
main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i47 + 1) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'

main_New_1(o2, static) -{34,34}> main_Load_967(o2, o6'1, 0) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_1(o2, static) -{34,34}> main_Load_967(o2, 1 + 0, 0) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1

(38) Obligation:

IntTrs with 2 rules
Start term: main_New_1(args, static)
Considered paths: all paths from start
Rules:
main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i47 + 1) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'
main_New_1(o2, static) -{34,34}> main_Load_967(o2, 1 + 0, 0) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1

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

Simplified expressions.

main_New_1(o2, static) -{34,34}> main_Load_967(o2, 1 + 0, 0) :|: 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o2 && o6'1 <= o6'1 + o6'1 && 0 <= 2 && 0 < o6'1 && 0 < 1 && 0 <= static && 0 <= static''' && o6'1 <= 1 + 0 && 0 <= 1 && static''' <= static + 2 && o6'1 = 1 + 0 && static'1 <= static''' + 1
was transformed to
main_New_1(o2, static) -{34,34}> main_Load_967(o2, 1, 0) :|: 0 <= static'1 && 0 < o2 && o6'1 <= 2 * o6'1 && 0 < o6'1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && o6'1 = 1 && static'1 <= static''' + 1

main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i47 + 1) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 + 0 && 0 < o363'1 && 0 <= i51' && 0 <= o358' && 0 < 1 && i47 < i53' && o363'1 <= o363'1 + o363'1 && o363'1 <= 1 + 0 && i51' < o349 && 0 < o358' && 0 <= i53'
was transformed to
main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i47 + 1) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 && 0 < o363'1 && i47 < i53' && o363'1 <= 2 * o363'1 && i51' < o349 && 0 < o358' && 0 <= i53'

(40) Obligation:

IntTrs with 2 rules
Start term: main_New_1(args, static)
Considered paths: all paths from start
Rules:
main_New_1(o2, static) -{34,34}> main_Load_967(o2, 1, 0) :|: 0 <= static'1 && 0 < o2 && o6'1 <= 2 * o6'1 && 0 < o6'1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && o6'1 = 1 && static'1 <= static''' + 1
main_Load_967(o349, o350, i47) -{54,54}> main_Load_967(o349, o350, i47 + 1) :|: 0 < i51' && 0 < o350 && o358' < o349 && 0 <= i57' && i47 + 1 = i57' && 0 < o349 && i53' <= o358' && 1 <= i51' && 1 <= i57' && 0 <= i47 && o363'1 = 1 && 0 < o363'1 && i47 < i53' && o363'1 <= 2 * o363'1 && i51' < o349 && 0 < o358' && 0 <= i53'

(41) koat Proof (EQUIVALENT transformation)

YES(?, 54*ar_0 + 34)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 34) main_New_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, 1, 0)) [ 0 <= static'1 /\ 0 < ar_0 /\ o6'1 <= 2*o6'1 /\ 0 < o6'1 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ o6'1 = 1 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 54) main_Load_967(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, ar_1, ar_2 + 1)) [ 0 < i51' /\ 0 < ar_1 /\ o358' < ar_0 /\ 0 <= i57' /\ ar_2 + 1 = i57' /\ 0 < ar_0 /\ i53' <= o358' /\ 1 <= i51' /\ 1 <= i57' /\ 0 <= ar_2 /\ o363'1 = 1 /\ 0 < o363'1 /\ ar_2 < i53' /\ o363'1 <= 2*o363'1 /\ i51' < ar_0 /\ 0 < o358' /\ 0 <= i53' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_1(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_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, 1, 0)) [ 0 <= static'1 /\ 0 < ar_0 /\ o6'1 <= 2*o6'1 /\ 0 < o6'1 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ o6'1 = 1 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 54) main_Load_967(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, ar_1, ar_2 + 1)) [ 0 < i51' /\ 0 < ar_1 /\ o358' < ar_0 /\ 0 <= i57' /\ ar_2 + 1 = i57' /\ 0 < ar_0 /\ i53' <= o358' /\ 1 <= i51' /\ 1 <= i57' /\ 0 <= ar_2 /\ o363'1 = 1 /\ 0 < o363'1 /\ ar_2 < i53' /\ o363'1 <= 2*o363'1 /\ i51' < ar_0 /\ 0 < o358' /\ 0 <= i53' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_New_1) = V_1
Pol(main_Load_967) = V_1 - V_3
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_Load_967(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, ar_1, ar_2 + 1)) [ 0 < i51' /\ 0 < ar_1 /\ o358' < ar_0 /\ 0 <= i57' /\ ar_2 + 1 = i57' /\ 0 < ar_0 /\ i53' <= o358' /\ 1 <= i51' /\ 1 <= i57' /\ 0 <= ar_2 /\ o363'1 = 1 /\ 0 < o363'1 /\ ar_2 < i53' /\ o363'1 <= 2*o363'1 /\ i51' < ar_0 /\ 0 < o358' /\ 0 <= i53' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 34) main_New_1(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, 1, 0)) [ 0 <= static'1 /\ 0 < ar_0 /\ o6'1 <= 2*o6'1 /\ 0 < o6'1 /\ 0 <= ar_1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ o6'1 = 1 /\ static'1 <= static''' + 1 ]
(Comp: ar_0, Cost: 54) main_Load_967(ar_0, ar_1, ar_2) -> Com_1(main_Load_967(ar_0, ar_1, ar_2 + 1)) [ 0 < i51' /\ 0 < ar_1 /\ o358' < ar_0 /\ 0 <= i57' /\ ar_2 + 1 = i57' /\ 0 < ar_0 /\ i53' <= o358' /\ 1 <= i51' /\ 1 <= i57' /\ 0 <= ar_2 /\ o363'1 = 1 /\ 0 < o363'1 /\ ar_2 < i53' /\ o363'1 <= 2*o363'1 /\ i51' < ar_0 /\ 0 < o358' /\ 0 <= i53' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_New_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 54*ar_0 + 34

Time: 0.064 sec (SMT: 0.056 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(45)) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

(41) koat Proof (EQUIVALENT transformation)

(42) BOUNDS(CONSTANT, 34 + 54 * |args|)