Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 1007 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 545 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇒, 0 ms)
        ↳9 intTRS
        ↳10 TerminationGraphProcessor (⇔, 5 ms)
        ↳11 YES
    ↳12 JBCTerminationSCC
        ↳13 SCCToIntTRSProof (⇒, 120 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

JBC Problem based on JBC Program:
package BinarySearch;

public class BinarySearch {
	public static void main(String[] argv) {
		Random.args = argv;

		int[] data = createArray();
		binarySearch(data, Random.random());
	}

	public static boolean binarySearch(int[] data, int val) {
		return binarySearch(data, val, 0, data.length);
	}

	private static boolean binarySearch(int[] data, int val, int l, int u) {
		if (l > u) {
			return false;
		}
		
		int mid = l + (u - l)/2;
		if (data[mid] == val) {
			return true;	
		} else {
			if (binarySearch(data, val, l, mid - 1)) {
				return true;
			}
			return binarySearch(data, val, mid + 1, u);
		}
	}

	public static int[] createArray() {
		int[] data = new int[Random.random()];
		for (int i = 0; i < data.length; i++) {
			data[i] = Random.random();
		}
		return data;
	}
}


package BinarySearch;

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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

BinarySearch.BinarySearch.createArray()[I: Graph of 180 nodes with 1 SCC.

BinarySearch.BinarySearch.binarySearch([IIII)Z: Graph of 148 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BinarySearch.BinarySearch.binarySearch([IIII)Z
SCC calls the following helper methods: BinarySearch.BinarySearch.binarySearch([IIII)Z
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 60 IRules

P rules:
f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655) → f2349_0_binarySearch_LE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656)
f2349_0_binarySearch_LE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656) → f2351_0_binarySearch_LE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656)
f2351_0_binarySearch_LE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656) → f2354_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656) | <=(i655, i656)
f2354_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656) → f2357_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655)
f2357_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655) → f2359_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656)
f2359_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656) → f2363_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656, i655)
f2363_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i656, i655) → f2379_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, -(i656, i655)) | >=(i655, 0)
f2379_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i677) → f2382_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i677, 2)
f2382_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i677, matching1) → f2386_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, /(i677, 2)) | =(matching1, 2)
f2386_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655, i685) → f2390_0_binarySearch_Store(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, +(i655, i685)) | >=(i655, 0)
f2390_0_binarySearch_Store(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688) → f2397_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688)
f2397_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688) → f2399_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688, java.lang.Object(ARRAY(i653)))
f2399_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688, java.lang.Object(ARRAY(i653))) → f2401_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i688, java.lang.Object(ARRAY(i653)), i688)
f2401_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i694) → f2405_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i694)
f2405_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i694) → f2408_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i694)
f2408_0_binarySearch_ArrayAccess(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i694) → f2411_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695) | <(i694, i653)
f2411_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695) → f2416_0_binarySearch_NE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695, i654)
f2416_0_binarySearch_NE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695, i654) → f2420_0_binarySearch_NE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695, i654)
f2420_0_binarySearch_NE(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, i695, i654) → f2426_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694) | !(=(i695, i654))
f2426_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694) → f2433_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)))
f2433_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653))) → f2436_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i654)
f2436_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i694, java.lang.Object(ARRAY(i653)), i654) → f2441_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655)
f2441_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655) → f2466_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i694)
f2466_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i694) → f2470_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i694, 1)
f2470_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i694, matching1) → f2473_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, -(i694, 1)) | &&(>=(i694, 0), =(matching1, 1))
f2473_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i717) → f2476_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717)
f2473_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i717) → f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i656, i694, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717)
f2476_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717) → f2481_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717)
f2481_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717) → f2344_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i717, java.lang.Object(ARRAY(i653)), i654, i655, i717)
f2344_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656) → f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i653)), i654, i655, i656, java.lang.Object(ARRAY(i653)), i654, i655, i656, i655)
f2520_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, java.lang.Object(ARRAY(i730)), i732, i734, i736, java.lang.Object(ARRAY(i730)), i732, i734, i736, matching1) → f2528_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, 0) | =(matching1, 0)
f2528_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, matching1) → f3166_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, 0) | =(matching1, 0)
f3166_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i656, i694, matching1) → f3220_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i656, i694, 0) | =(matching1, 0)
f3220_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i656, i694, matching1) → f3224_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i656, i694) | =(matching1, 0)
f3224_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i656, i694) → f3233_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i1308, i656, i694, java.lang.Object(ARRAY(i1307)))
f3233_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i1308, i656, i694, java.lang.Object(ARRAY(i1307))) → f3239_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, i694, java.lang.Object(ARRAY(i1307)), i1308)
f3239_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, i694, java.lang.Object(ARRAY(i1307)), i1308) → f3307_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, i694)
f3307_0_binarySearch_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, i694) → f3320_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, i694, 1)
f3320_0_binarySearch_IntArithmetic(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, i694, matching1) → f3321_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, +(i694, 1)) | &&(>=(i694, 0), =(matching1, 1))
f3321_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482) → f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656) → f3324_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656) → f3324_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f3324_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656) → f3326_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f3326_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656) → f2344_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f2521_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, java.lang.Object(ARRAY(i750)), i752, i754, i756, java.lang.Object(ARRAY(i750)), i752, i754, i756, i740, matching1) → f2530_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, 1) | =(matching1, 1)
f2530_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, matching1) → f2620_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, 1) | =(matching1, 1)
f2620_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i790)), i792, i794, i656, java.lang.Object(ARRAY(i790)), i792, i656, i694, matching1) → f3166_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i790)), i792, i794, i656, java.lang.Object(ARRAY(i790)), i792, i656, i694, 1) | =(matching1, 1)
f3318_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1455)), i1457, i1459, i656, java.lang.Object(ARRAY(i1455)), i1457, i656, i694, java.lang.Object(ARRAY(i1455)), i1457, i1459, i1461, java.lang.Object(ARRAY(i1455)), i1457, i1461, i1446, matching1) → f2608_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1455)), i1457, i1459, i656, java.lang.Object(ARRAY(i1455)), i1457, i656, i694, java.lang.Object(ARRAY(i1455)), i1457, i1459, i1461, java.lang.Object(ARRAY(i1455)), i1457, i1461, i1446, 1) | =(matching1, 1)
f2608_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i790)), i792, i794, i656, java.lang.Object(ARRAY(i790)), i792, i656, i694, java.lang.Object(ARRAY(i790)), i792, i794, i796, java.lang.Object(ARRAY(i790)), i792, i796, i781, matching1) → f2620_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i790)), i792, i794, i656, java.lang.Object(ARRAY(i790)), i792, i656, i694, 1) | =(matching1, 1)
f3682_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1715)), i1717, i1719, i656, java.lang.Object(ARRAY(i1715)), i1717, i656, i694, java.lang.Object(ARRAY(i1715)), i1717, i1719, i1721, matching1) → f3116_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1715)), i1717, i1719, i656, java.lang.Object(ARRAY(i1715)), i1717, i656, i694, java.lang.Object(ARRAY(i1715)), i1717, i1719, i1721, 0) | =(matching1, 0)
f3116_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1244)), i1245, i1246, i656, java.lang.Object(ARRAY(i1244)), i1245, i656, i694, java.lang.Object(ARRAY(i1244)), i1245, i1246, i1247, i1243) → f3165_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1244)), i1245, i1246, i656, java.lang.Object(ARRAY(i1244)), i1245, i656, i694, i1243)
f3165_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1244)), i1245, i1246, i656, java.lang.Object(ARRAY(i1244)), i1245, i656, i694, i1243) → f3166_0_binarySearch_EQ(EOS, java.lang.Object(ARRAY(i1244)), i1245, i1246, i656, java.lang.Object(ARRAY(i1244)), i1245, i656, i694, i1243)
f3691_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1835)), i1837, i1839, i656, java.lang.Object(ARRAY(i1835)), i1837, i656, i694, java.lang.Object(ARRAY(i1835)), i1837, i1839, i1841, matching1) → f3116_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1835)), i1837, i1839, i656, java.lang.Object(ARRAY(i1835)), i1837, i656, i694, java.lang.Object(ARRAY(i1835)), i1837, i1839, i1841, 1) | =(matching1, 1)
f4023_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i2100)), i2102, i2104, i656, java.lang.Object(ARRAY(i2100)), i2102, i656, i694, java.lang.Object(ARRAY(i2100)), i2102, i2104, i2106, i2091) → f3116_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i2100)), i2102, i2104, i656, java.lang.Object(ARRAY(i2100)), i2102, i656, i694, java.lang.Object(ARRAY(i2100)), i2102, i2104, i2106, i2091)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, java.lang.Object(ARRAY(i730)), i732, i734, i736, java.lang.Object(ARRAY(i730)), i732, i734, i736) → f2520_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i730)), i732, i734, i656, java.lang.Object(ARRAY(i730)), i732, i656, i694, java.lang.Object(ARRAY(i730)), i732, i734, i736, java.lang.Object(ARRAY(i730)), i732, i734, i736, 0)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, java.lang.Object(ARRAY(i750)), i752, i754, i756, java.lang.Object(ARRAY(i750)), i752, i754, i756) → f2521_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i750)), i752, i754, i656, java.lang.Object(ARRAY(i750)), i752, i656, i694, java.lang.Object(ARRAY(i750)), i752, i754, i756, java.lang.Object(ARRAY(i750)), i752, i754, i756, i740, 1)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1455)), i1457, i1459, i656, java.lang.Object(ARRAY(i1455)), i1457, i656, i694, java.lang.Object(ARRAY(i1455)), i1457, i1459, i1461, java.lang.Object(ARRAY(i1455)), i1457, i1459, i1461) → f3318_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1455)), i1457, i1459, i656, java.lang.Object(ARRAY(i1455)), i1457, i656, i694, java.lang.Object(ARRAY(i1455)), i1457, i1459, i1461, java.lang.Object(ARRAY(i1455)), i1457, i1461, i1446, 1)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1715)), i1717, i1719, i656, java.lang.Object(ARRAY(i1715)), i1717, i656, i694, java.lang.Object(ARRAY(i1715)), i1717, i1719, i1721, java.lang.Object(ARRAY(i1715)), i1717, i1719, i1721) → f3682_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1715)), i1717, i1719, i656, java.lang.Object(ARRAY(i1715)), i1717, i656, i694, java.lang.Object(ARRAY(i1715)), i1717, i1719, i1721, 0)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1835)), i1837, i1839, i656, java.lang.Object(ARRAY(i1835)), i1837, i656, i694, java.lang.Object(ARRAY(i1835)), i1837, i1839, i1841, java.lang.Object(ARRAY(i1835)), i1837, i1839, i1841) → f3691_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i1835)), i1837, i1839, i656, java.lang.Object(ARRAY(i1835)), i1837, i656, i694, java.lang.Object(ARRAY(i1835)), i1837, i1839, i1841, 1)
f2476_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i2100)), i2102, i2104, i656, java.lang.Object(ARRAY(i2100)), i2102, i656, i694, java.lang.Object(ARRAY(i2100)), i2102, i2104, i2106, java.lang.Object(ARRAY(i2100)), i2102, i2104, i2106) → f4023_0_binarySearch_Return(EOS, java.lang.Object(ARRAY(i2100)), i2102, i2104, i656, java.lang.Object(ARRAY(i2100)), i2102, i656, i694, java.lang.Object(ARRAY(i2100)), i2102, i2104, i2106, i2091)

Combined rules. Obtained 4 IRules

P rules:
f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656) → f3324_1_binarySearch_Load(EOS, java.lang.Object(ARRAY(i1307)), i1308, i1309, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x2, x3, x2) → f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1), java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1), x2) | &&(&&(&&(>=(x3, x2), >(+(x2, 1), 0)), <(+(x2, /(-(x3, x2), 2)), x0)), >=(+(x2, /(-(x3, x2), 2)), 0))
f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x3) → f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(x0)), x1, x4, x3, java.lang.Object(ARRAY(x0)), x1, x4, x3, x4)
f2346_0_binarySearch_Load(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x2, x3, x2) → f3322_0_binarySearch_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, +(+(x2, /(-(x3, x2), 2)), 1), x3) | &&(&&(&&(>=(x3, x2), >(+(x2, 1), 0)), >=(+(x2, /(-(x3, x2), 2)), 0)), <(+(x2, /(-(x3, x2), 2)), x0))

Filtered ground terms:


f3322_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f3322_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
f3324_1_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → f3324_1_binarySearch_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
f2346_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f2346_0_binarySearch_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f2346_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2346_0_binarySearch_Load(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Cond_f2346_0_binarySearch_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2346_0_binarySearch_Load1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)

Filtered duplicate terms:


f3322_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → f3322_0_binarySearch_InvokeMethod(x3, x5, x6, x7, x8)
f3324_1_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → f3324_1_binarySearch_Load(x3, x9, x10, x11, x12)
f2346_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f2346_0_binarySearch_Load(x5, x6, x8, x9)
Cond_f2346_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2346_0_binarySearch_Load(x1, x6, x7, x9, x10)
Cond_f2346_0_binarySearch_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2346_0_binarySearch_Load1(x1, x6, x7, x9, x10)

Filtered unneeded terms:


Cond_f2346_0_binarySearch_Load(x1, x2, x3, x4, x5) → Cond_f2346_0_binarySearch_Load(x1, x2, x4, x5)
Cond_f2346_0_binarySearch_Load1(x1, x2, x3, x4, x5) → Cond_f2346_0_binarySearch_Load1(x1, x2, x4, x5)
f2346_0_binarySearch_Load(x1, x2, x3, x4) → f2346_0_binarySearch_Load(x1, x3, x4)
f3322_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → f3322_0_binarySearch_InvokeMethod(x2, x4, x5)

Prepared 4 rules for path length conversion:

P rules:
f3322_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(i1307)), i1482, i656, i1307) → f3324_1_binarySearch_Load(i1309, java.lang.Object(ARRAY(i1307)), i1308, i1482, i656)
f2346_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x3, x2, x0) → f2346_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2, x0) | &&(&&(&&(>=(x3, x2), >(+(x2, 1), 0)), <(+(x2, /(-(x3, x2), 2)), x0)), >=(+(x2, /(-(x3, x2), 2)), 0))
f3322_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x4, x3, x0) → f2346_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x3, x4, x0)
f2346_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x3, x2, x0) → f3322_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), +(+(x2, /(-(x3, x2), 2)), 1), x3, x0) | &&(&&(&&(>=(x3, x2), >(+(x2, 1), 0)), >=(+(x2, /(-(x3, x2), 2)), 0)), <(+(x2, /(-(x3, x2), 2)), x0))

Finished conversion. Obtained 5 rules.

P rules:
f2346_0_binarySearch_Load(v22, x6, x7, x5) → f2346_0_binarySearch_Load'(v22, x6, x7, x5) | &&(&&(&&(&&(&&(&&(>(x7, -1), <=(x7, x6)), >=(+(x7, div1), 0)), <(+(x7, div), x5)), >(+(v23, 1), 1)), <=(v23, v22)), >(+(v22, 1), 1))
f2346_0_binarySearch_Load'(v22, x6, x7, x5) → f2346_0_binarySearch_Load(v23, -(+(x7, div2), 1), x7, x5) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x7, -1), <=(x7, x6)), >=(+(x7, div1), 0)), <(+(x7, div), x5)), >=(-(-(x6, x7), *(2, div2)), 0)), <(-(-(x6, x7), *(2, div2)), 2)), >=(-(-(x6, x7), *(2, div1)), 0)), <(-(-(x6, x7), *(2, div1)), 2)), >=(-(-(x6, x7), *(2, div)), 0)), <(-(-(x6, x7), *(2, div)), 2)), >(+(v23, 1), 1)), <=(v23, v22)), >(+(v22, 1), 1))
f3322_0_binarySearch_InvokeMethod(v24, x9, x10, x8) → f2346_0_binarySearch_Load(v25, x10, x9, x8) | &&(&&(>(+(v25, 1), 1), <=(v25, v24)), >(+(v24, 1), 1))
f2346_0_binarySearch_Load(v26, x12, x13, x11) → f2346_0_binarySearch_Load'(v26, x12, x13, x11) | &&(&&(&&(&&(&&(&&(>(x13, -1), <=(x13, x12)), <(+(x13, div1), x11)), >=(+(x13, div), 0)), >(+(v27, 1), 1)), <=(v27, v26)), >(+(v26, 1), 1))
f2346_0_binarySearch_Load'(v26, x12, x13, x11) → f3322_0_binarySearch_InvokeMethod(v27, +(+(x13, div2), 1), x12, x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x13, -1), <=(x13, x12)), <(+(x13, div1), x11)), >=(+(x13, div), 0)), >=(-(-(x12, x13), *(2, div2)), 0)), <(-(-(x12, x13), *(2, div2)), 2)), >=(-(-(x12, x13), *(2, div1)), 0)), <(-(-(x12, x13), *(2, div1)), 2)), >=(-(-(x12, x13), *(2, div)), 0)), <(-(-(x12, x13), *(2, div)), 2)), >(+(v27, 1), 1)), <=(v27, v26)), >(+(v26, 1), 1))

(7) Obligation:

Rules:
f2346_0_binarySearch_Load(v22, x6, x7, x5) → f2346_0_binarySearch_Load'(v22, x6, x7, x5) | &&(&&(&&(&&(&&(&&(>(x7, -1), <=(x7, x6)), >=(+(x7, div1), 0)), <(+(x7, div), x5)), >(+(v23, 1), 1)), <=(v23, v22)), >(+(v22, 1), 1))
f2346_0_binarySearch_Load'(v22, x6, x7, x5) → f2346_0_binarySearch_Load(v23, -(+(x7, div2), 1), x7, x5) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x7, -1), <=(x7, x6)), >=(+(x7, div1), 0)), <(+(x7, div), x5)), >=(-(-(x6, x7), *(2, div2)), 0)), <(-(-(x6, x7), *(2, div2)), 2)), >=(-(-(x6, x7), *(2, div1)), 0)), <(-(-(x6, x7), *(2, div1)), 2)), >=(-(-(x6, x7), *(2, div)), 0)), <(-(-(x6, x7), *(2, div)), 2)), >(+(v23, 1), 1)), <=(v23, v22)), >(+(v22, 1), 1))
f3322_0_binarySearch_InvokeMethod(v24, x9, x10, x8) → f2346_0_binarySearch_Load(v25, x10, x9, x8) | &&(&&(>(+(v25, 1), 1), <=(v25, v24)), >(+(v24, 1), 1))
f2346_0_binarySearch_Load(v26, x12, x13, x11) → f2346_0_binarySearch_Load'(v26, x12, x13, x11) | &&(&&(&&(&&(&&(&&(>(x13, -1), <=(x13, x12)), <(+(x13, div1), x11)), >=(+(x13, div), 0)), >(+(v27, 1), 1)), <=(v27, v26)), >(+(v26, 1), 1))
f2346_0_binarySearch_Load'(v26, x12, x13, x11) → f3322_0_binarySearch_InvokeMethod(v27, +(+(x13, div2), 1), x12, x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x13, -1), <=(x13, x12)), <(+(x13, div1), x11)), >=(+(x13, div), 0)), >=(-(-(x12, x13), *(2, div2)), 0)), <(-(-(x12, x13), *(2, div2)), 2)), >=(-(-(x12, x13), *(2, div1)), 0)), <(-(-(x12, x13), *(2, div1)), 2)), >=(-(-(x12, x13), *(2, div)), 0)), <(-(-(x12, x13), *(2, div)), 2)), >(+(v27, 1), 1)), <=(v27, v26)), >(+(v26, 1), 1))

(8) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f2346_0_binarySearch_Load(x36, x38, x40, x42)] = 2·x38 - 2·x40
[f2346_0_binarySearch_Load'(x45, x47, x49, x51)] = -1 + x47 - x49
[f3322_0_binarySearch_InvokeMethod(x54, x56, x58, x60)] = -2·x56 + 2·x58

Therefore the following rule(s) have been dropped:


f2346_0_binarySearch_Load(x0, x1, x2, x3) → f2346_0_binarySearch_Load'(x0, x1, x2, x3) | &&(&&(&&(&&(&&(&&(>(x2, -1), <=(x2, x1)), >=(+(x2, x4), 0)), <(+(x2, x5), x3)), >(+(x6, 1), 1)), <=(x6, x0)), >(+(x0, 1), 1))
f2346_0_binarySearch_Load(x20, x21, x22, x23) → f2346_0_binarySearch_Load'(x20, x21, x22, x23) | &&(&&(&&(&&(&&(&&(>(x22, -1), <=(x22, x21)), <(+(x22, x24), x23)), >=(+(x22, x25), 0)), >(+(x26, 1), 1)), <=(x26, x20)), >(+(x20, 1), 1))

(9) Obligation:

Rules:
f2346_0_binarySearch_Load'(x7, x8, x9, x10) → f2346_0_binarySearch_Load(x11, -(+(x9, x12), 1), x9, x10) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x9, -1), <=(x9, x8)), >=(+(x9, x13), 0)), <(+(x9, x14), x10)), >=(-(-(x8, x9), *(2, x12)), 0)), <(-(-(x8, x9), *(2, x12)), 2)), >=(-(-(x8, x9), *(2, x13)), 0)), <(-(-(x8, x9), *(2, x13)), 2)), >=(-(-(x8, x9), *(2, x14)), 0)), <(-(-(x8, x9), *(2, x14)), 2)), >(+(x11, 1), 1)), <=(x11, x7)), >(+(x7, 1), 1))
f3322_0_binarySearch_InvokeMethod(x15, x16, x17, x18) → f2346_0_binarySearch_Load(x19, x17, x16, x18) | &&(&&(>(+(x19, 1), 1), <=(x19, x15)), >(+(x15, 1), 1))
f2346_0_binarySearch_Load'(x27, x28, x29, x30) → f3322_0_binarySearch_InvokeMethod(x31, +(+(x29, x32), 1), x28, x30) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x29, -1), <=(x29, x28)), <(+(x29, x33), x30)), >=(+(x29, x34), 0)), >=(-(-(x28, x29), *(2, x32)), 0)), <(-(-(x28, x29), *(2, x32)), 2)), >=(-(-(x28, x29), *(2, x33)), 0)), <(-(-(x28, x29), *(2, x33)), 2)), >=(-(-(x28, x29), *(2, x34)), 0)), <(-(-(x28, x29), *(2, x34)), 2)), >(+(x31, 1), 1)), <=(x31, x27)), >(+(x27, 1), 1))

(10) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).


(11) YES

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BinarySearch.BinarySearch.createArray()[I
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • java.lang.String: [count]
  • Marker field analysis yielded the following relations that could be markers:

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 30 IRules

P rules:
f1444_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335, i335) → f1448_0_createArray_ArrayLength(EOS, java.lang.Object(ARRAY(i80)), i335, i335, java.lang.Object(ARRAY(i80)))
f1448_0_createArray_ArrayLength(EOS, java.lang.Object(ARRAY(i80)), i335, i335, java.lang.Object(ARRAY(i80))) → f1454_0_createArray_GE(EOS, java.lang.Object(ARRAY(i80)), i335, i335, i80) | >=(i80, 0)
f1454_0_createArray_GE(EOS, java.lang.Object(ARRAY(i80)), i335, i335, i80) → f1459_0_createArray_GE(EOS, java.lang.Object(ARRAY(i80)), i335, i335, i80)
f1459_0_createArray_GE(EOS, java.lang.Object(ARRAY(i80)), i335, i335, i80) → f1467_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335) | <(i335, i80)
f1467_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335) → f1479_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)))
f1479_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80))) → f1485_0_createArray_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335)
f1485_0_createArray_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335) → f1502_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335)
f1502_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335) → f1508_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78)))
f1508_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78))) → f1517_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78)), i334)
f1517_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78)), i334) → f1521_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78)), i334)
f1521_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i78)), i334) → f1525_0_random_Store(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376) | <(i334, i78)
f1525_0_random_Store(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376) → f1535_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376)
f1535_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376) → f1543_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, i334)
f1543_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, i334) → f1553_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, i334, 1)
f1553_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, i334, matching1) → f1563_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, +(i334, 1)) | &&(>(i334, 0), =(matching1, 1))
f1563_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376, i354) → f1571_0_random_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376)
f1571_0_random_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376) → f1588_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, o376)
f1588_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub)) → f1602_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub))
f1602_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub)) → f1615_0_length_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub), java.lang.Object(o403sub))
f1615_0_length_Load(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub), java.lang.Object(o403sub)) → f1657_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(o403sub), java.lang.Object(o403sub))
f1657_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(java.lang.String(o416sub, i386)), java.lang.Object(java.lang.String(o416sub, i386))) → f1666_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(java.lang.String(o416sub, i386)), java.lang.Object(java.lang.String(o416sub, i386)))
f1666_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(java.lang.String(o416sub, i386)), java.lang.Object(java.lang.String(o416sub, i386))) → f1678_0_length_Return(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(java.lang.String(o416sub, i386)))
f1678_0_length_Return(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(java.lang.String(o416sub, i386))) → f1690_0_random_Return(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335)
f1690_0_random_Return(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335) → f1698_0_createArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335)
f1698_0_createArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335) → f1709_0_createArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335)
f1709_0_createArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i80)), i335, java.lang.Object(ARRAY(i80)), i335) → f1720_0_createArray_Inc(EOS, java.lang.Object(ARRAY(i80)), i335) | <(i335, i80)
f1720_0_createArray_Inc(EOS, java.lang.Object(ARRAY(i80)), i335) → f1745_0_createArray_JMP(EOS, java.lang.Object(ARRAY(i80)), +(i335, 1)) | >=(i335, 0)
f1745_0_createArray_JMP(EOS, java.lang.Object(ARRAY(i80)), i413) → f1769_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i413)
f1769_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i413) → f1433_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i413)
f1433_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335) → f1444_0_createArray_Load(EOS, java.lang.Object(ARRAY(i80)), i335, i335)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f1444_0_createArray_Load(x1, x2, x3, x4) → f1444_0_createArray_Load(x2, x3, x4)
Cond_f1444_0_createArray_Load(x1, x2, x3, x4, x5) → Cond_f1444_0_createArray_Load(x1, x3, x4, x5)

Filtered duplicate terms:


f1444_0_createArray_Load(x1, x2, x3) → f1444_0_createArray_Load(x1, x3)
Cond_f1444_0_createArray_Load(x1, x2, x3, x4) → Cond_f1444_0_createArray_Load(x1, x2, x4)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(14) Obligation:

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

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


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

(16) YES