time complexity proof of /tmp/tmpjwrSAd/RunningPointers.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳18 WeightedIntTrs

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

↳30 JBCComplexityEdges

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

    ↳43 koat Proof (⇔, 213 ms)

    ↳44 BOUNDS(CONSTANT, 40 + 123 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class ObjectList {
  Object value;
  ObjectList next;

  public ObjectList(Object value, ObjectList next) {
    this.value = value;
    this.next = next;
  }

  public static ObjectList createList(int length) {
    ObjectList result = null;
    while (length > 0) {
      result = new ObjectList(new Object(), result);
      length--;
    }
    return result;
  }
}


/**
 * Allegedly based on an interview question at Microsoft.
 */
public class RunningPointers {

  public static boolean isCyclic(ObjectList l) {
    if (l == null) {
      return false;
    }
    ObjectList l1, l2;
    l1 = l;
    l2 = l.next;
    while (l2 != null && l1 != l2) {
      l2 = l2.next;
      if (l2 == null) {
        return false;
      }
      else if (l2 == l1) {
        return true;
      }
      else {
        l2 = l2.next;
      }
      l1 = l1.next;
    }
    return l2 != null;
  }

  public static void main(int x) {
    ObjectList list = ObjectList.createList(x);
    isCyclic(list);
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
RunningPointers.main(I)V: Graph of 183 nodes with 2 SCCs.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- ObjectList: [next]

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 120 jbc graph edges to a weighted ITS with 120 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 120 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_47(i1, env, static) :|: 0 >= 0
main_Load_47(i1, env, static) -{1,1}> main_InvokeMethod_51(i1, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, env, static) -{0,0}> main_InvokeMethod_52(i1, env, static) :|: 0 >= 0
main_InvokeMethod_52(i1, env, static) -{1,1}> createList_ConstantStackPush_54(i1, env, static) :|: 0 >= 0
createList_ConstantStackPush_54(i1, env, static) -{1,1}> createList_Store_56(NULL, i1, env, static) :|: NULL = 0
createList_Store_56(NULL, i1, env, static) -{1,1}> createList_Load_59(i1, NULL, env, static) :|: NULL = 0
createList_Load_59(i1, NULL, env, static) -{1,1}> createList_LE_62(i1, NULL, env, static) :|: NULL = 0
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
createList_LE_62(i10, NULL, env, static) -{0,0}> createList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createList_LE_64(i10, NULL, env, static) -{1,1}> createList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createList_New_68(i10, NULL, env, static) -{1,1}> createList_Duplicate_72(o4, i10, NULL, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4
createList_Duplicate_72(o4, i10, NULL, env, static) -{1,1}> createList_New_76(o4, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4
createList_New_76(o4, i10, NULL, env, static) -{1,1}> createList_Duplicate_81(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && o6 = 1
createList_Duplicate_81(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) -{1,1}> createList_Load_88(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_Load_88(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) -{0,0}> createList_InvokeMethod_493(o4, o6, NULL, i10, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && 0 <= NULL
createList_InvokeMethod_493(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Return_511(o98', i57, i58, o96, env, static) :|: NULL = 0 && o98' <= o98 + o96 && 0 < o98' && 1 <= i57 && o98' = o98 + o96 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Return_511(o98, i57, i58, o96, env, static) -{1,1}> createList_Store_512(o98, i57, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Store_512(o98, i57, i58, o96, env, static) -{1,1}> createList_Inc_513(i57, o98, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Inc_513(i57, o98, i58, o96, env, static) -{1,1}> createList_JMP_514(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 1 <= i57 && 0 <= o96 && 1 <= i58 && i57 + -1 = i62 && 0 < o98
createList_JMP_514(i62, o98, i58, o96, env, static) -{1,1}> createList_Load_516(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_516(i62, o98, i58, o96, env, static) -{1,1}> createList_LE_523(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_LE_523(iconst_0, o98, i58, o96, env, static) -{0,0}> createList_LE_525(iconst_0, o98, i58, o96, env, static) :|: 0 <= iconst_0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_LE_523(i67, o98, i58, o96, env, static) -{0,0}> createList_LE_526(i67, o98, i58, o96, env, static) :|: 1 <= i67 && 0 <= o96 && 0 <= i67 && 1 <= i58 && 0 < o98
createList_LE_525(iconst_0, o98, i58, o96, env, static) -{1,1}> createList_Load_528(o98, i58, o96, env, static) :|: iconst_0 <= 0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_LE_526(i67, o98, i58, o96, env, static) -{1,1}> createList_New_531(i67, o98, i58, o96, env, static) :|: 0 < i67 && 1 <= i67 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_528(o98, i58, o96, env, static) -{1,1}> createList_Return_542(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_New_531(i67, o98, i58, o96, env, static) -{1,1}> createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && o117 = 1 && 1 <= i58 && 0 < o98
createList_Return_542(o98, i58, o96, env, static) -{1,1}> main_Store_549(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
main_Store_549(i58, o98, o96, env, static) -{1,1}> main_Load_555(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o125 && o125 = 1 && 0 < o117 && 1 <= i58 && 0 < o98
main_Load_555(i58, o98, o96, env, static) -{1,1}> main_InvokeMethod_561(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
main_InvokeMethod_561(i58, o98, o96, env, static) -{1,1}> isCyclic_Load_566(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
isCyclic_Load_566(o98, i58, o96, env, static) -{1,1}> isCyclic_NONNULL_579(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) -{0,0}> createList_InvokeMethod_493(o117, o125, o98, i67, i58, NULL, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 <= o98 && 0 < o117 && 1 <= i58 && 0 < o98
isCyclic_NONNULL_579(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_581(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_581(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_583(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_583(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_585(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_585(o98, i58, o96, env, static) -{1,1}> isCyclic_FieldAccess_587(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_FieldAccess_587(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_589(o96, o98, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_589(o96, o98, i58, env, static) -{1,1}> isCyclic_Load_590(o98, o96, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_590(o98, o96, i58, env, static) -{0,0}> isCyclic_Load_681(o98, o96, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_681(o157, o160, i58, o158, env, static) -{0,0}> isCyclic_Load_768(o157, o160, i58, env, static) :|: 0 <= o158 && 0 < o157 && 1 <= i58 && 0 <= o157 && 0 <= o160
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(o194, o187, i58, env, static) -{0,0}> isCyclic_NULL_773(o194, o187, i58, env, static) :|: 0 < o194 && 0 <= o194 && 1 <= i58 && 0 <= o187
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
isCyclic_NULL_773(o194, o187, i58, env, static) -{1,1}> isCyclic_Load_776(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_776(o187, o194, i58, env, static) -{1,1}> isCyclic_Load_779(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_779(o187, o194, i58, env, static) -{1,1}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_781(NULL, o194, i58, env, static) -{0,0}> isCyclic_EQ_785(NULL, o194, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58 && 0 <= NULL
isCyclic_EQ_784(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_830(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_EQ_785(NULL, o194, i58, env, static) -{1,1}> isCyclic_Load_833(NULL, o194, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58
isCyclic_EQ_830(o195, o194, i58, env, static) -{1,1}> isCyclic_Load_845(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_Load_833(NULL, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_853(o194, NULL, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58
isCyclic_Load_845(o195, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_855(o194, o195, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_853(o211, NULL, i58, env, static) -{0,0}> isCyclic_FieldAccess_857(o211, NULL, i58, o213, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58 && 1 + o213 = o211 && 0 < o211
isCyclic_FieldAccess_855(o214, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) :|: 1 + o216 = o214 && 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_FieldAccess_857(o211, NULL, i58, o213, env, static) -{1,1}> isCyclic_Store_865(o213, NULL, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58 && 0 < o211
isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) -{1,1}> isCyclic_Store_868(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_Store_865(o213, NULL, i58, env, static) -{1,1}> isCyclic_Load_871(NULL, o213, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58
isCyclic_Store_868(o216, o195, i58, env, static) -{1,1}> isCyclic_Load_872(o195, o216, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_Load_871(NULL, o213, i58, env, static) -{1,1}> isCyclic_NONNULL_877(o213, NULL, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58
isCyclic_Load_872(o195, o216, i58, env, static) -{1,1}> isCyclic_NONNULL_880(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_NONNULL_877(NULL, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_890(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195 && 0 <= o227
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_890(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_906(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_906(o195, o227, i58, env, static) -{1,1}> isCyclic_Load_916(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_916(o227, o195, i58, env, static) -{1,1}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_929(o227, o195, i58, env, static) -{0,0}> isCyclic_NE_954(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
isCyclic_NE_954(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_958(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_958(o195, o227, i58, env, static) -{1,1}> isCyclic_FieldAccess_962(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_962(o252, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 1 + o254 = o252 && 0 < o252
isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) -{1,1}> isCyclic_Store_968(o254, o195, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 0 < o252
isCyclic_Store_968(o254, o195, i58, env, static) -{1,1}> isCyclic_Load_1009(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_Load_1009(o195, o254, i58, env, static) -{1,1}> isCyclic_FieldAccess_1017(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_1017(o270, o254, i58, env, static) -{0,0}> isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) :|: 0 <= o254 && 1 + o272 = o270 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) -{1,1}> isCyclic_Store_1026(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_Store_1026(o272, o254, i58, env, static) -{1,1}> isCyclic_JMP_1030(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_JMP_1030(o272, o254, i58, env, static) -{1,1}> isCyclic_Load_1033(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_Load_1033(o272, o254, i58, env, static) -{0,0}> isCyclic_Load_768(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58

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

obtained
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_47(i1, env, static) :|: 0 >= 0
main_Load_47(i1, env, static) -{1,1}> main_InvokeMethod_51(i1, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, env, static) -{0,0}> main_InvokeMethod_52(i1, env, static) :|: 0 >= 0
main_InvokeMethod_52(i1, env, static) -{1,1}> createList_ConstantStackPush_54(i1, env, static) :|: 0 >= 0
createList_ConstantStackPush_54(i1, env, static) -{1,1}> createList_Store_56(NULL, i1, env, static) :|: NULL = 0
createList_Store_56(NULL, i1, env, static) -{1,1}> createList_Load_59(i1, NULL, env, static) :|: NULL = 0
createList_Load_59(i1, NULL, env, static) -{1,1}> createList_LE_62(i1, NULL, env, static) :|: NULL = 0

obtained
createList_LE_62(i10, 0, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1
by chaining
createList_LE_62(i10, NULL, env, static) -{0,0}> createList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createList_LE_64(i10, NULL, env, static) -{1,1}> createList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createList_New_68(i10, NULL, env, static) -{1,1}> createList_Duplicate_72(o4, i10, NULL, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4
createList_Duplicate_72(o4, i10, NULL, env, static) -{1,1}> createList_New_76(o4, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4
createList_New_76(o4, i10, NULL, env, static) -{1,1}> createList_Duplicate_81(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && o6 = 1
createList_Duplicate_81(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) -{1,1}> createList_Load_88(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_Load_88(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) -{0,0}> createList_InvokeMethod_493(o4, o6, NULL, i10, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && 0 <= NULL

obtained
createList_InvokeMethod_493(o98, o97, o96, i57, i58, 0, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
by chaining
createList_InvokeMethod_493(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Return_511(o98', i57, i58, o96, env, static) :|: NULL = 0 && o98' <= o98 + o96 && 0 < o98' && 1 <= i57 && o98' = o98 + o96 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Return_511(o98, i57, i58, o96, env, static) -{1,1}> createList_Store_512(o98, i57, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Store_512(o98, i57, i58, o96, env, static) -{1,1}> createList_Inc_513(i57, o98, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Inc_513(i57, o98, i58, o96, env, static) -{1,1}> createList_JMP_514(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 1 <= i57 && 0 <= o96 && 1 <= i58 && i57 + -1 = i62 && 0 < o98
createList_JMP_514(i62, o98, i58, o96, env, static) -{1,1}> createList_Load_516(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_516(i62, o98, i58, o96, env, static) -{1,1}> createList_LE_523(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98

obtained
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
by chaining
createList_LE_523(i67, o98, i58, o96, env, static) -{0,0}> createList_LE_526(i67, o98, i58, o96, env, static) :|: 1 <= i67 && 0 <= o96 && 0 <= i67 && 1 <= i58 && 0 < o98
createList_LE_526(i67, o98, i58, o96, env, static) -{1,1}> createList_New_531(i67, o98, i58, o96, env, static) :|: 0 < i67 && 1 <= i67 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_New_531(i67, o98, i58, o96, env, static) -{1,1}> createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && o117 = 1 && 1 <= i58 && 0 < o98
createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o125 && o125 = 1 && 0 < o117 && 1 <= i58 && 0 < o98
createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) -{0,0}> createList_InvokeMethod_493(o117, o125, o98, i67, i58, NULL, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 <= o98 && 0 < o117 && 1 <= i58 && 0 < o98

obtained
createList_LE_523(0, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
by chaining
createList_LE_523(iconst_0, o98, i58, o96, env, static) -{0,0}> createList_LE_525(iconst_0, o98, i58, o96, env, static) :|: 0 <= iconst_0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_LE_525(iconst_0, o98, i58, o96, env, static) -{1,1}> createList_Load_528(o98, i58, o96, env, static) :|: iconst_0 <= 0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_Load_528(o98, i58, o96, env, static) -{1,1}> createList_Return_542(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Return_542(o98, i58, o96, env, static) -{1,1}> main_Store_549(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
main_Store_549(i58, o98, o96, env, static) -{1,1}> main_Load_555(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
main_Load_555(i58, o98, o96, env, static) -{1,1}> main_InvokeMethod_561(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
main_InvokeMethod_561(i58, o98, o96, env, static) -{1,1}> isCyclic_Load_566(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_566(o98, i58, o96, env, static) -{1,1}> isCyclic_NONNULL_579(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_NONNULL_579(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_581(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_581(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_583(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_583(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_585(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_585(o98, i58, o96, env, static) -{1,1}> isCyclic_FieldAccess_587(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_FieldAccess_587(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_589(o96, o98, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_589(o96, o98, i58, env, static) -{1,1}> isCyclic_Load_590(o98, o96, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_590(o98, o96, i58, env, static) -{0,0}> isCyclic_Load_681(o98, o96, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_681(o157, o160, i58, o158, env, static) -{0,0}> isCyclic_Load_768(o157, o160, i58, env, static) :|: 0 <= o158 && 0 < o157 && 1 <= i58 && 0 <= o157 && 0 <= o160

obtained
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
by chaining
isCyclic_NULL_771(o194, o187, i58, env, static) -{0,0}> isCyclic_NULL_773(o194, o187, i58, env, static) :|: 0 < o194 && 0 <= o194 && 1 <= i58 && 0 <= o187
isCyclic_NULL_773(o194, o187, i58, env, static) -{1,1}> isCyclic_Load_776(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_776(o187, o194, i58, env, static) -{1,1}> isCyclic_Load_779(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_779(o187, o194, i58, env, static) -{1,1}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187

obtained
isCyclic_EQ_781(0, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0
by chaining
isCyclic_EQ_781(NULL, o194, i58, env, static) -{0,0}> isCyclic_EQ_785(NULL, o194, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58 && 0 <= NULL
isCyclic_EQ_785(NULL, o194, i58, env, static) -{1,1}> isCyclic_Load_833(NULL, o194, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58
isCyclic_Load_833(NULL, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_853(o194, NULL, i58, env, static) :|: NULL = 0 && 0 < o194 && 1 <= i58
isCyclic_FieldAccess_853(o211, NULL, i58, env, static) -{0,0}> isCyclic_FieldAccess_857(o211, NULL, i58, o213, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58 && 1 + o213 = o211 && 0 < o211
isCyclic_FieldAccess_857(o211, NULL, i58, o213, env, static) -{1,1}> isCyclic_Store_865(o213, NULL, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58 && 0 < o211
isCyclic_Store_865(o213, NULL, i58, env, static) -{1,1}> isCyclic_Load_871(NULL, o213, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58
isCyclic_Load_871(NULL, o213, i58, env, static) -{1,1}> isCyclic_NONNULL_877(o213, NULL, i58, env, static) :|: NULL = 0 && 0 <= o213 && 1 <= i58

obtained
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
by chaining
isCyclic_EQ_784(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_830(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_EQ_830(o195, o194, i58, env, static) -{1,1}> isCyclic_Load_845(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_Load_845(o195, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_855(o194, o195, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_855(o214, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) :|: 1 + o216 = o214 && 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) -{1,1}> isCyclic_Store_868(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_Store_868(o216, o195, i58, env, static) -{1,1}> isCyclic_Load_872(o195, o216, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_Load_872(o195, o216, i58, env, static) -{1,1}> isCyclic_NONNULL_880(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216

obtained
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
by chaining
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_890(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195 && 0 <= o227
isCyclic_NONNULL_890(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_906(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_906(o195, o227, i58, env, static) -{1,1}> isCyclic_Load_916(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_916(o227, o195, i58, env, static) -{1,1}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195

obtained
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
by chaining
isCyclic_NE_929(o227, o195, i58, env, static) -{0,0}> isCyclic_NE_954(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_954(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_958(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_958(o195, o227, i58, env, static) -{1,1}> isCyclic_FieldAccess_962(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_962(o252, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 1 + o254 = o252 && 0 < o252
isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) -{1,1}> isCyclic_Store_968(o254, o195, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 0 < o252
isCyclic_Store_968(o254, o195, i58, env, static) -{1,1}> isCyclic_Load_1009(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_Load_1009(o195, o254, i58, env, static) -{1,1}> isCyclic_FieldAccess_1017(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_1017(o270, o254, i58, env, static) -{0,0}> isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) :|: 0 <= o254 && 1 + o272 = o270 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) -{1,1}> isCyclic_Store_1026(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_Store_1026(o272, o254, i58, env, static) -{1,1}> isCyclic_JMP_1030(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_JMP_1030(o272, o254, i58, env, static) -{1,1}> isCyclic_Load_1033(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_Load_1033(o272, o254, i58, env, static) -{0,0}> isCyclic_Load_768(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58

(8) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
createList_LE_62(i10, 0, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1
createList_InvokeMethod_493(o98, o97, o96, i57, i58, 0, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_523(0, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_781(0, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_NONNULL_877(NULL, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195

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

Moved arithmethic from lhss to constraints.

createList_LE_523(0, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
was transformed to
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0

createList_InvokeMethod_493(o98, o97, o96, i57, i58, 0, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
was transformed to
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0

createList_LE_62(i10, 0, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1
was transformed to
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0

isCyclic_EQ_781(0, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0
was transformed to
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0

(10) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NONNULL_877(NULL, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0

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

Linearized lhss.

isCyclic_NONNULL_877(NULL, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL
was transformed to
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

(12) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

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

Moved arithmethic from constraints to rhss.

createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
was transformed to
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0

isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
was transformed to
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(0, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187

createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
was transformed to
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0

isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
was transformed to
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58

isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
was transformed to
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(0, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL

isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL
was transformed to
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(0, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

(14) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(0, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(0, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(0, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

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

Simplified expressions.

createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
was transformed to
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96

createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
was transformed to
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
was transformed to
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 < o226 && 1 <= i58

main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
was transformed to
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
was transformed to
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 - 1, o98 + o96, i58, o96, env, static) :|: 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 - 1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0

isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
was transformed to
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194

createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
was transformed to
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 < o98 && x = 0

isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
was transformed to
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195

isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0
was transformed to
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && x = 0

isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
was transformed to
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o195 && 0 < o227 && 1 <= i58

(16) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(0, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(0, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o195 && 0 < o227 && 1 <= i58
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && x = 0
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 < o226 && 1 <= i58
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 < o98 && x = 0
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 - 1, o98 + o96, i58, o96, env, static) :|: 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 - 1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(0, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187

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

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

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(NULL, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, NULL, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(NULL, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(NULL, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 1 <= i10 && 0 < 1 && x = 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194 && 0 <= o194
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(0, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && 0 <= 0 && x = 0
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 <= o226 && 0 < o226 && 1 <= i58
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 <= o227 && 0 < o195 && 0 < o227 && 1 <= i58
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(0, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(0, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL

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

Simplified expressions.

(28) Obligation:

IntTrs with 19 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
isCyclic_NE_929(o242, o195, i58, env, static) -{0,0}> isCyclic_NE_955(o242, i58, env, static) :|: 0 < o242 && 1 <= i58 && 0 < o195
isCyclic_NONNULL_877(NULL, x, i58, env, static) -{0,0}> isCyclic_NONNULL_888(0, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && x = NULL
createList_LE_62(i9, NULL, env, static) -{0,0}> createList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
isCyclic_EQ_784(o195, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_880(o216', o195, i58, env, static) :|: 1 + o216' = o194 && 0 <= o216' && 0 < o195 && 1 <= i58 && 0 < o194
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_NONNULL_880(NULL, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_891(0, o195, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 < o195 && 0 <= NULL
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{3,3}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o195 && 0 < o227 && 1 <= i58
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96
isCyclic_NE_929(o227, o195, i58, env, static) -{8,8}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o254' = o227 && 1 <= i58 && 0 < o227 && 0 <= o254' && 0 <= o272' && 1 + o272' = o195 && 0 < o195
isCyclic_EQ_781(x, o194, i58, env, static) -{5,5}> isCyclic_NONNULL_877(o213', 0, i58, env, static) :|: 0 < o194 && 1 <= i58 && 1 + o213' = o194 && 0 <= o213' && x = 0
main_Load_1(i1, env, static) -{20,20}> createList_LE_62(i1, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
isCyclic_NONNULL_877(o226, NULL, i58, env, static) -{0,0}> isCyclic_NONNULL_887(o226, 0, i58, env, static) :|: NULL = 0 && 0 < o226 && 1 <= i58
createList_LE_523(x, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 < o98 && x = 0
isCyclic_EQ_784(o198, o194, i58, env, static) -{0,0}> isCyclic_EQ_831(o198, i58, env, static) :|: 0 < o198 && 0 < o194 && 1 <= i58
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(o194, o187, i58, env, static) -{3,3}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 < o194
createList_LE_62(i10, x, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, 0, i10, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58, x, env, static) -{14,14}> createList_LE_523(i57 - 1, o98 + o96, i58, o96, env, static) :|: 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 - 1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98 && x = 0
isCyclic_NULL_771(NULL, o187, i58, env, static) -{0,0}> isCyclic_NULL_774(0, o187, i58, env, static) :|: NULL = 0 && 1 <= i58 && 0 <= NULL && 0 <= o187

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

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

(30) Obligation:

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

Used field analysis yielded the following read fields:
- ObjectList: [next]

Considered paths: all paths from start

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

Transformed 106 jbc graph edges to a weighted ITS with 106 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 106 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_47(i1, env, static) :|: 0 >= 0
main_Load_47(i1, env, static) -{1,1}> main_InvokeMethod_51(i1, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, env, static) -{0,0}> main_InvokeMethod_52(i1, env, static) :|: 0 >= 0
main_InvokeMethod_52(i1, env, static) -{1,1}> createList_ConstantStackPush_54(i1, env, static) :|: 0 >= 0
createList_ConstantStackPush_54(i1, env, static) -{1,1}> createList_Store_56(NULL, i1, env, static) :|: NULL = 0
createList_Store_56(NULL, i1, env, static) -{1,1}> createList_Load_59(i1, NULL, env, static) :|: NULL = 0
createList_Load_59(i1, NULL, env, static) -{1,1}> createList_LE_62(i1, NULL, env, static) :|: NULL = 0
createList_LE_62(i10, NULL, env, static) -{0,0}> createList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createList_LE_64(i10, NULL, env, static) -{1,1}> createList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createList_New_68(i10, NULL, env, static) -{1,1}> createList_Duplicate_72(o4, i10, NULL, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4
createList_Duplicate_72(o4, i10, NULL, env, static) -{1,1}> createList_New_76(o4, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4
createList_New_76(o4, i10, NULL, env, static) -{1,1}> createList_Duplicate_81(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && o6 = 1
createList_Duplicate_81(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) -{1,1}> createList_Load_88(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_Load_88(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) -{0,0}> createList_InvokeMethod_493(o4, o6, NULL, i10, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && 0 <= NULL
createList_InvokeMethod_493(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_494(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_InvokeMethod_496(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_498(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_500(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_502(o98, o97, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 0 < o97 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_505(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Load_507(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) :|: NULL = 0 && 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_FieldAccess_509(o98, o96, i57, i58, NULL, env, static) -{1,1}> langle_init_rangle_Return_511(o98', i57, i58, o96, env, static) :|: NULL = 0 && o98' <= o98 + o96 && 0 < o98' && 1 <= i57 && o98' = o98 + o96 && 0 <= o96 && 1 <= i58 && 0 < o98
langle_init_rangle_Return_511(o98, i57, i58, o96, env, static) -{1,1}> createList_Store_512(o98, i57, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Store_512(o98, i57, i58, o96, env, static) -{1,1}> createList_Inc_513(i57, o98, i58, o96, env, static) :|: 1 <= i57 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Inc_513(i57, o98, i58, o96, env, static) -{1,1}> createList_JMP_514(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 1 <= i57 && 0 <= o96 && 1 <= i58 && i57 + -1 = i62 && 0 < o98
createList_JMP_514(i62, o98, i58, o96, env, static) -{1,1}> createList_Load_516(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_516(i62, o98, i58, o96, env, static) -{1,1}> createList_LE_523(i62, o98, i58, o96, env, static) :|: 0 <= i62 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_LE_523(iconst_0, o98, i58, o96, env, static) -{0,0}> createList_LE_525(iconst_0, o98, i58, o96, env, static) :|: 0 <= iconst_0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_LE_523(i67, o98, i58, o96, env, static) -{0,0}> createList_LE_526(i67, o98, i58, o96, env, static) :|: 1 <= i67 && 0 <= o96 && 0 <= i67 && 1 <= i58 && 0 < o98
createList_LE_525(iconst_0, o98, i58, o96, env, static) -{1,1}> createList_Load_528(o98, i58, o96, env, static) :|: iconst_0 <= 0 && 0 <= o96 && iconst_0 = 0 && 1 <= i58 && 0 < o98
createList_LE_526(i67, o98, i58, o96, env, static) -{1,1}> createList_New_531(i67, o98, i58, o96, env, static) :|: 0 < i67 && 1 <= i67 && 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_528(o98, i58, o96, env, static) -{1,1}> createList_Return_542(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_New_531(i67, o98, i58, o96, env, static) -{1,1}> createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && o117 = 1 && 1 <= i58 && 0 < o98
createList_Return_542(o98, i58, o96, env, static) -{1,1}> main_Store_549(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Duplicate_546(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
main_Store_549(i58, o98, o96, env, static) -{1,1}> main_Load_555(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_New_552(o117, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 <= o96 && 0 < o125 && o125 = 1 && 0 < o117 && 1 <= i58 && 0 < o98
main_Load_555(i58, o98, o96, env, static) -{1,1}> main_InvokeMethod_561(i58, o98, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Duplicate_558(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
main_InvokeMethod_561(i58, o98, o96, env, static) -{1,1}> isCyclic_Load_566(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_InvokeMethod_564(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
isCyclic_Load_566(o98, i58, o96, env, static) -{1,1}> isCyclic_NONNULL_579(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
createList_Load_569(o117, o125, i67, o98, i58, NULL, o96, env, static) -{1,1}> createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 < o117 && 1 <= i58 && 0 < o98
createList_InvokeMethod_576(o117, o125, o98, i67, i58, NULL, o96, env, static) -{0,0}> createList_InvokeMethod_493(o117, o125, o98, i67, i58, NULL, env, static) :|: NULL = 0 && 1 <= i67 && 0 < o125 && 0 <= o96 && 0 <= o98 && 0 < o117 && 1 <= i58 && 0 < o98
isCyclic_NONNULL_579(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_581(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_581(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_583(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_583(o98, i58, o96, env, static) -{1,1}> isCyclic_Load_585(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_585(o98, i58, o96, env, static) -{1,1}> isCyclic_FieldAccess_587(o98, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_FieldAccess_587(o98, i58, o96, env, static) -{1,1}> isCyclic_Store_589(o96, o98, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Store_589(o96, o98, i58, env, static) -{1,1}> isCyclic_Load_590(o98, o96, i58, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_590(o98, o96, i58, env, static) -{0,0}> isCyclic_Load_681(o98, o96, i58, o96, env, static) :|: 0 <= o96 && 1 <= i58 && 0 < o98
isCyclic_Load_681(o157, o160, i58, o158, env, static) -{0,0}> isCyclic_Load_768(o157, o160, i58, env, static) :|: 0 <= o158 && 0 < o157 && 1 <= i58 && 0 <= o157 && 0 <= o160
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(o194, o187, i58, env, static) -{0,0}> isCyclic_NULL_773(o194, o187, i58, env, static) :|: 0 < o194 && 0 <= o194 && 1 <= i58 && 0 <= o187
isCyclic_NULL_773(o194, o187, i58, env, static) -{1,1}> isCyclic_Load_776(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_776(o187, o194, i58, env, static) -{1,1}> isCyclic_Load_779(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_779(o187, o194, i58, env, static) -{1,1}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_784(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_830(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_EQ_830(o195, o194, i58, env, static) -{1,1}> isCyclic_Load_845(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_Load_845(o195, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_855(o194, o195, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_855(o214, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) :|: 1 + o216 = o214 && 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) -{1,1}> isCyclic_Store_868(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_Store_868(o216, o195, i58, env, static) -{1,1}> isCyclic_Load_872(o195, o216, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_Load_872(o195, o216, i58, env, static) -{1,1}> isCyclic_NONNULL_880(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_890(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195 && 0 <= o227
isCyclic_NONNULL_890(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_906(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_906(o195, o227, i58, env, static) -{1,1}> isCyclic_Load_916(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_916(o227, o195, i58, env, static) -{1,1}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_929(o227, o195, i58, env, static) -{0,0}> isCyclic_NE_954(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_954(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_958(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_958(o195, o227, i58, env, static) -{1,1}> isCyclic_FieldAccess_962(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_962(o252, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 1 + o254 = o252 && 0 < o252
isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) -{1,1}> isCyclic_Store_968(o254, o195, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 0 < o252
isCyclic_Store_968(o254, o195, i58, env, static) -{1,1}> isCyclic_Load_1009(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_Load_1009(o195, o254, i58, env, static) -{1,1}> isCyclic_FieldAccess_1017(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_1017(o270, o254, i58, env, static) -{0,0}> isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) :|: 0 <= o254 && 1 + o272 = o270 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) -{1,1}> isCyclic_Store_1026(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_Store_1026(o272, o254, i58, env, static) -{1,1}> isCyclic_JMP_1030(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_JMP_1030(o272, o254, i58, env, static) -{1,1}> isCyclic_Load_1033(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_Load_1033(o272, o254, i58, env, static) -{0,0}> isCyclic_Load_768(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58

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

obtained
main_Load_1(i1, env, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
by chaining
main_Load_1(i1, env, static) -{0,0}> main_Load_3(i1, env, static) :|: 0 >= 0
main_Load_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, env, static) -{1,1}> main_Load_41(i1, env, static) :|: 0 >= 0
main_Load_41(i1, env, static) -{0,0}> main_Load_42(i1, env, static) :|: 0 >= 0
main_Load_42(i1, env, static) -{0,0}> main_Load_43(i1, env, static) :|: 0 <= static
main_Load_43(i1, env, static) -{0,0}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_47(i1, env, static) :|: 0 >= 0
main_Load_47(i1, env, static) -{1,1}> main_InvokeMethod_51(i1, env, static) :|: 0 >= 0
main_InvokeMethod_51(i1, env, static) -{0,0}> main_InvokeMethod_52(i1, env, static) :|: 0 >= 0
main_InvokeMethod_52(i1, env, static) -{1,1}> createList_ConstantStackPush_54(i1, env, static) :|: 0 >= 0
createList_ConstantStackPush_54(i1, env, static) -{1,1}> createList_Store_56(NULL, i1, env, static) :|: NULL = 0
createList_Store_56(NULL, i1, env, static) -{1,1}> createList_Load_59(i1, NULL, env, static) :|: NULL = 0
createList_Load_59(i1, NULL, env, static) -{1,1}> createList_LE_62(i1, NULL, env, static) :|: NULL = 0
createList_LE_62(i10, NULL, env, static) -{0,0}> createList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createList_LE_64(i10, NULL, env, static) -{1,1}> createList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createList_New_68(i10, NULL, env, static) -{1,1}> createList_Duplicate_72(o4, i10, NULL, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4
createList_Duplicate_72(o4, i10, NULL, env, static) -{1,1}> createList_New_76(o4, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4
createList_New_76(o4, i10, NULL, env, static) -{1,1}> createList_Duplicate_81(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && o6 = 1
createList_Duplicate_81(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_84(o4, o6, i10, NULL, env, static) -{1,1}> createList_Load_88(o4, o6, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_Load_88(o4, o6, i10, NULL, env, static) -{1,1}> createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4
createList_InvokeMethod_90(o4, o6, NULL, i10, env, static) -{0,0}> createList_InvokeMethod_493(o4, o6, NULL, i10, i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o6 && 0 < o4 && 0 <= NULL

obtained
isCyclic_Load_768(o187, o188, i58, env, static) -{20,20}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187
by chaining
isCyclic_Load_768(o187, o188, i58, env, static) -{1,1}> isCyclic_NULL_771(o188, o187, i58, env, static) :|: 1 <= i58 && 0 <= o187 && 0 <= o188
isCyclic_NULL_771(o194, o187, i58, env, static) -{0,0}> isCyclic_NULL_773(o194, o187, i58, env, static) :|: 0 < o194 && 0 <= o194 && 1 <= i58 && 0 <= o187
isCyclic_NULL_773(o194, o187, i58, env, static) -{1,1}> isCyclic_Load_776(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_776(o187, o194, i58, env, static) -{1,1}> isCyclic_Load_779(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_Load_779(o187, o194, i58, env, static) -{1,1}> isCyclic_EQ_781(o187, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 <= o187
isCyclic_EQ_781(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_784(o195, o194, i58, env, static) :|: 0 < o194 && 0 <= o195 && 1 <= i58 && 0 < o195
isCyclic_EQ_784(o195, o194, i58, env, static) -{0,0}> isCyclic_EQ_830(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_EQ_830(o195, o194, i58, env, static) -{1,1}> isCyclic_Load_845(o195, o194, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_Load_845(o195, o194, i58, env, static) -{1,1}> isCyclic_FieldAccess_855(o194, o195, i58, env, static) :|: 0 < o194 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_855(o214, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) :|: 1 + o216 = o214 && 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_FieldAccess_861(o214, o195, i58, o216, env, static) -{1,1}> isCyclic_Store_868(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o214 && 0 < o195 && 0 <= o216
isCyclic_Store_868(o216, o195, i58, env, static) -{1,1}> isCyclic_Load_872(o195, o216, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_Load_872(o195, o216, i58, env, static) -{1,1}> isCyclic_NONNULL_880(o216, o195, i58, env, static) :|: 1 <= i58 && 0 < o195 && 0 <= o216
isCyclic_NONNULL_880(o227, o195, i58, env, static) -{0,0}> isCyclic_NONNULL_890(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195 && 0 <= o227
isCyclic_NONNULL_890(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_906(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_906(o195, o227, i58, env, static) -{1,1}> isCyclic_Load_916(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_916(o227, o195, i58, env, static) -{1,1}> isCyclic_NE_929(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_929(o227, o195, i58, env, static) -{0,0}> isCyclic_NE_954(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_NE_954(o227, o195, i58, env, static) -{1,1}> isCyclic_Load_958(o195, o227, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_Load_958(o195, o227, i58, env, static) -{1,1}> isCyclic_FieldAccess_962(o227, o195, i58, env, static) :|: 0 < o227 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_962(o252, o195, i58, env, static) -{0,0}> isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 1 + o254 = o252 && 0 < o252
isCyclic_FieldAccess_965(o252, o195, i58, o254, env, static) -{1,1}> isCyclic_Store_968(o254, o195, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195 && 0 < o252
isCyclic_Store_968(o254, o195, i58, env, static) -{1,1}> isCyclic_Load_1009(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_Load_1009(o195, o254, i58, env, static) -{1,1}> isCyclic_FieldAccess_1017(o195, o254, i58, env, static) :|: 0 <= o254 && 1 <= i58 && 0 < o195
isCyclic_FieldAccess_1017(o270, o254, i58, env, static) -{0,0}> isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) :|: 0 <= o254 && 1 + o272 = o270 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_FieldAccess_1024(o270, o254, i58, o272, env, static) -{1,1}> isCyclic_Store_1026(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58 && 0 < o270
isCyclic_Store_1026(o272, o254, i58, env, static) -{1,1}> isCyclic_JMP_1030(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_JMP_1030(o272, o254, i58, env, static) -{1,1}> isCyclic_Load_1033(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58
isCyclic_Load_1033(o272, o254, i58, env, static) -{0,0}> isCyclic_Load_768(o272, o254, i58, env, static) :|: 0 <= o254 && 0 <= o272 && 1 <= i58

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, env, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
createList_InvokeMethod_493(o98, o97, o96, i57, i58, 0, env, static) -{14,14}> createList_LE_523(i62', o98''', i58, o96, env, static) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
createList_LE_523(i67, o98, i58, o96, env, static) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58, 0, env, static) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_523(0, o98, i58, o96, env, static) -{13,13}> isCyclic_Load_768(o98, o96, i58, env, static) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
isCyclic_Load_768(o187, o188, i58, env, static) -{20,20}> isCyclic_Load_768(o272', o254', i58, env, static) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187

(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_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
createList_InvokeMethod_493(x1, x2, x3, x4, x5, x6, x7, x8) → createList_InvokeMethod_493(x1, x2, x3, x4, x5)
createList_LE_523(x1, x2, x3, x4, x5, x6) → createList_LE_523(x1, x2, x3, x4)
isCyclic_Load_768(x1, x2, x3, x4, x5) → isCyclic_Load_768(x1, x2, x3)

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i62', o98''', i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
createList_LE_523(0, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187

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

Moved arithmethic from lhss to constraints.

createList_LE_523(0, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98
was transformed to
createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i62', o98''', i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187
createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67

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

Moved arithmethic from constraints to rhss.

createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i62', o98''', i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
was transformed to
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98

(40) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187
createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67

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

Simplified expressions.

main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 >= 0 && 0 < 1 && 0 <= 2 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i1
was transformed to
main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= static && 0 <= static'1 && 0 < i1

createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 <= o98 && 0 <= 0 && 0 < o98 && x = 0
was transformed to
createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 < o98 && x = 0

isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o187 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 <= o188 && 0 <= o216' && 0 < o216' && 0 < o187
was transformed to
isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 < o216' && 0 < o187

createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i57 + -1, o98 + o96, i58, o96) :|: o98''' <= o98 + o96 && 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 + -1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98
was transformed to
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i57 - 1, o98 + o96, i58, o96) :|: 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 - 1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98

createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96 && 0 < 1 && 0 <= o98 && 0 <= i67
was transformed to
createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96

(42) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i1, static) -{27,27}> createList_InvokeMethod_493(1, 1, 0, i1, i1) :|: static'1 <= static''' + 1 && 0 <= static''' && 1 <= i1 && static''' <= static + 2 && 0 <= static && 0 <= static'1 && 0 < i1
createList_LE_523(i67, o98, i58, o96) -{7,7}> createList_InvokeMethod_493(1, 1, o98, i67, i58) :|: 0 < i67 && 0 < o98 && 1 <= i67 && 1 <= i58 && 0 <= o96
isCyclic_Load_768(o187, o188, i58) -{20,20}> isCyclic_Load_768(o272', o254', i58) :|: 1 + o216' = o188 && 1 <= i58 && 0 <= o254' && 0 <= o272' && 1 + o254' = o216' && 0 < o188 && 1 + o272' = o187 && 0 < o216' && 0 < o187
createList_LE_523(x, o98, i58, o96) -{13,13}> isCyclic_Load_768(o98, o96, i58) :|: 1 <= i58 && 0 <= o96 && 0 < o98 && x = 0
createList_InvokeMethod_493(o98, o97, o96, i57, i58) -{14,14}> createList_LE_523(i57 - 1, o98 + o96, i58, o96) :|: 0 < o98''' && o98''' = o98 + o96 && 1 <= i58 && i57 - 1 = i62' && 0 <= i62' && 0 <= o96 && 1 <= i57 && 0 < o97 && 0 < o98

(43) koat Proof (EQUIVALENT transformation)

YES(?, 123*ar_0 + 40)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, 0, ar_0, ar_0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ 1 <= ar_0 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 7) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, ar_1, ar_0, ar_2)) [ 0 < ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 20) isCyclic_Load_768(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(o272', o254', ar_2, arityPad, arityPad)) [ o216' + 1 = ar_1 /\ 1 <= ar_2 /\ 0 <= o254' /\ 0 <= o272' /\ o254' + 1 = o216' /\ 0 < ar_1 /\ o272' + 1 = ar_0 /\ 0 < o216' /\ 0 < ar_0 ]
(Comp: ?, Cost: 13) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(ar_1, ar_3, ar_2, arityPad, arityPad)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 14) createList_InvokeMethod_493(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_523(ar_3 - 1, ar_0 + ar_2, ar_4, ar_2, arityPad)) [ 0 < o98''' /\ o98''' = ar_0 + ar_2 /\ 1 <= ar_4 /\ ar_3 - 1 = i62' /\ 0 <= i62' /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, 0, ar_0, ar_0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ 1 <= ar_0 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 7) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, ar_1, ar_0, ar_2)) [ 0 < ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 20) isCyclic_Load_768(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(o272', o254', ar_2, arityPad, arityPad)) [ o216' + 1 = ar_1 /\ 1 <= ar_2 /\ 0 <= o254' /\ 0 <= o272' /\ o254' + 1 = o216' /\ 0 < ar_1 /\ o272' + 1 = ar_0 /\ 0 < o216' /\ 0 < ar_0 ]
(Comp: ?, Cost: 13) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(ar_1, ar_3, ar_2, arityPad, arityPad)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 14) createList_InvokeMethod_493(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_523(ar_3 - 1, ar_0 + ar_2, ar_4, ar_2, arityPad)) [ 0 < o98''' /\ o98''' = ar_0 + ar_2 /\ 1 <= ar_4 /\ ar_3 - 1 = i62' /\ 0 <= i62' /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = 1
Pol(createList_InvokeMethod_493) = 1
Pol(createList_LE_523) = 1
Pol(isCyclic_Load_768) = 0
Pol(koat_start) = 1
orients all transitions weakly and the transition
createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(ar_1, ar_3, ar_2, arityPad, arityPad)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ ar_0 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, 0, ar_0, ar_0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ 1 <= ar_0 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 7) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, ar_1, ar_0, ar_2)) [ 0 < ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 20) isCyclic_Load_768(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(o272', o254', ar_2, arityPad, arityPad)) [ o216' + 1 = ar_1 /\ 1 <= ar_2 /\ 0 <= o254' /\ 0 <= o272' /\ o254' + 1 = o216' /\ 0 < ar_1 /\ o272' + 1 = ar_0 /\ 0 < o216' /\ 0 < ar_0 ]
(Comp: 1, Cost: 13) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(ar_1, ar_3, ar_2, arityPad, arityPad)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ ar_0 = 0 ]
(Comp: ?, Cost: 14) createList_InvokeMethod_493(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_523(ar_3 - 1, ar_0 + ar_2, ar_4, ar_2, arityPad)) [ 0 < o98''' /\ o98''' = ar_0 + ar_2 /\ 1 <= ar_4 /\ ar_3 - 1 = i62' /\ 0 <= i62' /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = 3*V_1
Pol(createList_InvokeMethod_493) = V_1 + V_3 + 3*V_4 - 2
Pol(createList_LE_523) = 3*V_1 + V_2
Pol(isCyclic_Load_768) = V_1
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
isCyclic_Load_768(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(o272', o254', ar_2, arityPad, arityPad)) [ o216' + 1 = ar_1 /\ 1 <= ar_2 /\ 0 <= o254' /\ 0 <= o272' /\ o254' + 1 = o216' /\ 0 < ar_1 /\ o272' + 1 = ar_0 /\ 0 < o216' /\ 0 < ar_0 ]
createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, ar_1, ar_0, ar_2)) [ 0 < ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 <= ar_3 ]
createList_InvokeMethod_493(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_523(ar_3 - 1, ar_0 + ar_2, ar_4, ar_2, arityPad)) [ 0 < o98''' /\ o98''' = ar_0 + ar_2 /\ 1 <= ar_4 /\ ar_3 - 1 = i62' /\ 0 <= i62' /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_1 /\ 0 < ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 27) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, 0, ar_0, ar_0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ 1 <= ar_0 /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 /\ 0 < ar_0 ]
(Comp: 3*ar_0, Cost: 7) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_InvokeMethod_493(1, 1, ar_1, ar_0, ar_2)) [ 0 < ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 <= ar_3 ]
(Comp: 3*ar_0, Cost: 20) isCyclic_Load_768(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(o272', o254', ar_2, arityPad, arityPad)) [ o216' + 1 = ar_1 /\ 1 <= ar_2 /\ 0 <= o254' /\ 0 <= o272' /\ o254' + 1 = o216' /\ 0 < ar_1 /\ o272' + 1 = ar_0 /\ 0 < o216' /\ 0 < ar_0 ]
(Comp: 1, Cost: 13) createList_LE_523(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(isCyclic_Load_768(ar_1, ar_3, ar_2, arityPad, arityPad)) [ 1 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ ar_0 = 0 ]
(Comp: 3*ar_0, Cost: 14) createList_InvokeMethod_493(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_523(ar_3 - 1, ar_0 + ar_2, ar_4, ar_2, arityPad)) [ 0 < o98''' /\ o98''' = ar_0 + ar_2 /\ 1 <= ar_4 /\ ar_3 - 1 = i62' /\ 0 <= i62' /\ 0 <= ar_2 /\ 1 <= ar_3 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 123*ar_0 + 40

Time: 0.218 sec (SMT: 0.198 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(62)) 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(67)) 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) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

(43) koat Proof (EQUIVALENT transformation)

(44) BOUNDS(CONSTANT, 40 + 123 * |#0|)