Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

/**
 * A very simple loop over an array.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class Loop1 {
    public static void main(String[] args) {
	for (int i = 0; i < args.length; i++) {}
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Loop1.main([Ljava/lang/String;)V: Graph of 40 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Loop1.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
• Marker field analysis yielded the following relations that could be markers:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 8 IRules

P rules:
f215_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27) → f217_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, java.lang.Object(ARRAY(i6)))
f217_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, java.lang.Object(ARRAY(i6))) → f219_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) | >=(i6, 0)
f219_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) → f222_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6)
f222_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) → f225_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) | <(i27, i6)
f225_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) → f228_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), +(i27, 1)) | >=(i27, 0)
f228_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i30) → f248_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i30)
f248_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i30) → f212_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i30)
f212_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) → f215_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27)

Combined rules. Obtained 1 IRules

P rules:
f215_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f215_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 0)), <(x1, x0))

Filtered ground terms:

f215_0_main_Load(x1, x2, x3, x4, x5) → f215_0_main_Load(x2, x3, x4, x5)
Cond_f215_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f215_0_main_Load(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f215_0_main_Load(x1, x2, x3, x4) → f215_0_main_Load(x2, x4)
Cond_f215_0_main_Load(x1, x2, x3, x4, x5) → Cond_f215_0_main_Load(x1, x3, x5)

Prepared 1 rules for path length conversion:

P rules:
f215_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f215_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 0)), <(x1, x0))

Finished conversion. Obtained 1 rules.

P rules:
f215_0_main_Load(v5, x1, x0) → f215_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(6) Obligation:

Rules:
f215_0_main_Load(v5, x1, x0) → f215_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f215_0_main_Load(x5, x7, x9)] = -x7 + x9

Therefore the following rule(s) have been dropped:

f215_0_main_Load(x0, x1, x2) → f215_0_main_Load(x3, +(x1, 1), x2) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x2)), >(x2, -1)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))

(8) YES