time complexity proof of /tmp/tmpTJbCQp/ListContent.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(82, 63 + 19 * #0)).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 CESProof (⇔, 238 ms)

        ↳26 BOUNDS(CONSTANT, max(55, 36 + 19 * #0))

↳27 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(27)), 1 ms)

↳28 JBCComplexityEdges

    ↳29 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 244 ms)

    ↳30 WeightedIntTrs

    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 ms)

    ↳32 WeightedIntTrs

    ↳33 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 45 ms)

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class ListContent{

  public static void main(int i) {
    IntList l = IntList.createIntList(i);

    while (l.value > 0) l.value--;
  }

}

class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public static IntList createIntList(int i) {

    IntList l = null;

    while (i > 0) {
      l = new IntList(i, l);
      i--;
    }

    return l;
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- IntList: [value]

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 81 jbc graph edges to a weighted ITS with 81 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 81 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_12(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_12(i2, env, static) -{0,0}> langle_clinit_rangle_New_13(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_13(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o1, i2, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_17(o1, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_23(o1, i2, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_23(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Load_28(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_30(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_33(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_35(o1, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 >= 0
main_Load_47(i2, env, static) -{1,1}> main_InvokeMethod_49(i2, env, static) :|: 0 >= 0
main_InvokeMethod_49(i2, env, static) -{0,0}> main_InvokeMethod_50(i2, env, static) :|: 0 >= 0
main_InvokeMethod_50(i2, env, static) -{1,1}> createIntList_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_52(i2, env, static) -{1,1}> createIntList_Store_56(NULL, i2, env, static) :|: NULL = 0
createIntList_Store_56(NULL, i2, env, static) -{1,1}> createIntList_Load_58(i2, NULL, env, static) :|: NULL = 0
createIntList_Load_58(i2, NULL, env, static) -{1,1}> createIntList_LE_62(i2, NULL, env, static) :|: NULL = 0
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
createIntList_LE_62(i10, NULL, env, static) -{0,0}> createIntList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createIntList_LE_64(i10, NULL, env, static) -{1,1}> createIntList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createIntList_New_68(i10, NULL, env, static) -{1,1}> createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_355(o4, i10, NULL, i10, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0 && 0 <= NULL
langle_init_rangle_Load_355(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_363(o88', o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && o88' <= o88 + i67 && 0 < o88' && 0 < o88 && iconst_0 = 0 && o88 < o88' && 1 <= i68
langle_init_rangle_Load_363(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Return_371(o88, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Return_371(o88, i67, i68, env, static) -{1,1}> createIntList_Store_373(o88, i67, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Store_373(o88, i67, i68, env, static) -{1,1}> createIntList_Inc_375(i67, o88, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Inc_375(i67, o88, i68, env, static) -{1,1}> createIntList_JMP_378(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && i67 + -1 = i76 && 0 < o88 && 1 <= i68
createIntList_JMP_378(i76, o88, i68, i67, env, static) -{1,1}> createIntList_Load_380(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68
createIntList_Load_380(i76, o88, i68, i67, env, static) -{1,1}> createIntList_LE_388(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68
createIntList_LE_388(iconst_0, o88, i68, i67, env, static) -{0,0}> createIntList_LE_390(iconst_0, o88, i68, i67, env, static) :|: 0 <= iconst_0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_LE_388(i83, o88, i68, i84, env, static) -{0,0}> createIntList_LE_391(i83, o88, i68, i84, env, static) :|: 1 <= i84 && 2 <= i84 && 1 <= i83 && 0 < o88 && 1 <= i68 && 0 <= i83
createIntList_LE_390(iconst_0, o88, i68, i67, env, static) -{1,1}> createIntList_Load_393(o88, i68, i67, env, static) :|: iconst_0 <= 0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_LE_391(i83, o88, i68, i84, env, static) -{1,1}> createIntList_New_395(i83, o88, i68, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83 && 1 <= i68
createIntList_Load_393(o88, i68, i67, env, static) -{1,1}> createIntList_Return_397(o88, i68, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_New_395(i83, o88, i68, i84, env, static) -{1,1}> createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) :|: o109 = 1 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < o109 && iconst_0 = 0 && 1 <= i68
createIntList_Return_397(o88, i68, i67, env, static) -{1,1}> main_Store_402(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Store_402(i68, o88, i67, env, static) -{1,1}> main_Load_405(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Load_405(i68, o88, i67, env, static) -{0,0}> main_Load_438(i68, o88, i67, env, static) :|: 1 <= i67 && 0 <= i67 && 0 < o88 && 1 <= i68
createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) -{0,0}> langle_init_rangle_Load_355(o109, i83, o88, i68, iconst_0, env, static) :|: 2 <= i84 && 1 <= i83 && 0 <= o88 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Load_438(i68, o135, i97, env, static) -{1,1}> main_FieldAccess_462(i68, o135, i97, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_FieldAccess_462(i68, o135, i97, env, static) -{1,1}> main_LE_465(i68, i97, o135, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, iconst_0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{0,0}> main_LE_468(i68, i105, o135, env, static) :|: 0 < o135 && 0 <= i105 && 1 <= i68 && 1 <= i105
main_LE_468(i68, i105, o135, env, static) -{1,1}> main_Load_472(i68, o135, i105, env, static) :|: 0 < o135 && 0 < i105 && 1 <= i68 && 1 <= i105
main_Load_472(i68, o135, i105, env, static) -{1,1}> main_Duplicate_476(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_Duplicate_476(i68, o135, i105, env, static) -{1,1}> main_FieldAccess_478(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_FieldAccess_478(i68, o135, i105, env, static) -{1,1}> main_ConstantStackPush_480(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_ConstantStackPush_480(i68, o135, i105, env, static) -{1,1}> main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) :|: 0 < o135 && iconst_1 = 1 && 1 <= i68 && 1 <= i105
main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) -{1,1}> main_FieldAccess_484(i68, o135, i107, i105, env, static) :|: 0 < o135 && i105 - iconst_1 = i107 && iconst_1 = 1 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_FieldAccess_484(i68, o135, i107, i105, env, static) -{1,1}> main_JMP_487(i68, o135', i107, env, static) :|: 0 < o135 && o135' <= o135 + i107 && 0 < o135' && o135' < o135 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_JMP_487(i68, o135, i107, env, static) -{1,1}> main_Load_492(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107
main_Load_492(i68, o135, i107, env, static) -{0,0}> main_Load_438(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107

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

obtained
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1 && 0 >= 0
by chaining
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_12(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_12(i2, env, static) -{0,0}> langle_clinit_rangle_New_13(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_13(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o1, i2, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_17(o1, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_23(o1, i2, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_23(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Load_28(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_30(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_33(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_35(o1, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 >= 0
main_Load_47(i2, env, static) -{1,1}> main_InvokeMethod_49(i2, env, static) :|: 0 >= 0
main_InvokeMethod_49(i2, env, static) -{0,0}> main_InvokeMethod_50(i2, env, static) :|: 0 >= 0
main_InvokeMethod_50(i2, env, static) -{1,1}> createIntList_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_52(i2, env, static) -{1,1}> createIntList_Store_56(NULL, i2, env, static) :|: NULL = 0
createIntList_Store_56(NULL, i2, env, static) -{1,1}> createIntList_Load_58(i2, NULL, env, static) :|: NULL = 0
createIntList_Load_58(i2, NULL, env, static) -{1,1}> createIntList_LE_62(i2, NULL, env, static) :|: NULL = 0

obtained
createIntList_LE_62(i10, 0, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10
by chaining
createIntList_LE_62(i10, NULL, env, static) -{0,0}> createIntList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createIntList_LE_64(i10, NULL, env, static) -{1,1}> createIntList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createIntList_New_68(i10, NULL, env, static) -{1,1}> createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_355(o4, i10, NULL, i10, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0 && 0 <= NULL

obtained
langle_init_rangle_Load_355(o88, i67, o89, i68, 0, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
by chaining
langle_init_rangle_Load_355(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_363(o88', o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && o88' <= o88 + i67 && 0 < o88' && 0 < o88 && iconst_0 = 0 && o88 < o88' && 1 <= i68
langle_init_rangle_Load_363(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Return_371(o88, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Return_371(o88, i67, i68, env, static) -{1,1}> createIntList_Store_373(o88, i67, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Store_373(o88, i67, i68, env, static) -{1,1}> createIntList_Inc_375(i67, o88, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Inc_375(i67, o88, i68, env, static) -{1,1}> createIntList_JMP_378(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && i67 + -1 = i76 && 0 < o88 && 1 <= i68
createIntList_JMP_378(i76, o88, i68, i67, env, static) -{1,1}> createIntList_Load_380(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68
createIntList_Load_380(i76, o88, i68, i67, env, static) -{1,1}> createIntList_LE_388(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68

obtained
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
by chaining
createIntList_LE_388(i83, o88, i68, i84, env, static) -{0,0}> createIntList_LE_391(i83, o88, i68, i84, env, static) :|: 1 <= i84 && 2 <= i84 && 1 <= i83 && 0 < o88 && 1 <= i68 && 0 <= i83
createIntList_LE_391(i83, o88, i68, i84, env, static) -{1,1}> createIntList_New_395(i83, o88, i68, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83 && 1 <= i68
createIntList_New_395(i83, o88, i68, i84, env, static) -{1,1}> createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) :|: o109 = 1 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < o109 && iconst_0 = 0 && 1 <= i68
createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) -{0,0}> langle_init_rangle_Load_355(o109, i83, o88, i68, iconst_0, env, static) :|: 2 <= i84 && 1 <= i83 && 0 <= o88 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68

obtained
createIntList_LE_388(0, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
by chaining
createIntList_LE_388(iconst_0, o88, i68, i67, env, static) -{0,0}> createIntList_LE_390(iconst_0, o88, i68, i67, env, static) :|: 0 <= iconst_0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_LE_390(iconst_0, o88, i68, i67, env, static) -{1,1}> createIntList_Load_393(o88, i68, i67, env, static) :|: iconst_0 <= 0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_Load_393(o88, i68, i67, env, static) -{1,1}> createIntList_Return_397(o88, i68, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Return_397(o88, i68, i67, env, static) -{1,1}> main_Store_402(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
main_Store_402(i68, o88, i67, env, static) -{1,1}> main_Load_405(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
main_Load_405(i68, o88, i67, env, static) -{0,0}> main_Load_438(i68, o88, i67, env, static) :|: 1 <= i67 && 0 <= i67 && 0 < o88 && 1 <= i68

obtained
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
by chaining
main_Load_438(i68, o135, i97, env, static) -{1,1}> main_FieldAccess_462(i68, o135, i97, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_FieldAccess_462(i68, o135, i97, env, static) -{1,1}> main_LE_465(i68, i97, o135, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68

obtained
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i107', env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
by chaining
main_LE_465(i68, i105, o135, env, static) -{0,0}> main_LE_468(i68, i105, o135, env, static) :|: 0 < o135 && 0 <= i105 && 1 <= i68 && 1 <= i105
main_LE_468(i68, i105, o135, env, static) -{1,1}> main_Load_472(i68, o135, i105, env, static) :|: 0 < o135 && 0 < i105 && 1 <= i68 && 1 <= i105
main_Load_472(i68, o135, i105, env, static) -{1,1}> main_Duplicate_476(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_Duplicate_476(i68, o135, i105, env, static) -{1,1}> main_FieldAccess_478(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_FieldAccess_478(i68, o135, i105, env, static) -{1,1}> main_ConstantStackPush_480(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_ConstantStackPush_480(i68, o135, i105, env, static) -{1,1}> main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) :|: 0 < o135 && iconst_1 = 1 && 1 <= i68 && 1 <= i105
main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) -{1,1}> main_FieldAccess_484(i68, o135, i107, i105, env, static) :|: 0 < o135 && i105 - iconst_1 = i107 && iconst_1 = 1 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_FieldAccess_484(i68, o135, i107, i105, env, static) -{1,1}> main_JMP_487(i68, o135', i107, env, static) :|: 0 < o135 && o135' <= o135 + i107 && 0 < o135' && o135' < o135 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_JMP_487(i68, o135, i107, env, static) -{1,1}> main_Load_492(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107
main_Load_492(i68, o135, i107, env, static) -{0,0}> main_Load_438(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1 && 0 >= 0
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
createIntList_LE_62(i10, 0, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10
langle_init_rangle_Load_355(o88, i67, o89, i68, 0, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
createIntList_LE_388(0, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, iconst_0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i107', env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'

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

Moved arithmethic from lhss to constraints.

createIntList_LE_388(0, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
was transformed to
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0

langle_init_rangle_Load_355(o88, i67, o89, i68, 0, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
was transformed to
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0

createIntList_LE_62(i10, 0, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10
was transformed to
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10 && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, NULL, env, static) :|: NULL = 0 && i9 <= 0
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i107', env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, iconst_0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10 && x = 0
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1 && 0 >= 0

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

Moved arithmethic from constraints to rhss.

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

langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
was transformed to
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0

main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i107', env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
was transformed to
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'

main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, iconst_0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
was transformed to
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, 0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, 0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1 && 0 >= 0
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10 && x = 0

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

Simplified expressions.

createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0
was transformed to
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= i67 && x = 0

createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
was transformed to
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83

main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
was transformed to
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 < i105 && o135''' <= o135 + i107'

langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
was transformed to
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 - 1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 - 1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0

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

createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10 && x = 0
was transformed to
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

(14) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= i67 && x = 0
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 - 1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 - 1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, 0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 < i105 && o135''' <= o135 + i107'
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static'''
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i105 && 0 < i105 && o135''' <= o135 + i107'
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, 0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 < 2 && 0 <= static && 0 <= 1 && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 < 1 && 0 >= 0
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 0 <= 0 && 0 < 1 && 1 <= i10 && x = 0

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

Simplified expressions.

(24) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_438(i68, o135, i97, env, static) -{2,2}> main_LE_465(i68, i97, o135, env, static) :|: 1 <= i68 && 0 < o135 && 0 <= i97
createIntList_LE_388(x, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= i67 && x = 0
langle_init_rangle_Load_355(o88, i67, o89, i68, x, env, static) -{10,10}> createIntList_LE_388(i67 - 1, o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 - 1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67 && x = 0
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83
main_LE_465(i68, iconst_0, o135, env, static) -{0,0}> main_LE_467(i68, 0, o135, env, static) :|: 0 < o135 && 0 <= iconst_0 && iconst_0 = 0 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{8,8}> main_Load_438(i68, o135''', i105 - 1, env, static) :|: i105 - 1 = i107' && 0 <= i107' && 1 <= i105 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 < i105 && o135''' <= o135 + i107'
createIntList_LE_62(i9, NULL, env, static) -{0,0}> createIntList_LE_63(i9, 0, env, static) :|: NULL = 0 && i9 <= 0
main_Load_1(i2, env, static) -{20,20}> createIntList_LE_62(i2, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static'''
createIntList_LE_62(i10, x, env, static) -{9,9}> langle_init_rangle_Load_355(1, i10, 0, i10, 0, env, static) :|: 0 < i10 && 1 <= i10 && x = 0

(25) CESProof (EQUIVALENT transformation)

proved upper bound max(55, 36 + 19 * #0) using cofloco

(26) BOUNDS(CONSTANT, max(55, 36 + 19 * #0))

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

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

(28) Obligation:

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

Used field analysis yielded the following read fields:
- IntList: [value]

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 79 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_12(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_12(i2, env, static) -{0,0}> langle_clinit_rangle_New_13(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_13(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o1, i2, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_17(o1, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_23(o1, i2, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_23(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Load_28(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_30(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_33(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_35(o1, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 >= 0
main_Load_47(i2, env, static) -{1,1}> main_InvokeMethod_49(i2, env, static) :|: 0 >= 0
main_InvokeMethod_49(i2, env, static) -{0,0}> main_InvokeMethod_50(i2, env, static) :|: 0 >= 0
main_InvokeMethod_50(i2, env, static) -{1,1}> createIntList_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_52(i2, env, static) -{1,1}> createIntList_Store_56(NULL, i2, env, static) :|: NULL = 0
createIntList_Store_56(NULL, i2, env, static) -{1,1}> createIntList_Load_58(i2, NULL, env, static) :|: NULL = 0
createIntList_Load_58(i2, NULL, env, static) -{1,1}> createIntList_LE_62(i2, NULL, env, static) :|: NULL = 0
createIntList_LE_62(i10, NULL, env, static) -{0,0}> createIntList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createIntList_LE_64(i10, NULL, env, static) -{1,1}> createIntList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createIntList_New_68(i10, NULL, env, static) -{1,1}> createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_355(o4, i10, NULL, i10, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0 && 0 <= NULL
langle_init_rangle_Load_355(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_FieldAccess_360(o88, i67, o89, i68, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_363(o88', o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && o88' <= o88 + i67 && 0 < o88' && 0 < o88 && iconst_0 = 0 && o88 < o88' && 1 <= i68
langle_init_rangle_Load_363(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Load_365(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_FieldAccess_367(o88, o89, i67, i68, env, static) -{1,1}> langle_init_rangle_Return_371(o88, i67, i68, env, static) :|: 0 <= o89 && 1 <= i67 && 0 < o88 && 1 <= i68
langle_init_rangle_Return_371(o88, i67, i68, env, static) -{1,1}> createIntList_Store_373(o88, i67, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Store_373(o88, i67, i68, env, static) -{1,1}> createIntList_Inc_375(i67, o88, i68, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Inc_375(i67, o88, i68, env, static) -{1,1}> createIntList_JMP_378(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && i67 + -1 = i76 && 0 < o88 && 1 <= i68
createIntList_JMP_378(i76, o88, i68, i67, env, static) -{1,1}> createIntList_Load_380(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68
createIntList_Load_380(i76, o88, i68, i67, env, static) -{1,1}> createIntList_LE_388(i76, o88, i68, i67, env, static) :|: 1 <= i67 && 0 <= i76 && 0 < o88 && 1 <= i68
createIntList_LE_388(iconst_0, o88, i68, i67, env, static) -{0,0}> createIntList_LE_390(iconst_0, o88, i68, i67, env, static) :|: 0 <= iconst_0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_LE_388(i83, o88, i68, i84, env, static) -{0,0}> createIntList_LE_391(i83, o88, i68, i84, env, static) :|: 1 <= i84 && 2 <= i84 && 1 <= i83 && 0 < o88 && 1 <= i68 && 0 <= i83
createIntList_LE_390(iconst_0, o88, i68, i67, env, static) -{1,1}> createIntList_Load_393(o88, i68, i67, env, static) :|: iconst_0 <= 0 && 1 <= i67 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_LE_391(i83, o88, i68, i84, env, static) -{1,1}> createIntList_New_395(i83, o88, i68, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83 && 1 <= i68
createIntList_Load_393(o88, i68, i67, env, static) -{1,1}> createIntList_Return_397(o88, i68, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_New_395(i83, o88, i68, i84, env, static) -{1,1}> createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) :|: o109 = 1 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < o109 && iconst_0 = 0 && 1 <= i68
createIntList_Return_397(o88, i68, i67, env, static) -{1,1}> main_Store_402(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Duplicate_399(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Store_402(i68, o88, i67, env, static) -{1,1}> main_Load_405(i68, o88, i67, env, static) :|: 1 <= i67 && 0 < o88 && 1 <= i68
createIntList_Load_404(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Load_405(i68, o88, i67, env, static) -{0,0}> main_Load_438(i68, o88, i67, env, static) :|: 1 <= i67 && 0 <= i67 && 0 < o88 && 1 <= i68
createIntList_Load_406(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
createIntList_InvokeMethod_408(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_410(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_InvokeMethod_415(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_419(o109, i83, o88, i68, iconst_0, i84, env, static) -{1,1}> langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) :|: 2 <= i84 && 1 <= i83 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
langle_init_rangle_Load_422(o109, i83, o88, i68, iconst_0, i84, env, static) -{0,0}> langle_init_rangle_Load_355(o109, i83, o88, i68, iconst_0, env, static) :|: 2 <= i84 && 1 <= i83 && 0 <= o88 && 0 < o109 && 0 < o88 && iconst_0 = 0 && 1 <= i68
main_Load_438(i68, o135, i97, env, static) -{1,1}> main_FieldAccess_462(i68, o135, i97, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_FieldAccess_462(i68, o135, i97, env, static) -{1,1}> main_LE_465(i68, i97, o135, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{0,0}> main_LE_468(i68, i105, o135, env, static) :|: 0 < o135 && 0 <= i105 && 1 <= i68 && 1 <= i105
main_LE_468(i68, i105, o135, env, static) -{1,1}> main_Load_472(i68, o135, i105, env, static) :|: 0 < o135 && 0 < i105 && 1 <= i68 && 1 <= i105
main_Load_472(i68, o135, i105, env, static) -{1,1}> main_Duplicate_476(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_Duplicate_476(i68, o135, i105, env, static) -{1,1}> main_FieldAccess_478(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_FieldAccess_478(i68, o135, i105, env, static) -{1,1}> main_ConstantStackPush_480(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_ConstantStackPush_480(i68, o135, i105, env, static) -{1,1}> main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) :|: 0 < o135 && iconst_1 = 1 && 1 <= i68 && 1 <= i105
main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) -{1,1}> main_FieldAccess_484(i68, o135, i107, i105, env, static) :|: 0 < o135 && i105 - iconst_1 = i107 && iconst_1 = 1 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_FieldAccess_484(i68, o135, i107, i105, env, static) -{1,1}> main_JMP_487(i68, o135', i107, env, static) :|: 0 < o135 && o135' <= o135 + i107 && 0 < o135' && o135' < o135 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_JMP_487(i68, o135, i107, env, static) -{1,1}> main_Load_492(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107
main_Load_492(i68, o135, i107, env, static) -{0,0}> main_Load_438(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107

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

obtained
main_Load_1(i2, env, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2, 0, env, static'1) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
by chaining
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_10(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_12(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_12(i2, env, static) -{0,0}> langle_clinit_rangle_New_13(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_13(i2, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_15(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o1, i2, env, static) :|: o1 = 1 && 0 < o1
langle_clinit_rangle_Duplicate_17(o1, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_19(o1, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) :|: NULL = 0 && 0 < o1
langle_clinit_rangle_InvokeMethod_21(o1, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_23(o1, i2, env, static) :|: NULL = 0 && 0 < o1
langle_init_rangle_Load_23(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_26(o1, i2, env, static) -{1,1}> langle_init_rangle_Load_28(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Load_28(o1, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_InvokeMethod_30(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_33(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_33(o1, i2, env, static) -{1,1}> langle_init_rangle_Return_35(o1, i2, env, static) :|: 0 < o1
langle_init_rangle_Return_35(o1, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) :|: 0 < o1
langle_clinit_rangle_FieldAccess_38(o1, i2, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, env, static') :|: static' <= static + o1 && 0 <= o1 && 0 <= static && 0 < o1
langle_clinit_rangle_Return_40(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_43(i2, env, static) :|: 0 <= static
main_Load_43(i2, env, static) -{0,0}> main_Load_45(i2, env, static) :|: 0 >= 0
main_Load_45(i2, env, static) -{0,0}> main_Load_47(i2, env, static) :|: 0 >= 0
main_Load_47(i2, env, static) -{1,1}> main_InvokeMethod_49(i2, env, static) :|: 0 >= 0
main_InvokeMethod_49(i2, env, static) -{0,0}> main_InvokeMethod_50(i2, env, static) :|: 0 >= 0
main_InvokeMethod_50(i2, env, static) -{1,1}> createIntList_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
createIntList_ConstantStackPush_52(i2, env, static) -{1,1}> createIntList_Store_56(NULL, i2, env, static) :|: NULL = 0
createIntList_Store_56(NULL, i2, env, static) -{1,1}> createIntList_Load_58(i2, NULL, env, static) :|: NULL = 0
createIntList_Load_58(i2, NULL, env, static) -{1,1}> createIntList_LE_62(i2, NULL, env, static) :|: NULL = 0
createIntList_LE_62(i10, NULL, env, static) -{0,0}> createIntList_LE_64(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10
createIntList_LE_64(i10, NULL, env, static) -{1,1}> createIntList_New_68(i10, NULL, env, static) :|: NULL = 0 && 1 <= i10 && 0 < i10
createIntList_New_68(i10, NULL, env, static) -{1,1}> createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Duplicate_72(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_76(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_Load_81(o4, i10, NULL, iconst_0, env, static) -{1,1}> createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
createIntList_InvokeMethod_86(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_89(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_93(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_98(o4, i10, NULL, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_102(o4, i10, NULL, iconst_0, env, static) -{0,0}> langle_init_rangle_Load_355(o4, i10, NULL, i10, iconst_0, env, static) :|: NULL = 0 && 1 <= i10 && 0 < o4 && iconst_0 = 0 && 0 <= NULL

obtained
main_Load_438(i68, o135, i97, env, static) -{10,10}> main_Load_438(i68, o135''', i107', env, static) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'
by chaining
main_Load_438(i68, o135, i97, env, static) -{1,1}> main_FieldAccess_462(i68, o135, i97, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_FieldAccess_462(i68, o135, i97, env, static) -{1,1}> main_LE_465(i68, i97, o135, env, static) :|: 0 < o135 && 0 <= i97 && 1 <= i68
main_LE_465(i68, i105, o135, env, static) -{0,0}> main_LE_468(i68, i105, o135, env, static) :|: 0 < o135 && 0 <= i105 && 1 <= i68 && 1 <= i105
main_LE_468(i68, i105, o135, env, static) -{1,1}> main_Load_472(i68, o135, i105, env, static) :|: 0 < o135 && 0 < i105 && 1 <= i68 && 1 <= i105
main_Load_472(i68, o135, i105, env, static) -{1,1}> main_Duplicate_476(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_Duplicate_476(i68, o135, i105, env, static) -{1,1}> main_FieldAccess_478(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_FieldAccess_478(i68, o135, i105, env, static) -{1,1}> main_ConstantStackPush_480(i68, o135, i105, env, static) :|: 0 < o135 && 1 <= i68 && 1 <= i105
main_ConstantStackPush_480(i68, o135, i105, env, static) -{1,1}> main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) :|: 0 < o135 && iconst_1 = 1 && 1 <= i68 && 1 <= i105
main_IntArithmetic_482(i68, o135, i105, iconst_1, env, static) -{1,1}> main_FieldAccess_484(i68, o135, i107, i105, env, static) :|: 0 < o135 && i105 - iconst_1 = i107 && iconst_1 = 1 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_FieldAccess_484(i68, o135, i107, i105, env, static) -{1,1}> main_JMP_487(i68, o135', i107, env, static) :|: 0 < o135 && o135' <= o135 + i107 && 0 < o135' && o135' < o135 && 1 <= i68 && 1 <= i105 && 0 <= i107
main_JMP_487(i68, o135, i107, env, static) -{1,1}> main_Load_492(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107
main_Load_492(i68, o135, i107, env, static) -{0,0}> main_Load_438(i68, o135, i107, env, static) :|: 0 < o135 && 1 <= i68 && 0 <= i107

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, env, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2, 0, env, static'1) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
langle_init_rangle_Load_355(o88, i67, o89, i68, 0, env, static) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67, env, static) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
createIntList_LE_388(i83, o88, i68, i84, env, static) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68, 0, env, static) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
createIntList_LE_388(0, o88, i68, i67, env, static) -{4,4}> main_Load_438(i68, o88, i67, env, static) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
main_Load_438(i68, o135, i97, env, static) -{10,10}> main_Load_438(i68, o135''', i107', env, static) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'

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

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

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
langle_init_rangle_Load_355(x1, x2, x3, x4, x5, x6, x7) → langle_init_rangle_Load_355(x1, x2, x3, x4)
createIntList_LE_388(x1, x2, x3, x4, x5, x6) → createIntList_LE_388(x1, x2, x3, x4)
main_Load_438(x1, x2, x3, x4, x5) → main_Load_438(x1, x2, x3)

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
createIntList_LE_388(0, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i107') :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'

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

Moved arithmethic from lhss to constraints.

createIntList_LE_388(0, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67
was transformed to
createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i107') :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'
main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0

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

Moved arithmethic from constraints to rhss.

langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i76', o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
was transformed to
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67

main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i107') :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'
was transformed to
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i97 - 1) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i97 - 1) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'
main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0

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

Simplified expressions.

createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < 1 && 0 <= o88 && 0 < i83 && 0 <= i83
was transformed to
createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83

main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i97 - 1) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 <= i97 && 0 < i97 && o135''' <= o135 + i107'
was transformed to
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i97 - 1) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 < i97 && o135''' <= o135 + i107'

langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i67 + -1, o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 + -1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
was transformed to
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i67 - 1, o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 - 1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67

main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= 2 && 0 <= 0 && 0 >= 0 && 0 <= static''' && 0 < 1 && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 < i2
was transformed to
main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= static''' && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= static && 0 <= static'1 && 0 < i2

createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= 0 && 0 <= i67 && x = 0
was transformed to
createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= i67 && x = 0

(40) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_438(i68, o135, i97) -{10,10}> main_Load_438(i68, o135''', i97 - 1) :|: i97 - 1 = i107' && 0 <= i107' && 1 <= i97 && 0 < o135''' && 1 <= i68 && 0 < o135 && o135''' < o135 && 0 < i97 && o135''' <= o135 + i107'
langle_init_rangle_Load_355(o88, i67, o89, i68) -{10,10}> createIntList_LE_388(i67 - 1, o88''', i68, i67) :|: o88 < o88''' && 1 <= i68 && 0 < o88 && 0 < o88''' && i67 - 1 = i76' && 1 <= i67 && 0 <= i76' && 0 <= o89 && o88''' <= o88 + i67
createIntList_LE_388(i83, o88, i68, i84) -{9,9}> langle_init_rangle_Load_355(1, i83, o88, i68) :|: 1 <= i84 && 1 <= i68 && 2 <= i84 && 1 <= i83 && 0 < o88 && 0 < i83
createIntList_LE_388(x, o88, i68, i67) -{4,4}> main_Load_438(i68, o88, i67) :|: 0 < o88 && 1 <= i68 && 1 <= i67 && 0 <= i67 && x = 0
main_Load_1(i2, static) -{29,29}> langle_init_rangle_Load_355(1, i2, 0, i2) :|: 0 <= static''' && static''' <= static + 2 && 1 <= i2 && static'1 <= static''' + 1 && 0 <= static && 0 <= static'1 && 0 < i2