The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 18 + 6 * |#0| + 10 * |#1|).

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 440 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 0 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 106 ms)
    ↳6 WeightedIntTrs
    ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 30 ms)
    ↳8 WeightedIntTrs
    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 18 ms)
    ↳10 WeightedIntTrs
    ↳11 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳12 WeightedIntTrs
    ↳13 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳14 WeightedIntTrs
    ↳15 koat Proof (⇔, 42 ms)
    ↳16 BOUNDS(CONSTANT, 16 + 6 * |#0| + 10 * |#1|)
↳17 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 13 ms)
↳18 JBCComplexityEdges
    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 91 ms)
    ↳20 WeightedIntTrs
        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 29 ms)
        ↳22 WeightedIntTrs
        ↳23 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳24 WeightedIntTrs
        ↳25 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 8 ms)
        ↳26 WeightedIntTrs
    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 90 ms)
    ↳28 WeightedIntTrs
        ↳29 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 26 ms)
        ↳30 WeightedIntTrs
        ↳31 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳32 WeightedIntTrs
        ↳33 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 13 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 PastaB12 {
    public static void main(int x, int y) {
        while (x > 0 || y > 0) {
            if (x > 0) {
                x--;
            } else if (y > 0) {
                y--;
            } else {
                continue;
            }
        }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
PastaB12.main(II)V: Graph of 48 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 46 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 46 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

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

obtained
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0

obtained
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
by chaining
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344

obtained
main_GT_1003(i298, i134, i333, i300, env, static) -{10,10}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'
by chaining
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

(8) Obligation:

IntTrs with 3 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
main_GT_1003(i298, i134, i333, i300, env, static) -{10,10}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_GT_1003(x1, x2, x3, x4, x5, x6) → main_GT_1003(x3, x4)

(10) Obligation:

IntTrs with 3 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i2, i3, static) -{16,16}> main_GT_1003(i2, i3) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i344', i300) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i348') :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'

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

Moved arithmethic from constraints to rhss.

main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i348') :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'
was transformed to
main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i300 + -1) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'

main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i344', i300) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i334 + -1, i300) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

(12) Obligation:

IntTrs with 3 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i300 + -1) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'
main_Load_2(i2, i3, static) -{16,16}> main_GT_1003(i2, i3) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i334 + -1, i300) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

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

Simplified expressions.

main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i334 + -1, i300) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i334 - 1, i300) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334

main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i300 + -1) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 + -1 = i348'
was transformed to
main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i300 - 1) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 - 1 = i348'

main_Load_2(i2, i3, static) -{16,16}> main_GT_1003(i2, i3) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_2(i2, i3, static) -{16,16}> main_GT_1003(i2, i3) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(14) Obligation:

IntTrs with 3 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_GT_1003(i333, i300) -{10,10}> main_GT_1003(i333, i300 - 1) :|: 0 < i300 && 0 <= i348' && i333 <= 0 && 1 <= i300 && i300 - 1 = i348'
main_Load_2(i2, i3, static) -{16,16}> main_GT_1003(i2, i3) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_1003(i334, i300) -{6,6}> main_GT_1003(i334 - 1, i300) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334

(15) koat Proof (EQUIVALENT transformation)

YES(?, 10*ar_1 + 6*ar_0 + 16)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 10) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1 - 1, arityPad)) [ 0 < ar_1 /\ 0 <= i348' /\ ar_0 <= 0 /\ 1 <= ar_1 /\ ar_1 - 1 = i348' ]
(Comp: ?, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0 - 1, ar_1, arityPad)) [ 0 <= i344' /\ ar_0 - 1 = i344' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 10) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1 - 1, arityPad)) [ 0 < ar_1 /\ 0 <= i348' /\ ar_0 <= 0 /\ 1 <= ar_1 /\ ar_1 - 1 = i348' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0 - 1, ar_1, arityPad)) [ 0 <= i344' /\ ar_0 - 1 = i344' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_GT_1003) = V_2
Pol(main_Load_2) = V_2
Pol(koat_start) = V_2
orients all transitions weakly and the transition
main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1 - 1, arityPad)) [ 0 < ar_1 /\ 0 <= i348' /\ ar_0 <= 0 /\ 1 <= ar_1 /\ ar_1 - 1 = i348' ]
strictly and produces the following problem:
3: T:
(Comp: ar_1, Cost: 10) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1 - 1, arityPad)) [ 0 < ar_1 /\ 0 <= i348' /\ ar_0 <= 0 /\ 1 <= ar_1 /\ ar_1 - 1 = i348' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0 - 1, ar_1, arityPad)) [ 0 <= i344' /\ ar_0 - 1 = i344' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_GT_1003) = V_1
Pol(main_Load_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0 - 1, ar_1, arityPad)) [ 0 <= i344' /\ ar_0 - 1 = i344' /\ 1 <= ar_0 /\ 0 < ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: ar_1, Cost: 10) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1 - 1, arityPad)) [ 0 < ar_1 /\ 0 <= i348' /\ ar_0 <= 0 /\ 1 <= ar_1 /\ ar_1 - 1 = i348' ]
(Comp: 1, Cost: 16) main_Load_2(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0, ar_1, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_0, Cost: 6) main_GT_1003(ar_0, ar_1, ar_2) -> Com_1(main_GT_1003(ar_0 - 1, ar_1, arityPad)) [ 0 <= i344' /\ ar_0 - 1 = i344' /\ 1 <= ar_0 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 10*ar_1 + 6*ar_0 + 16

Time: 0.134 sec (SMT: 0.116 sec)

(16) BOUNDS(CONSTANT, 16 + 6 * |#0| + 10 * |#1|)

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

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

(18) Obligation:

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

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

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

(20) Obligation:

IntTrs with 47 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

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

obtained
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0

obtained
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
by chaining
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344

obtained
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
by chaining
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0

obtained
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
by chaining
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

(22) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'

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

Moved arithmethic from constraints to rhss.

main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
was transformed to
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'

main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

(24) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

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

Simplified expressions.

main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
was transformed to
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 - 1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 - 1 = i348'

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

main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 - 1, i300, env, static) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334

(26) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 - 1, i300, env, static) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 - 1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 - 1 = i348'

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

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

(28) Obligation:

IntTrs with 47 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

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

obtained
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i2, i3, env, static) -{0,0}> main_Load_3(i2, i3, env, static) :|: 0 >= 0
main_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_17(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, i3, env, static) -{1,1}> main_Load_41(i2, i3, env, static) :|: 0 >= 0
main_Load_41(i2, i3, env, static) -{0,0}> main_Load_42(i2, i3, env, static) :|: 0 >= 0
main_Load_42(i2, i3, env, static) -{0,0}> main_Load_44(i2, i3, env, static) :|: 0 <= static
main_Load_44(i2, i3, env, static) -{0,0}> main_Load_46(i2, i3, env, static) :|: 0 >= 0
main_Load_46(i2, i3, env, static) -{0,0}> main_Load_48(i2, i3, env, static) :|: 0 >= 0
main_Load_48(i2, i3, env, static) -{0,0}> main_Load_997(i2, i3, i2, i3, env, static) :|: 0 >= 0
main_Load_997(i298, i134, i299, i300, env, static) -{1,1}> main_GT_1003(i298, i134, i299, i300, env, static) :|: 0 >= 0

obtained
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
by chaining
main_GT_1003(i298, i134, i334, i300, env, static) -{0,0}> main_GT_1006(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_GT_1006(i298, i134, i334, i300, env, static) -{1,1}> main_Load_1010(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Load_1010(i298, i134, i334, i300, env, static) -{1,1}> main_LE_1015(i298, i134, i334, i300, env, static) :|: 1 <= i334
main_LE_1015(i298, i134, i334, i300, env, static) -{1,1}> main_Inc_1019(i298, i134, i334, i300, env, static) :|: 1 <= i334 && 0 < i334
main_Inc_1019(i298, i134, i334, i300, env, static) -{1,1}> main_JMP_1027(i298, i134, i344, i300, env, static) :|: i334 + -1 = i344 && 1 <= i334 && 0 <= i344
main_JMP_1027(i298, i134, i344, i300, env, static) -{1,1}> main_Load_1035(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_Load_1035(i298, i134, i344, i300, env, static) -{1,1}> main_GT_1044(i298, i134, i344, i300, env, static) :|: 0 <= i344
main_GT_1044(i298, i134, i344, i300, env, static) -{0,0}> main_GT_1003(i298, i134, i344, i300, env, static) :|: 0 <= i344

obtained
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
by chaining
main_GT_1003(i298, i134, i333, i300, env, static) -{0,0}> main_GT_1005(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_GT_1005(i298, i134, i333, i300, env, static) -{1,1}> main_Load_1008(i298, i134, i333, i300, env, static) :|: i333 <= 0
main_Load_1008(i298, i134, i333, i300, env, static) -{1,1}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0

obtained
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
by chaining
main_LE_1013(i298, i134, i342, i333, env, static) -{0,0}> main_LE_1017(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1017(i298, i134, i342, i333, env, static) -{1,1}> main_Load_1024(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Load_1024(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1032(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1032(i298, i134, i333, i342, env, static) -{1,1}> main_Load_1038(i298, i134, i333, i342, env, static) :|: 1 <= i342 && i333 <= 0
main_Load_1038(i298, i134, i333, i342, env, static) -{1,1}> main_LE_1047(i298, i134, i342, i333, env, static) :|: 1 <= i342 && i333 <= 0
main_LE_1047(i298, i134, i342, i333, env, static) -{1,1}> main_Inc_1049(i298, i134, i333, i342, env, static) :|: 1 <= i342 && 0 < i342 && i333 <= 0
main_Inc_1049(i298, i134, i333, i342, env, static) -{1,1}> main_JMP_1051(i298, i134, i333, i348, env, static) :|: 1 <= i342 && 0 <= i348 && i333 <= 0 && i342 + -1 = i348
main_JMP_1051(i298, i134, i333, i348, env, static) -{1,1}> main_Load_1055(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_Load_1055(i298, i134, i333, i348, env, static) -{1,1}> main_GT_1062(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0
main_GT_1062(i298, i134, i333, i348, env, static) -{0,0}> main_GT_1003(i298, i134, i333, i348, env, static) :|: 0 <= i348 && i333 <= 0

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'

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

Moved arithmethic from constraints to rhss.

main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i348', env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
was transformed to
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'

main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i344', i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334

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

Simplified expressions.

main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 + -1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 + -1 = i348'
was transformed to
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 - 1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 - 1 = i348'

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

main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 + -1, i300, env, static) :|: 0 <= i344' && i334 + -1 = i344' && 1 <= i334 && 0 < i334
was transformed to
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 - 1, i300, env, static) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GT_1003(i298, i134, i333, i300, env, static) -{2,2}> main_LE_1013(i298, i134, i300, i333, env, static) :|: i333 <= 0
main_LE_1013(i298, i134, i341, i333, env, static) -{0,0}> main_LE_1016(i298, i134, i341, i333, env, static) :|: i341 <= 0 && i333 <= 0
main_Load_2(i2, i3, env, static) -{16,16}> main_GT_1003(i2, i3, i2, i3, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_GT_1003(i298, i134, i334, i300, env, static) -{6,6}> main_GT_1003(i298, i134, i334 - 1, i300, env, static) :|: 0 <= i344' && i334 - 1 = i344' && 1 <= i334 && 0 < i334
main_LE_1013(i298, i134, i342, i333, env, static) -{8,8}> main_GT_1003(i298, i134, i333, i342 - 1, env, static) :|: 0 < i342 && 0 <= i348' && i333 <= 0 && 1 <= i342 && i342 - 1 = i348'