Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package TwoWay;

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    final String string = args[index];
    index++;
    return string.length();
  }
}


package TwoWay;

public class TwoWay {
	public static void main(String[] args) {
		Random.args = args;
		twoWay(true, Random.random());
	}

	public static int twoWay(boolean terminate, int n) {
		if (n < 0) {
			return 1;
		} else {
			int m = n;
			if (terminate) {
				m--;
			} else {
				m++;
			}
			return m*twoWay(terminate, m);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
TwoWay.TwoWay.main([Ljava/lang/String;)V: Graph of 107 nodes with 0 SCCs.

TwoWay.TwoWay.twoWay(ZI)I: Graph of 30 nodes with 0 SCCs.

(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: TwoWay.TwoWay.twoWay(ZI)I
SCC calls the following helper methods: TwoWay.TwoWay.twoWay(ZI)I
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 16 IRules

P rules:
f253_0_twoWay_GE(EOS, matching1, i29, matching2, i29, i29) → f261_0_twoWay_GE(EOS, 1, i29, 1, i29, i29) | &&(=(matching1, 1), =(matching2, 1))
f261_0_twoWay_GE(EOS, matching1, i29, matching2, i29, i29) → f271_0_twoWay_Load(EOS, 1, i29, 1, i29) | &&(&&(>=(i29, 0), =(matching1, 1)), =(matching2, 1))
f271_0_twoWay_Load(EOS, matching1, i29, matching2, i29) → f280_0_twoWay_Store(EOS, 1, i29, 1, i29) | &&(=(matching1, 1), =(matching2, 1))
f280_0_twoWay_Store(EOS, matching1, i29, matching2, i29) → f291_0_twoWay_Load(EOS, 1, i29, 1, i29) | &&(=(matching1, 1), =(matching2, 1))
f291_0_twoWay_Load(EOS, matching1, i29, matching2, i29) → f328_0_twoWay_EQ(EOS, 1, i29, 1, i29, 1) | &&(=(matching1, 1), =(matching2, 1))
f328_0_twoWay_EQ(EOS, matching1, i29, matching2, i29, matching3) → f331_0_twoWay_Inc(EOS, 1, i29, 1, i29) | &&(&&(&&(>(1, 0), =(matching1, 1)), =(matching2, 1)), =(matching3, 1))
f331_0_twoWay_Inc(EOS, matching1, i29, matching2, i29) → f335_0_twoWay_JMP(EOS, 1, i29, 1, +(i29, -1)) | &&(&&(>=(i29, 0), =(matching1, 1)), =(matching2, 1))
f335_0_twoWay_JMP(EOS, matching1, i29, matching2, i42) → f337_0_twoWay_Load(EOS, 1, i29, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f337_0_twoWay_Load(EOS, matching1, i29, matching2, i42) → f338_0_twoWay_Load(EOS, 1, i29, 1, i42, i42) | &&(=(matching1, 1), =(matching2, 1))
f338_0_twoWay_Load(EOS, matching1, i29, matching2, i42, i42) → f341_0_twoWay_Load(EOS, 1, i29, i42, i42, 1) | &&(=(matching1, 1), =(matching2, 1))
f341_0_twoWay_Load(EOS, matching1, i29, i42, i42, matching2) → f343_0_twoWay_InvokeMethod(EOS, 1, i29, i42, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f343_0_twoWay_InvokeMethod(EOS, matching1, i29, i42, matching2, i42) → f345_0_twoWay_Load(EOS, 1, i42, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f343_0_twoWay_InvokeMethod(EOS, matching1, i29, i42, matching2, i42) → f345_1_twoWay_Load(EOS, 1, i29, i42, 1, i42, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f345_0_twoWay_Load(EOS, matching1, i42, matching2, i42) → f347_0_twoWay_Load(EOS, 1, i42, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f347_0_twoWay_Load(EOS, matching1, i42, matching2, i42) → f247_0_twoWay_Load(EOS, 1, i42, 1, i42) | &&(=(matching1, 1), =(matching2, 1))
f247_0_twoWay_Load(EOS, matching1, i25, matching2, i25) → f253_0_twoWay_GE(EOS, 1, i25, 1, i25, i25) | &&(=(matching1, 1), =(matching2, 1))

Combined rules. Obtained 2 IRules

P rules:
f253_0_twoWay_GE(EOS, 1, x1, 1, x1, x1) → f345_1_twoWay_Load(EOS, 1, x1, -(x1, 1), 1, -(x1, 1), 1, -(x1, 1)) | >(+(x1, 1), 0)
f253_0_twoWay_GE(EOS, 1, x1, 1, x1, x1) → f253_0_twoWay_GE(EOS, 1, -(x1, 1), 1, -(x1, 1), -(x1, 1)) | >(+(x1, 1), 0)

Filtered ground terms:

f253_0_twoWay_GE(x1, x2, x3, x4, x5, x6) → f253_0_twoWay_GE(x3, x5, x6)
Cond_f253_0_twoWay_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f253_0_twoWay_GE(x1, x4, x6, x7)
f345_1_twoWay_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f345_1_twoWay_Load(x3, x4, x6, x8)
Cond_f253_0_twoWay_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f253_0_twoWay_GE1(x1, x4, x6, x7)

Filtered duplicate terms:

f253_0_twoWay_GE(x1, x2, x3) → f253_0_twoWay_GE(x3)
Cond_f253_0_twoWay_GE(x1, x2, x3, x4) → Cond_f253_0_twoWay_GE(x1, x4)
f345_1_twoWay_Load(x1, x2, x3, x4) → f345_1_twoWay_Load(x4)
Cond_f253_0_twoWay_GE1(x1, x2, x3, x4) → Cond_f253_0_twoWay_GE1(x1, x4)

Filtered unneeded terms:

Cond_f253_0_twoWay_GE(x1, x2) → Cond_f253_0_twoWay_GE(x1)

Prepared 2 rules for path length conversion:

P rules:
f253_0_twoWay_GE(x1) → f345_1_twoWay_Load(-(x1, 1)) | >(+(x1, 1), 0)
f253_0_twoWay_GE(x1) → f253_0_twoWay_GE(-(x1, 1)) | >(+(x1, 1), 0)

Finished conversion. Obtained 1 rules.

P rules:
f253_0_twoWay_GE(x1) → f253_0_twoWay_GE(-(x1, 1)) | >(x1, -1)

(6) Obligation:

Rules:
f253_0_twoWay_GE(x1) → f253_0_twoWay_GE(-(x1, 1)) | >(x1, -1)

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f253_0_twoWay_GE(x2)] = x2

Therefore the following rule(s) have been dropped:

f253_0_twoWay_GE(x0) → f253_0_twoWay_GE(-(x0, 1)) | >(x0, -1)

(8) YES