time complexity proof of /tmp/tmpBBROMc/PastaC1.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(4 + nat(8 * #0) * nat(-2 + #0) + nat(-8 + 8 * #0) + max(25 + 9 * #0, 25), 29)).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

        ↳13 CESProof (⇔, 218 ms)

        ↳14 BOUNDS(CONSTANT, max(25, nat(8 * #0) * nat(-2 + #0) + nat(-8 + 8 * #0) + max(25 + 9 * #0, 25)))

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

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)), 0 ms)

↳24 JBCComplexityEdges

    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 54 ms)

    ↳26 WeightedIntTrs

    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 16 ms)

    ↳28 WeightedIntTrs

    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 16 ms)

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaC1 {
    public static void main(int x) {
		while (x >= 0) {
			int y = 1;
			while (x > y) {
				y = 2*y;
			}
			x--;
		}
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 52 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_49(i1, env, static) :|: 0 <= static
main_Load_49(i1, env, static) -{0,0}> main_Load_50(i1, env, static) :|: 0 >= 0
main_Load_50(i1, env, static) -{0,0}> main_Load_51(i1, env, static) :|: 0 >= 0
main_Load_51(i1, env, static) -{1,1}> main_LT_52(i1, env, static) :|: 0 >= 0
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 0 <= i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
main_ConstantStackPush_321(i39, i110, env, static) -{1,1}> main_Store_322(i39, iconst_1, i110, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Store_322(i39, iconst_1, i110, env, static) -{1,1}> main_Load_324(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Load_324(i39, i110, iconst_1, env, static) -{0,0}> main_Load_420(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 <= 4 && 1 <= iconst_1 && iconst_1 = 1 && 0 <= i110
main_Load_420(i39, i146, i147, env, static) -{0,0}> main_Load_468(i39, i146, i147, env, static) :|: 0 <= i39 && i147 <= 8 && 1 <= i147 && i147 <= 4
main_Load_468(i39, i169, i170, env, static) -{0,0}> main_Load_516(i39, i169, i170, env, static) :|: 0 <= i39 && i170 <= 8 && 1 <= i170
main_Load_516(i39, i188, i189, env, static) -{1,1}> main_Load_517(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_Load_517(i39, i188, i189, env, static) -{1,1}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_533(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_534(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i189 < i188
main_LE_533(i39, i188, i189, env, static) -{1,1}> main_Inc_535(i39, i188, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_534(i39, i188, i189, env, static) -{1,1}> main_ConstantStackPush_536(i39, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && i189 < i188
main_Inc_535(i39, i188, env, static) -{1,1}> main_JMP_538(i39, i196, env, static) :|: 0 <= i39 && i188 + -1 = i196
main_ConstantStackPush_536(i39, i188, i189, env, static) -{1,1}> main_Load_540(i39, iconst_2, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_JMP_538(i39, i196, env, static) -{1,1}> main_Load_543(i39, i196, env, static) :|: 0 <= i39
main_Load_540(i39, iconst_2, i188, i189, env, static) -{1,1}> main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_Load_543(i39, i196, env, static) -{1,1}> main_LT_551(i39, i196, env, static) :|: 0 <= i39
main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) -{1,1}> main_Store_554(i39, i206, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206 && 1 <= i189 && iconst_2 * i189 = i206 && iconst_2 = 2
main_LT_551(i39, i207, env, static) -{0,0}> main_LT_556(i39, i207, env, static) :|: 0 <= i39 && i207 <= -1
main_LT_551(i39, i208, env, static) -{0,0}> main_LT_558(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_Store_554(i39, i206, i188, env, static) -{1,1}> main_JMP_559(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_LT_558(i39, i208, env, static) -{1,1}> main_ConstantStackPush_567(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_JMP_559(i39, i188, i206, env, static) -{1,1}> main_Load_571(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_ConstantStackPush_567(i39, i208, env, static) -{0,0}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_Load_571(i39, i188, i206, env, static) -{0,0}> main_Load_516(i39, i188, i206, env, static) :|: 0 <= i39 && 1 <= i206 && 2 <= i188 && 2 <= i206

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

obtained
main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_49(i1, env, static) :|: 0 <= static
main_Load_49(i1, env, static) -{0,0}> main_Load_50(i1, env, static) :|: 0 >= 0
main_Load_50(i1, env, static) -{0,0}> main_Load_51(i1, env, static) :|: 0 >= 0
main_Load_51(i1, env, static) -{1,1}> main_LT_52(i1, env, static) :|: 0 >= 0

obtained
main_LT_52(i10, env, static) -{1,1}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
by chaining
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 0 <= i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10

obtained
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
by chaining
main_ConstantStackPush_321(i39, i110, env, static) -{1,1}> main_Store_322(i39, iconst_1, i110, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Store_322(i39, iconst_1, i110, env, static) -{1,1}> main_Load_324(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Load_324(i39, i110, iconst_1, env, static) -{0,0}> main_Load_420(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 <= 4 && 1 <= iconst_1 && iconst_1 = 1 && 0 <= i110
main_Load_420(i39, i146, i147, env, static) -{0,0}> main_Load_468(i39, i146, i147, env, static) :|: 0 <= i39 && i147 <= 8 && 1 <= i147 && i147 <= 4
main_Load_468(i39, i169, i170, env, static) -{0,0}> main_Load_516(i39, i169, i170, env, static) :|: 0 <= i39 && i170 <= 8 && 1 <= i170

obtained
main_Load_516(i39, i188, i189, env, static) -{2,2}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
by chaining
main_Load_516(i39, i188, i189, env, static) -{1,1}> main_Load_517(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_Load_517(i39, i188, i189, env, static) -{1,1}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189

obtained
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, i206', env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
by chaining
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_534(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i189 < i188
main_LE_534(i39, i188, i189, env, static) -{1,1}> main_ConstantStackPush_536(i39, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && i189 < i188
main_ConstantStackPush_536(i39, i188, i189, env, static) -{1,1}> main_Load_540(i39, iconst_2, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_Load_540(i39, iconst_2, i188, i189, env, static) -{1,1}> main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) -{1,1}> main_Store_554(i39, i206, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206 && 1 <= i189 && iconst_2 * i189 = i206 && iconst_2 = 2
main_Store_554(i39, i206, i188, env, static) -{1,1}> main_JMP_559(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_JMP_559(i39, i188, i206, env, static) -{1,1}> main_Load_571(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_Load_571(i39, i188, i206, env, static) -{0,0}> main_Load_516(i39, i188, i206, env, static) :|: 0 <= i39 && 1 <= i206 && 2 <= i188 && 2 <= i206

obtained
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i196', env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189
by chaining
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_533(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_533(i39, i188, i189, env, static) -{1,1}> main_Inc_535(i39, i188, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_Inc_535(i39, i188, env, static) -{1,1}> main_JMP_538(i39, i196, env, static) :|: 0 <= i39 && i188 + -1 = i196
main_JMP_538(i39, i196, env, static) -{1,1}> main_Load_543(i39, i196, env, static) :|: 0 <= i39
main_Load_543(i39, i196, env, static) -{1,1}> main_LT_551(i39, i196, env, static) :|: 0 <= i39

obtained
main_LT_551(i39, i208, env, static) -{1,1}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
by chaining
main_LT_551(i39, i208, env, static) -{0,0}> main_LT_558(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_LT_558(i39, i208, env, static) -{1,1}> main_ConstantStackPush_567(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_ConstantStackPush_567(i39, i208, env, static) -{0,0}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_52(i10, env, static) -{1,1}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
main_Load_516(i39, i188, i189, env, static) -{2,2}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, i206', env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i196', env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189
main_LT_551(i39, i207, env, static) -{0,0}> main_LT_556(i39, i207, env, static) :|: 0 <= i39 && i207 <= -1
main_LT_551(i39, i208, env, static) -{1,1}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208

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

Moved arithmethic from constraints to rhss.

main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i196', env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189
was transformed to
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i188 + -1, env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189

main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, i206', env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
was transformed to
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, 2 * i189, env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i188 + -1, env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, 2 * i189, env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
main_LT_551(i39, i207, env, static) -{0,0}> main_LT_556(i39, i207, env, static) :|: 0 <= i39 && i207 <= -1
main_Load_516(i39, i188, i189, env, static) -{2,2}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LT_52(i10, env, static) -{1,1}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_551(i39, i208, env, static) -{1,1}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4

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

Simplified expressions.

main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i188 + -1, env, static) :|: 0 <= i39 && 1 <= i189 && i188 + -1 = i196' && i188 <= i189
was transformed to
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i188 - 1, env, static) :|: 0 <= i39 && 1 <= i189 && i188 - 1 = i196' && i188 <= i189

main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
was transformed to
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 0 <= i39 && 0 <= i110

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 0 <= i39 && 0 <= i110
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, 2 * i189, env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_Load_2(i1, env, static) -{16,16}> main_LT_52(i1, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LT_52(i10, env, static) -{1,1}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
main_Load_516(i39, i188, i189, env, static) -{2,2}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LT_551(i39, i207, env, static) -{0,0}> main_LT_556(i39, i207, env, static) :|: 0 <= i39 && i207 <= -1
main_LT_52(i9, env, static) -{0,0}> main_LT_53(i9, env, static) :|: i9 <= -1
main_LT_551(i39, i208, env, static) -{1,1}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_LE_526(i39, i188, i189, env, static) -{4,4}> main_LT_551(i39, i188 - 1, env, static) :|: 0 <= i39 && 1 <= i189 && i188 - 1 = i196' && i188 <= i189

(13) CESProof (EQUIVALENT transformation)

proved upper bound max(25, nat(8 * #0) * nat(-2 + #0) + nat(-8 + 8 * #0) + max(25 + 9 * #0, 25)) using cofloco

(14) BOUNDS(CONSTANT, max(25, nat(8 * #0) * nat(-2 + #0) + nat(-8 + 8 * #0) + max(25 + 9 * #0, 25)))

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from constraints to rhss.

(20) Obligation:

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

Simplified expressions.

(22) Obligation:

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(4)) transformation)

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

(24) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(26) Obligation:

IntTrs with 50 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_49(i1, env, static) :|: 0 <= static
main_Load_49(i1, env, static) -{0,0}> main_Load_50(i1, env, static) :|: 0 >= 0
main_Load_50(i1, env, static) -{0,0}> main_Load_51(i1, env, static) :|: 0 >= 0
main_Load_51(i1, env, static) -{1,1}> main_LT_52(i1, env, static) :|: 0 >= 0
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 0 <= i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10
main_ConstantStackPush_321(i39, i110, env, static) -{1,1}> main_Store_322(i39, iconst_1, i110, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Store_322(i39, iconst_1, i110, env, static) -{1,1}> main_Load_324(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 = 1 && 0 <= i110
main_Load_324(i39, i110, iconst_1, env, static) -{0,0}> main_Load_420(i39, i110, iconst_1, env, static) :|: 0 <= i39 && iconst_1 <= 4 && 1 <= iconst_1 && iconst_1 = 1 && 0 <= i110
main_Load_420(i39, i146, i147, env, static) -{0,0}> main_Load_468(i39, i146, i147, env, static) :|: 0 <= i39 && i147 <= 8 && 1 <= i147 && i147 <= 4
main_Load_468(i39, i169, i170, env, static) -{0,0}> main_Load_516(i39, i169, i170, env, static) :|: 0 <= i39 && i170 <= 8 && 1 <= i170
main_Load_516(i39, i188, i189, env, static) -{1,1}> main_Load_517(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_Load_517(i39, i188, i189, env, static) -{1,1}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_533(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_534(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i189 < i188
main_LE_533(i39, i188, i189, env, static) -{1,1}> main_Inc_535(i39, i188, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_534(i39, i188, i189, env, static) -{1,1}> main_ConstantStackPush_536(i39, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && i189 < i188
main_Inc_535(i39, i188, env, static) -{1,1}> main_JMP_538(i39, i196, env, static) :|: 0 <= i39 && i188 + -1 = i196
main_ConstantStackPush_536(i39, i188, i189, env, static) -{1,1}> main_Load_540(i39, iconst_2, i188, i189, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_JMP_538(i39, i196, env, static) -{1,1}> main_Load_543(i39, i196, env, static) :|: 0 <= i39
main_Load_540(i39, iconst_2, i188, i189, env, static) -{1,1}> main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 1 <= i189 && iconst_2 = 2
main_Load_543(i39, i196, env, static) -{1,1}> main_LT_551(i39, i196, env, static) :|: 0 <= i39
main_IntArithmetic_545(i39, iconst_2, i189, i188, env, static) -{1,1}> main_Store_554(i39, i206, i188, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206 && 1 <= i189 && iconst_2 * i189 = i206 && iconst_2 = 2
main_LT_551(i39, i208, env, static) -{0,0}> main_LT_558(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_Store_554(i39, i206, i188, env, static) -{1,1}> main_JMP_559(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_LT_558(i39, i208, env, static) -{1,1}> main_ConstantStackPush_567(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_JMP_559(i39, i188, i206, env, static) -{1,1}> main_Load_571(i39, i188, i206, env, static) :|: 0 <= i39 && 2 <= i188 && 2 <= i206
main_ConstantStackPush_567(i39, i208, env, static) -{0,0}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_Load_571(i39, i188, i206, env, static) -{0,0}> main_Load_516(i39, i188, i206, env, static) :|: 0 <= i39 && 1 <= i206 && 2 <= i188 && 2 <= i206

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

obtained
main_Load_2(i1, env, static) -{17,17}> main_ConstantStackPush_321(i1, i1, env, static'1) :|: 0 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, env, static) -{0,0}> main_Load_4(i1, env, static) :|: 0 >= 0
main_Load_4(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_14(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_23(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> main_Load_45(i1, env, static) :|: 0 >= 0
main_Load_45(i1, env, static) -{0,0}> main_Load_46(i1, env, static) :|: 0 >= 0
main_Load_46(i1, env, static) -{0,0}> main_Load_49(i1, env, static) :|: 0 <= static
main_Load_49(i1, env, static) -{0,0}> main_Load_50(i1, env, static) :|: 0 >= 0
main_Load_50(i1, env, static) -{0,0}> main_Load_51(i1, env, static) :|: 0 >= 0
main_Load_51(i1, env, static) -{1,1}> main_LT_52(i1, env, static) :|: 0 >= 0
main_LT_52(i10, env, static) -{0,0}> main_LT_54(i10, env, static) :|: 0 <= i10
main_LT_54(i10, env, static) -{1,1}> main_ConstantStackPush_58(i10, env, static) :|: 0 <= i10
main_ConstantStackPush_58(i10, env, static) -{0,0}> main_ConstantStackPush_321(i10, i10, env, static) :|: 0 <= i10

obtained
main_LE_526(i39, i188, i189, env, static) -{5,5}> main_ConstantStackPush_321(i39, i196', env, static) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189
by chaining
main_LE_526(i39, i188, i189, env, static) -{0,0}> main_LE_533(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_LE_533(i39, i188, i189, env, static) -{1,1}> main_Inc_535(i39, i188, env, static) :|: 0 <= i39 && 1 <= i189 && i188 <= i189
main_Inc_535(i39, i188, env, static) -{1,1}> main_JMP_538(i39, i196, env, static) :|: 0 <= i39 && i188 + -1 = i196
main_JMP_538(i39, i196, env, static) -{1,1}> main_Load_543(i39, i196, env, static) :|: 0 <= i39
main_Load_543(i39, i196, env, static) -{1,1}> main_LT_551(i39, i196, env, static) :|: 0 <= i39
main_LT_551(i39, i208, env, static) -{0,0}> main_LT_558(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_LT_558(i39, i208, env, static) -{1,1}> main_ConstantStackPush_567(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208
main_ConstantStackPush_567(i39, i208, env, static) -{0,0}> main_ConstantStackPush_321(i39, i208, env, static) :|: 0 <= i39 && 0 <= i208

(28) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, env, static) -{17,17}> main_ConstantStackPush_321(i1, i1, env, static'1) :|: 0 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_ConstantStackPush_321(i39, i110, env, static) -{2,2}> main_Load_516(i39, i110, 1, env, static) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
main_Load_516(i39, i188, i189, env, static) -{2,2}> main_LE_526(i39, i188, i189, env, static) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{6,6}> main_Load_516(i39, i188, i206', env, static) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_LE_526(i39, i188, i189, env, static) -{5,5}> main_ConstantStackPush_321(i39, i196', env, static) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189

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

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

main_Load_2(x1, x2, x3) → main_Load_2(x1, x3)
main_ConstantStackPush_321(x1, x2, x3, x4) → main_ConstantStackPush_321(x1, x2)
main_Load_516(x1, x2, x3, x4, x5) → main_Load_516(x1, x2, x3)
main_LE_526(x1, x2, x3, x4, x5) → main_LE_526(x1, x2, x3)

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, static) -{17,17}> main_ConstantStackPush_321(i1, i1) :|: 0 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_ConstantStackPush_321(i39, i110) -{2,2}> main_Load_516(i39, i110, 1) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
main_Load_516(i39, i188, i189) -{2,2}> main_LE_526(i39, i188, i189) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189) -{6,6}> main_Load_516(i39, i188, i206') :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i196') :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189

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

Moved arithmethic from constraints to rhss.

main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i196') :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189
was transformed to
main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i188 + -1) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189

main_LE_526(i39, i188, i189) -{6,6}> main_Load_516(i39, i188, i206') :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
was transformed to
main_LE_526(i39, i188, i189) -{6,6}> main_Load_516(i39, i188, 2 * i189) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_516(i39, i188, i189) -{2,2}> main_LE_526(i39, i188, i189) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i188 + -1) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189
main_LE_526(i39, i188, i189) -{6,6}> main_Load_516(i39, i188, 2 * i189) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189
main_ConstantStackPush_321(i39, i110) -{2,2}> main_Load_516(i39, i110, 1) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
main_Load_2(i1, static) -{17,17}> main_ConstantStackPush_321(i1, i1) :|: 0 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1

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

Simplified expressions.

main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i188 + -1) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 + -1 = i196' && 1 <= i189
was transformed to
main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i188 - 1) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 - 1 = i196' && 1 <= i189

main_ConstantStackPush_321(i39, i110) -{2,2}> main_Load_516(i39, i110, 1) :|: 1 <= 8 && 1 <= 1 && 0 <= i39 && 0 <= i110 && 1 <= 4
was transformed to
main_ConstantStackPush_321(i39, i110) -{2,2}> main_Load_516(i39, i110, 1) :|: 0 <= i39 && 0 <= i110

main_Load_2(i1, static) -{17,17}> main_ConstantStackPush_321(i1, i1) :|: 0 <= i1 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, static) -{17,17}> main_ConstantStackPush_321(i1, i1) :|: 0 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, static)
Considered paths: all paths from start
Rules:
main_Load_516(i39, i188, i189) -{2,2}> main_LE_526(i39, i188, i189) :|: 0 <= i39 && 1 <= i189
main_LE_526(i39, i188, i189) -{5,5}> main_ConstantStackPush_321(i39, i188 - 1) :|: i188 <= i189 && 0 <= i39 && 0 <= i196' && i188 - 1 = i196' && 1 <= i189
main_Load_2(i1, static) -{17,17}> main_ConstantStackPush_321(i1, i1) :|: 0 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_ConstantStackPush_321(i39, i110) -{2,2}> main_Load_516(i39, i110, 1) :|: 0 <= i39 && 0 <= i110
main_LE_526(i39, i188, i189) -{6,6}> main_Load_516(i39, i188, 2 * i189) :|: i189 < i188 && 2 <= i206' && 2 <= i188 && 0 <= i39 && 1 <= i206' && 2 * i189 = i206' && 1 <= i189