Termination proof of /tmp/tmpCuMFmw/BinarySearch.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 750 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1810 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 690 ms)

        ↳9 AND

            ↳10 IDP

                ↳11 IDependencyGraphProof (⇔, 0 ms)

                ↳12 IDP

                ↳13 UsableRulesProof (⇔, 0 ms)

                ↳14 IDP

                ↳15 IDPNonInfProof (⇒, 2240 ms)

                ↳16 IDP

                ↳17 IDependencyGraphProof (⇔, 0 ms)

                ↳18 TRUE

            ↳19 IDP

                ↳20 IDependencyGraphProof (⇔, 0 ms)

                ↳21 IDP

                ↳22 UsableRulesProof (⇔, 0 ms)

                ↳23 IDP

                ↳24 IDPNonInfProof (⇒, 2420 ms)

                ↳25 IDP

                ↳26 IDependencyGraphProof (⇔, 0 ms)

                ↳27 TRUE

    ↳28 JBCTerminationSCC

        ↳29 SCCToIDPv1Proof (⇒, 290 ms)

        ↳30 IDP

        ↳31 IDPNonInfProof (⇒, 250 ms)

        ↳32 AND

            ↳33 IDP

                ↳34 IDependencyGraphProof (⇔, 0 ms)

                ↳35 TRUE

            ↳36 IDP

                ↳37 IDependencyGraphProof (⇔, 0 ms)

                ↳38 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_25 (Sun Microsystems Inc.) Main-Class: BinarySearch/BinarySearch

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 156 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: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 58 rules for P and 105 rules for R.

P rules:
1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542) → 1906_0_binarySearch_LE(EOS(STATIC_1906), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1906_0_binarySearch_LE(EOS(STATIC_1906), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1907_0_binarySearch_LE(EOS(STATIC_1907), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1907_0_binarySearch_LE(EOS(STATIC_1907), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1909_0_binarySearch_Load(EOS(STATIC_1909), java.lang.Object(ARRAY(i540)), i541, i542, i543) | <=(i542, i543)
1909_0_binarySearch_Load(EOS(STATIC_1909), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1911_0_binarySearch_Load(EOS(STATIC_1911), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542)
1911_0_binarySearch_Load(EOS(STATIC_1911), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542) → 1914_0_binarySearch_Load(EOS(STATIC_1914), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1914_0_binarySearch_Load(EOS(STATIC_1914), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1917_0_binarySearch_IntArithmetic(EOS(STATIC_1917), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543, i542)
1917_0_binarySearch_IntArithmetic(EOS(STATIC_1917), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543, i542) → 1923_0_binarySearch_ConstantStackPush(EOS(STATIC_1923), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, -(i543, i542))
1923_0_binarySearch_ConstantStackPush(EOS(STATIC_1923), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555) → 1925_0_binarySearch_IntArithmetic(EOS(STATIC_1925), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555, 2)
1925_0_binarySearch_IntArithmetic(EOS(STATIC_1925), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i555, matching1) → 1929_0_binarySearch_IntArithmetic(EOS(STATIC_1929), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, /(i555, 2)) | =(matching1, 2)
1929_0_binarySearch_IntArithmetic(EOS(STATIC_1929), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i558) → 1932_0_binarySearch_Store(EOS(STATIC_1932), java.lang.Object(ARRAY(i540)), i541, i542, i543, +(i542, i558))
1932_0_binarySearch_Store(EOS(STATIC_1932), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561) → 1937_0_binarySearch_Load(EOS(STATIC_1937), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561)
1937_0_binarySearch_Load(EOS(STATIC_1937), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561) → 1940_0_binarySearch_Load(EOS(STATIC_1940), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540)))
1940_0_binarySearch_Load(EOS(STATIC_1940), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540))) → 1942_0_binarySearch_ArrayAccess(EOS(STATIC_1942), java.lang.Object(ARRAY(i540)), i541, i542, i543, i561, java.lang.Object(ARRAY(i540)), i561)
1942_0_binarySearch_ArrayAccess(EOS(STATIC_1942), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1945_0_binarySearch_ArrayAccess(EOS(STATIC_1945), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1945_0_binarySearch_ArrayAccess(EOS(STATIC_1945), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1947_0_binarySearch_ArrayAccess(EOS(STATIC_1947), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1947_0_binarySearch_ArrayAccess(EOS(STATIC_1947), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1950_0_binarySearch_Load(EOS(STATIC_1950), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569) | <(i568, i540)
1950_0_binarySearch_Load(EOS(STATIC_1950), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569) → 1955_0_binarySearch_NE(EOS(STATIC_1955), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569, i541)
1955_0_binarySearch_NE(EOS(STATIC_1955), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569, i541) → 1958_0_binarySearch_NE(EOS(STATIC_1958), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569, i541)
1958_0_binarySearch_NE(EOS(STATIC_1958), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i569, i541) → 1964_0_binarySearch_Load(EOS(STATIC_1964), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568) | !(=(i569, i541))
1964_0_binarySearch_Load(EOS(STATIC_1964), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568) → 1970_0_binarySearch_Load(EOS(STATIC_1970), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)))
1970_0_binarySearch_Load(EOS(STATIC_1970), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540))) → 1975_0_binarySearch_Load(EOS(STATIC_1975), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i541)
1975_0_binarySearch_Load(EOS(STATIC_1975), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i541) → 1981_0_binarySearch_Load(EOS(STATIC_1981), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542)
1981_0_binarySearch_Load(EOS(STATIC_1981), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542) → 1990_0_binarySearch_ConstantStackPush(EOS(STATIC_1990), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i568)
1990_0_binarySearch_ConstantStackPush(EOS(STATIC_1990), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i568) → 1996_0_binarySearch_IntArithmetic(EOS(STATIC_1996), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i568, 1)
1996_0_binarySearch_IntArithmetic(EOS(STATIC_1996), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i568, matching1) → 1999_0_binarySearch_InvokeMethod(EOS(STATIC_1999), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, -(i568, 1)) | &&(>=(i568, 0), =(matching1, 1))
1999_0_binarySearch_InvokeMethod(EOS(STATIC_1999), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i580) → 2002_1_binarySearch_InvokeMethod(2002_0_binarySearch_Load(EOS(STATIC_2002), java.lang.Object(ARRAY(i540)), i541, i542, i580), java.lang.Object(ARRAY(i540)), i541, i543, i568, java.lang.Object(ARRAY(i540)), i541, i542, i580)
2002_0_binarySearch_Load(EOS(STATIC_2002), java.lang.Object(ARRAY(i540)), i541, i542, i580) → 2006_0_binarySearch_Load(EOS(STATIC_2006), java.lang.Object(ARRAY(i540)), i541, i542, i580)
2002_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(EOS(STATIC_1912), java.lang.Object(ARRAY(i588)), i589, i590, i591, matching1), java.lang.Object(ARRAY(i588)), i589, i543, i568, java.lang.Object(ARRAY(i588)), i589, i590, i591) → 2022_0_binarySearch_Return(EOS(STATIC_2022), java.lang.Object(ARRAY(i588)), i589, i543, i568, java.lang.Object(ARRAY(i588)), i589, i590, i591, java.lang.Object(ARRAY(i588)), i589, i590, i591, 0) | =(matching1, 0)
2002_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(EOS(STATIC_1972), java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, matching1), java.lang.Object(ARRAY(i601)), i602, i543, i568, java.lang.Object(ARRAY(i601)), i602, i603, i604) → 2023_0_binarySearch_Return(EOS(STATIC_2023), java.lang.Object(ARRAY(i601)), i602, i543, i568, java.lang.Object(ARRAY(i601)), i602, i603, i604, java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, 1) | =(matching1, 1)
2002_1_binarySearch_InvokeMethod(2312_0_binarySearch_Return(EOS(STATIC_2312), java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, matching1), java.lang.Object(ARRAY(i1099)), i1100, i543, i568, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102) → 2341_0_binarySearch_Return(EOS(STATIC_2341), java.lang.Object(ARRAY(i1099)), i1100, i543, i568, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, 1) | =(matching1, 1)
2002_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return(EOS(STATIC_2394), matching1), java.lang.Object(ARRAY(i1294)), i1295, i543, i568, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297) → 2449_0_binarySearch_Return(EOS(STATIC_2449), java.lang.Object(ARRAY(i1294)), i1295, i543, i568, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, 0) | =(matching1, 0)
2002_1_binarySearch_InvokeMethod(2405_0_binarySearch_Return(EOS(STATIC_2405), matching1), java.lang.Object(ARRAY(i1330)), i1331, i543, i568, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333) → 2457_0_binarySearch_Return(EOS(STATIC_2457), java.lang.Object(ARRAY(i1330)), i1331, i543, i568, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, 1) | =(matching1, 1)
2002_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(EOS(STATIC_2481), i1373), java.lang.Object(ARRAY(i1522)), i1523, i543, i568, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525) → 2555_0_binarySearch_Return(EOS(STATIC_2555), java.lang.Object(ARRAY(i1522)), i1523, i543, i568, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1373)
2006_0_binarySearch_Load(EOS(STATIC_2006), java.lang.Object(ARRAY(i540)), i541, i542, i580) → 1900_0_binarySearch_Load(EOS(STATIC_1900), java.lang.Object(ARRAY(i540)), i541, i542, i580)
1900_0_binarySearch_Load(EOS(STATIC_1900), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542)
2022_0_binarySearch_Return(EOS(STATIC_2022), java.lang.Object(ARRAY(i588)), i589, i543, i568, java.lang.Object(ARRAY(i588)), i589, i590, i591, java.lang.Object(ARRAY(i588)), i589, i590, i591, matching1) → 2028_0_binarySearch_EQ(EOS(STATIC_2028), java.lang.Object(ARRAY(i588)), i589, i543, i568, 0) | =(matching1, 0)
2028_0_binarySearch_EQ(EOS(STATIC_2028), java.lang.Object(ARRAY(i588)), i589, i543, i568, matching1) → 2282_0_binarySearch_EQ(EOS(STATIC_2282), java.lang.Object(ARRAY(i588)), i589, i543, i568, 0) | =(matching1, 0)
2282_0_binarySearch_EQ(EOS(STATIC_2282), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, matching1) → 2297_0_binarySearch_EQ(EOS(STATIC_2297), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, 0) | =(matching1, 0)
2297_0_binarySearch_EQ(EOS(STATIC_2297), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, matching1) → 2303_0_binarySearch_Load(EOS(STATIC_2303), java.lang.Object(ARRAY(i1019)), i1020, i543, i568) | =(matching1, 0)
2303_0_binarySearch_Load(EOS(STATIC_2303), java.lang.Object(ARRAY(i1019)), i1020, i543, i568) → 2313_0_binarySearch_Load(EOS(STATIC_2313), i1020, i543, i568, java.lang.Object(ARRAY(i1019)))
2313_0_binarySearch_Load(EOS(STATIC_2313), i1020, i543, i568, java.lang.Object(ARRAY(i1019))) → 2317_0_binarySearch_Load(EOS(STATIC_2317), i543, i568, java.lang.Object(ARRAY(i1019)), i1020)
2317_0_binarySearch_Load(EOS(STATIC_2317), i543, i568, java.lang.Object(ARRAY(i1019)), i1020) → 2332_0_binarySearch_ConstantStackPush(EOS(STATIC_2332), i543, java.lang.Object(ARRAY(i1019)), i1020, i568)
2332_0_binarySearch_ConstantStackPush(EOS(STATIC_2332), i543, java.lang.Object(ARRAY(i1019)), i1020, i568) → 2342_0_binarySearch_IntArithmetic(EOS(STATIC_2342), i543, java.lang.Object(ARRAY(i1019)), i1020, i568, 1)
2342_0_binarySearch_IntArithmetic(EOS(STATIC_2342), i543, java.lang.Object(ARRAY(i1019)), i1020, i568, matching1) → 2343_0_binarySearch_Load(EOS(STATIC_2343), i543, java.lang.Object(ARRAY(i1019)), i1020, +(i568, 1)) | &&(>=(i568, 0), =(matching1, 1))
2343_0_binarySearch_Load(EOS(STATIC_2343), i543, java.lang.Object(ARRAY(i1019)), i1020, i1130) → 2344_0_binarySearch_InvokeMethod(EOS(STATIC_2344), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543)
2344_0_binarySearch_InvokeMethod(EOS(STATIC_2344), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543) → 2346_1_binarySearch_InvokeMethod(2346_0_binarySearch_Load(EOS(STATIC_2346), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543)
2346_0_binarySearch_Load(EOS(STATIC_2346), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543) → 2347_0_binarySearch_Load(EOS(STATIC_2347), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543)
2347_0_binarySearch_Load(EOS(STATIC_2347), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543) → 1900_0_binarySearch_Load(EOS(STATIC_1900), java.lang.Object(ARRAY(i1019)), i1020, i1130, i543)
2023_0_binarySearch_Return(EOS(STATIC_2023), java.lang.Object(ARRAY(i601)), i602, i543, i568, java.lang.Object(ARRAY(i601)), i602, i603, i604, java.lang.Object(ARRAY(i601)), i602, i603, i604, i597, matching1) → 2030_0_binarySearch_EQ(EOS(STATIC_2030), java.lang.Object(ARRAY(i601)), i602, i543, i568, 1) | =(matching1, 1)
2030_0_binarySearch_EQ(EOS(STATIC_2030), java.lang.Object(ARRAY(i601)), i602, i543, i568, matching1) → 2083_0_binarySearch_EQ(EOS(STATIC_2083), java.lang.Object(ARRAY(i601)), i602, i543, i568, 1) | =(matching1, 1)
2083_0_binarySearch_EQ(EOS(STATIC_2083), java.lang.Object(ARRAY(i619)), i620, i543, i568, matching1) → 2282_0_binarySearch_EQ(EOS(STATIC_2282), java.lang.Object(ARRAY(i619)), i620, i543, i568, 1) | =(matching1, 1)
2341_0_binarySearch_Return(EOS(STATIC_2341), java.lang.Object(ARRAY(i1099)), i1100, i543, i568, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, matching1) → 2074_0_binarySearch_Return(EOS(STATIC_2074), java.lang.Object(ARRAY(i1099)), i1100, i543, i568, java.lang.Object(ARRAY(i1099)), i1100, i1101, i1102, java.lang.Object(ARRAY(i1099)), i1100, i1102, i1098, 1) | =(matching1, 1)
2074_0_binarySearch_Return(EOS(STATIC_2074), java.lang.Object(ARRAY(i619)), i620, i543, i568, java.lang.Object(ARRAY(i619)), i620, i621, i622, java.lang.Object(ARRAY(i619)), i620, i622, i618, matching1) → 2083_0_binarySearch_EQ(EOS(STATIC_2083), java.lang.Object(ARRAY(i619)), i620, i543, i568, 1) | =(matching1, 1)
2449_0_binarySearch_Return(EOS(STATIC_2449), java.lang.Object(ARRAY(i1294)), i1295, i543, i568, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, matching1) → 2255_0_binarySearch_Return(EOS(STATIC_2255), java.lang.Object(ARRAY(i1294)), i1295, i543, i568, java.lang.Object(ARRAY(i1294)), i1295, i1296, i1297, 0) | =(matching1, 0)
2255_0_binarySearch_Return(EOS(STATIC_2255), java.lang.Object(ARRAY(i911)), i912, i543, i568, java.lang.Object(ARRAY(i911)), i912, i913, i917, i916) → 2281_0_binarySearch_EQ(EOS(STATIC_2281), java.lang.Object(ARRAY(i911)), i912, i543, i568, i916)
2281_0_binarySearch_EQ(EOS(STATIC_2281), java.lang.Object(ARRAY(i911)), i912, i543, i568, i916) → 2282_0_binarySearch_EQ(EOS(STATIC_2282), java.lang.Object(ARRAY(i911)), i912, i543, i568, i916)
2457_0_binarySearch_Return(EOS(STATIC_2457), java.lang.Object(ARRAY(i1330)), i1331, i543, i568, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, matching1) → 2255_0_binarySearch_Return(EOS(STATIC_2255), java.lang.Object(ARRAY(i1330)), i1331, i543, i568, java.lang.Object(ARRAY(i1330)), i1331, i1332, i1333, 1) | =(matching1, 1)
2555_0_binarySearch_Return(EOS(STATIC_2555), java.lang.Object(ARRAY(i1522)), i1523, i543, i568, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1373) → 2255_0_binarySearch_Return(EOS(STATIC_2255), java.lang.Object(ARRAY(i1522)), i1523, i543, i568, java.lang.Object(ARRAY(i1522)), i1523, i1524, i1525, i1373)
R rules:
1906_0_binarySearch_LE(EOS(STATIC_1906), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1908_0_binarySearch_LE(EOS(STATIC_1908), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543)
1908_0_binarySearch_LE(EOS(STATIC_1908), java.lang.Object(ARRAY(i540)), i541, i542, i543, i542, i543) → 1910_0_binarySearch_ConstantStackPush(EOS(STATIC_1910), java.lang.Object(ARRAY(i540)), i541, i542, i543) | >(i542, i543)
1910_0_binarySearch_ConstantStackPush(EOS(STATIC_1910), java.lang.Object(ARRAY(i540)), i541, i542, i543) → 1912_0_binarySearch_Return(EOS(STATIC_1912), java.lang.Object(ARRAY(i540)), i541, i542, i543, 0)
1942_0_binarySearch_ArrayAccess(EOS(STATIC_1942), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1944_0_binarySearch_ArrayAccess(EOS(STATIC_1944), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1944_0_binarySearch_ArrayAccess(EOS(STATIC_1944), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1946_0_<init>_Load(EOS(STATIC_1946), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) | <=(i567, -1)
1945_0_binarySearch_ArrayAccess(EOS(STATIC_1945), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1948_0_binarySearch_ArrayAccess(EOS(STATIC_1948), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1946_0_<init>_Load(EOS(STATIC_1946), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1953_0_<init>_InvokeMethod(EOS(STATIC_1953), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1948_0_binarySearch_ArrayAccess(EOS(STATIC_1948), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1952_0_<init>_Load(EOS(STATIC_1952), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) | >=(i568, i540)
1952_0_<init>_Load(EOS(STATIC_1952), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1962_0_<init>_InvokeMethod(EOS(STATIC_1962), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1953_0_<init>_InvokeMethod(EOS(STATIC_1953), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1957_0_<init>_Load(EOS(STATIC_1957), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1955_0_binarySearch_NE(EOS(STATIC_1955), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i541, i541) → 1960_0_binarySearch_NE(EOS(STATIC_1960), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i541, i541)
1957_0_<init>_Load(EOS(STATIC_1957), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1969_0_<init>_InvokeMethod(EOS(STATIC_1969), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1960_0_binarySearch_NE(EOS(STATIC_1960), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, i541, i541) → 1966_0_binarySearch_ConstantStackPush(EOS(STATIC_1966), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568)
1962_0_<init>_InvokeMethod(EOS(STATIC_1962), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1967_0_<init>_Load(EOS(STATIC_1967), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1966_0_binarySearch_ConstantStackPush(EOS(STATIC_1966), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568) → 1972_0_binarySearch_Return(EOS(STATIC_1972), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, 1)
1967_0_<init>_Load(EOS(STATIC_1967), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1979_0_<init>_InvokeMethod(EOS(STATIC_1979), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1969_0_<init>_InvokeMethod(EOS(STATIC_1969), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1974_0_<init>_Load(EOS(STATIC_1974), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1974_0_<init>_Load(EOS(STATIC_1974), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1989_0_<init>_InvokeMethod(EOS(STATIC_1989), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1979_0_<init>_InvokeMethod(EOS(STATIC_1979), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1987_0_<init>_Load(EOS(STATIC_1987), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1987_0_<init>_Load(EOS(STATIC_1987), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 1998_0_<init>_InvokeMethod(EOS(STATIC_1998), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
1989_0_<init>_InvokeMethod(EOS(STATIC_1989), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 1994_0_<init>_Load(EOS(STATIC_1994), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1994_0_<init>_Load(EOS(STATIC_1994), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2001_0_<init>_InvokeMethod(EOS(STATIC_2001), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
1998_0_<init>_InvokeMethod(EOS(STATIC_1998), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2000_0_<init>_Load(EOS(STATIC_2000), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2000_0_<init>_Load(EOS(STATIC_2000), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2008_0_<init>_InvokeMethod(EOS(STATIC_2008), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2001_0_<init>_InvokeMethod(EOS(STATIC_2001), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2004_0_<init>_Load(EOS(STATIC_2004), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(EOS(STATIC_2107), java.lang.Object(ARRAY(i713)), i714, i715, i716, i567, java.lang.Object(ARRAY(i713)), i567), java.lang.Object(ARRAY(i713)), i714, i543, i568, java.lang.Object(ARRAY(i713)), i714, i715, i716) → 2159_0_binarySearch_ArrayAccess(EOS(STATIC_2159), java.lang.Object(ARRAY(i713)), i714, i543, i568, java.lang.Object(ARRAY(i713)), i714, i715, i716, java.lang.Object(ARRAY(i713)), i714, i715, i716, i567, java.lang.Object(ARRAY(i713)), i567)
2002_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(EOS(STATIC_2141), java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747), java.lang.Object(ARRAY(i751)), i752, i543, i568, java.lang.Object(ARRAY(i751)), i752, i753, i754) → 2203_0_binarySearch_ArrayAccess(EOS(STATIC_2203), java.lang.Object(ARRAY(i751)), i752, i543, i568, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747)
2002_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i786), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052) → 2299_0_binarySearch_InvokeMethod(EOS(STATIC_2299), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052, java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i786)
2002_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052), java.lang.Object(ARRAY(i1086)), i1087, i543, i568, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089) → 2337_0_binarySearch_InvokeMethod(EOS(STATIC_2337), java.lang.Object(ARRAY(i1086)), i1087, i543, i568, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052)
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315), java.lang.Object(ARRAY(i1312)), i1313, i543, i568, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315) → 2452_0_binarySearch_InvokeMethod(EOS(STATIC_2452), java.lang.Object(ARRAY(i1312)), i1313, i543, i568, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315, java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315), java.lang.Object(ARRAY(i1485)), i1486, i543, i568, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488) → 2537_0_binarySearch_InvokeMethod(EOS(STATIC_2537), java.lang.Object(ARRAY(i1485)), i1486, i543, i568, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315)
2002_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(i1504)), i1505, i1321, i1507), java.lang.Object(ARRAY(i1504)), i1505, i543, i568, java.lang.Object(ARRAY(i1504)), i1505, i1506, i1507) → 2548_0_binarySearch_InvokeMethod(EOS(STATIC_2548), java.lang.Object(ARRAY(i1504)), i1505, i543, i568, java.lang.Object(ARRAY(i1504)), i1505, i1506, i1507, java.lang.Object(ARRAY(i1504)), i1505, i1321, i1507)
2004_0_<init>_Load(EOS(STATIC_2004), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2011_0_<init>_InvokeMethod(EOS(STATIC_2011), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2008_0_<init>_InvokeMethod(EOS(STATIC_2008), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2010_0_<init>_Load(EOS(STATIC_2010), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2010_0_<init>_Load(EOS(STATIC_2010), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2025_0_<init>_InvokeMethod(EOS(STATIC_2025), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2011_0_<init>_InvokeMethod(EOS(STATIC_2011), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2021_0_<init>_Load(EOS(STATIC_2021), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2021_0_<init>_Load(EOS(STATIC_2021), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2026_0_<init>_Load(EOS(STATIC_2026), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2025_0_<init>_InvokeMethod(EOS(STATIC_2025), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2031_0_<init>_Load(EOS(STATIC_2031), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2026_0_<init>_Load(EOS(STATIC_2026), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2033_0_<init>_FieldAccess(EOS(STATIC_2033), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2031_0_<init>_Load(EOS(STATIC_2031), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2039_0_<init>_Load(EOS(STATIC_2039), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2033_0_<init>_FieldAccess(EOS(STATIC_2033), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2042_0_<init>_Load(EOS(STATIC_2042), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2039_0_<init>_Load(EOS(STATIC_2039), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2047_0_<init>_FieldAccess(EOS(STATIC_2047), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2042_0_<init>_Load(EOS(STATIC_2042), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2049_0_<init>_InvokeMethod(EOS(STATIC_2049), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2047_0_<init>_FieldAccess(EOS(STATIC_2047), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2056_0_<init>_Load(EOS(STATIC_2056), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2049_0_<init>_InvokeMethod(EOS(STATIC_2049), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2058_0_<init>_StackPop(EOS(STATIC_2058), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2056_0_<init>_Load(EOS(STATIC_2056), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2067_0_<init>_InvokeMethod(EOS(STATIC_2067), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2058_0_<init>_StackPop(EOS(STATIC_2058), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2069_0_<init>_Return(EOS(STATIC_2069), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2067_0_<init>_InvokeMethod(EOS(STATIC_2067), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2077_0_<init>_StackPop(EOS(STATIC_2077), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2069_0_<init>_Return(EOS(STATIC_2069), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2079_0_<init>_Return(EOS(STATIC_2079), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2077_0_<init>_StackPop(EOS(STATIC_2077), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2086_0_<init>_Return(EOS(STATIC_2086), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2079_0_<init>_Return(EOS(STATIC_2079), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2087_0_<init>_Return(EOS(STATIC_2087), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2086_0_<init>_Return(EOS(STATIC_2086), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2092_0_<init>_Return(EOS(STATIC_2092), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2087_0_<init>_Return(EOS(STATIC_2087), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2094_0_<init>_Return(EOS(STATIC_2094), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2092_0_<init>_Return(EOS(STATIC_2092), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2099_0_<init>_Return(EOS(STATIC_2099), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2094_0_<init>_Return(EOS(STATIC_2094), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2100_0_<init>_Return(EOS(STATIC_2100), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2099_0_<init>_Return(EOS(STATIC_2099), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2106_0_<init>_Return(EOS(STATIC_2106), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2100_0_<init>_Return(EOS(STATIC_2100), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567) → 2107_0_binarySearch_ArrayAccess(EOS(STATIC_2107), java.lang.Object(ARRAY(i540)), i541, i542, i543, i567, java.lang.Object(ARRAY(i540)), i567)
2106_0_<init>_Return(EOS(STATIC_2106), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2117_0_<init>_Return(EOS(STATIC_2117), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2117_0_<init>_Return(EOS(STATIC_2117), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568) → 2141_0_binarySearch_ArrayAccess(EOS(STATIC_2141), java.lang.Object(ARRAY(i540)), i541, i542, i543, i568, java.lang.Object(ARRAY(i540)), i568)
2159_0_binarySearch_ArrayAccess(EOS(STATIC_2159), java.lang.Object(ARRAY(i713)), i714, i543, i568, java.lang.Object(ARRAY(i713)), i714, i715, i716, java.lang.Object(ARRAY(i713)), i714, i715, i716, i567, java.lang.Object(ARRAY(i713)), i567) → 2204_0_binarySearch_ArrayAccess(EOS(STATIC_2204), java.lang.Object(ARRAY(i713)), i714, i543, i568, java.lang.Object(ARRAY(i713)), i714, i715, i716, java.lang.Object(ARRAY(i713)), i714, i715, i716, i567, java.lang.Object(ARRAY(i713)), i567)
2203_0_binarySearch_ArrayAccess(EOS(STATIC_2203), java.lang.Object(ARRAY(i751)), i752, i543, i568, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747) → 2204_0_binarySearch_ArrayAccess(EOS(STATIC_2204), java.lang.Object(ARRAY(i751)), i752, i543, i568, java.lang.Object(ARRAY(i751)), i752, i753, i754, java.lang.Object(ARRAY(i751)), i752, i753, i754, i747, java.lang.Object(ARRAY(i751)), i747)
2204_0_binarySearch_ArrayAccess(EOS(STATIC_2204), java.lang.Object(ARRAY(i781)), i782, i543, i568, java.lang.Object(ARRAY(i781)), i782, i783, i786, java.lang.Object(ARRAY(i781)), i782, i783, i786, i787, java.lang.Object(ARRAY(i781)), i787) → 2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(i781)), i782, i543, i568, java.lang.Object(ARRAY(i781)), i782, i783, i786)
2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(i781)), i782, i543, i568, java.lang.Object(ARRAY(i781)), i782, i783, i786) → 2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(i781)), i782, i543, i568, java.lang.Object(ARRAY(i781)), i782, i783, i786)
2282_0_binarySearch_EQ(EOS(STATIC_2282), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, matching1) → 2296_0_binarySearch_EQ(EOS(STATIC_2296), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, 1) | =(matching1, 1)
2296_0_binarySearch_EQ(EOS(STATIC_2296), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, matching1) → 2302_0_binarySearch_ConstantStackPush(EOS(STATIC_2302), java.lang.Object(ARRAY(i1019)), i1020, i543, i568) | &&(>(1, 0), =(matching1, 1))
2299_0_binarySearch_InvokeMethod(EOS(STATIC_2299), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052, java.lang.Object(ARRAY(i1049)), i1050, i1052, i1048, java.lang.Object(ARRAY(i1049)), i1050, i1051, i786) → 2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052)
2302_0_binarySearch_ConstantStackPush(EOS(STATIC_2302), java.lang.Object(ARRAY(i1019)), i1020, i543, i568) → 2312_0_binarySearch_Return(EOS(STATIC_2312), java.lang.Object(ARRAY(i1019)), i1020, i543, i568, 1)
2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(i1049)), i1050, i543, i568, java.lang.Object(ARRAY(i1049)), i1050, i1051, i1052)
2337_0_binarySearch_InvokeMethod(EOS(STATIC_2337), java.lang.Object(ARRAY(i1086)), i1087, i543, i568, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052) → 2299_0_binarySearch_InvokeMethod(EOS(STATIC_2299), java.lang.Object(ARRAY(i1086)), i1087, i543, i568, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1089, java.lang.Object(ARRAY(i1086)), i1087, i1089, i1085, java.lang.Object(ARRAY(i1086)), i1087, i1088, i1052)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(EOS(STATIC_1912), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, matching1), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140) → 2378_0_binarySearch_Return(EOS(STATIC_2378), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, 0) | =(matching1, 0)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(EOS(STATIC_1972), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148, i568, matching1), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148) → 2379_0_binarySearch_Return(EOS(STATIC_2379), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148, java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148, i568, 1) | =(matching1, 1)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(EOS(STATIC_2107), java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, i567, java.lang.Object(ARRAY(i1152)), i567), java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155) → 2380_0_binarySearch_ArrayAccess(EOS(STATIC_2380), java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, i567, java.lang.Object(ARRAY(i1152)), i567)
2346_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(EOS(STATIC_2141), java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, i568, java.lang.Object(ARRAY(i1159)), i568), java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162) → 2387_0_binarySearch_ArrayAccess(EOS(STATIC_2387), java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, i568, java.lang.Object(ARRAY(i1159)), i568)
2346_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(i1166)), i1167, i1169, i568, java.lang.Object(ARRAY(i1166)), i1167, i1168, i786), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169) → 2389_0_binarySearch_InvokeMethod(EOS(STATIC_2389), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169, java.lang.Object(ARRAY(i1166)), i1167, i1169, i568, java.lang.Object(ARRAY(i1166)), i1167, i1168, i786)
2346_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(i1173)), i1174, i1176, i568, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176) → 2392_0_binarySearch_InvokeMethod(EOS(STATIC_2392), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i568, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052)
2346_1_binarySearch_InvokeMethod(2312_0_binarySearch_Return(EOS(STATIC_2312), java.lang.Object(ARRAY(i1185)), i1186, i1188, i568, matching1), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188) → 2393_0_binarySearch_Return(EOS(STATIC_2393), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188, java.lang.Object(ARRAY(i1185)), i1186, i1188, i568, 1) | =(matching1, 1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return(EOS(STATIC_2394), matching1), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304) → 2450_0_binarySearch_Return(EOS(STATIC_2450), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, 0) | =(matching1, 0)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322) → 2453_0_binarySearch_InvokeMethod(EOS(STATIC_2453), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322, java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322)
2346_1_binarySearch_InvokeMethod(2405_0_binarySearch_Return(EOS(STATIC_2405), matching1), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340) → 2462_0_binarySearch_Return(EOS(STATIC_2462), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, 1) | =(matching1, 1)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(i1492)), i1493, i1495, i568, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495) → 2541_0_binarySearch_InvokeMethod(EOS(STATIC_2541), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i568, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315)
2346_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(i1511)), i1512, i1321, i1514), java.lang.Object(ARRAY(i1511)), i1512, i1513, i1514) → 2550_0_binarySearch_InvokeMethod(EOS(STATIC_2550), java.lang.Object(ARRAY(i1511)), i1512, i1513, i1514, java.lang.Object(ARRAY(i1511)), i1512, i1321, i1514)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(EOS(STATIC_2481), i1373), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532) → 2556_0_binarySearch_Return(EOS(STATIC_2556), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1373)
2378_0_binarySearch_Return(EOS(STATIC_2378), java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, java.lang.Object(ARRAY(i1137)), i1138, i1139, i1140, matching1) → 2394_0_binarySearch_Return(EOS(STATIC_2394), 0) | =(matching1, 0)
2379_0_binarySearch_Return(EOS(STATIC_2379), java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148, java.lang.Object(ARRAY(i1144)), i1145, i1146, i1148, i568, matching1) → 2396_0_binarySearch_Return(EOS(STATIC_2396), 1) | =(matching1, 1)
2380_0_binarySearch_ArrayAccess(EOS(STATIC_2380), java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, i567, java.lang.Object(ARRAY(i1152)), i567) → 2388_0_binarySearch_ArrayAccess(EOS(STATIC_2388), java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, java.lang.Object(ARRAY(i1152)), i1153, i1154, i1155, i567, java.lang.Object(ARRAY(i1152)), i567)
2387_0_binarySearch_ArrayAccess(EOS(STATIC_2387), java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, i568, java.lang.Object(ARRAY(i1159)), i568) → 2388_0_binarySearch_ArrayAccess(EOS(STATIC_2388), java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, java.lang.Object(ARRAY(i1159)), i1160, i1161, i1162, i568, java.lang.Object(ARRAY(i1159)), i568)
2388_0_binarySearch_ArrayAccess(EOS(STATIC_2388), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193, java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193, i1197, java.lang.Object(ARRAY(i1191)), i1197) → 2399_0_binarySearch_InvokeMethod(EOS(STATIC_2399), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193)
2389_0_binarySearch_InvokeMethod(EOS(STATIC_2389), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169, java.lang.Object(ARRAY(i1166)), i1167, i1169, i568, java.lang.Object(ARRAY(i1166)), i1167, i1168, i786) → 2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169)
2392_0_binarySearch_InvokeMethod(EOS(STATIC_2392), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i568, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052) → 2389_0_binarySearch_InvokeMethod(EOS(STATIC_2389), java.lang.Object(ARRAY(i1173)), i1174, i1175, i1176, java.lang.Object(ARRAY(i1173)), i1174, i1176, i568, java.lang.Object(ARRAY(i1173)), i1174, i1175, i1052)
2393_0_binarySearch_Return(EOS(STATIC_2393), java.lang.Object(ARRAY(i1185)), i1186, i1187, i1188, java.lang.Object(ARRAY(i1185)), i1186, i1188, i568, matching1) → 2405_0_binarySearch_Return(EOS(STATIC_2405), 1) | =(matching1, 1)
2394_0_binarySearch_Return(EOS(STATIC_2394), matching1) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 0) | =(matching1, 0)
2396_0_binarySearch_Return(EOS(STATIC_2396), matching1) → 2405_0_binarySearch_Return(EOS(STATIC_2405), 1) | =(matching1, 1)
2399_0_binarySearch_InvokeMethod(EOS(STATIC_2399), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193) → 2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(i1191)), i1192, i1196, i1193)
2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(i1166)), i1167, i1168, i1169)
2405_0_binarySearch_Return(EOS(STATIC_2405), matching1) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 1) | =(matching1, 1)
2450_0_binarySearch_Return(EOS(STATIC_2450), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, matching1) → 2463_0_binarySearch_Return(EOS(STATIC_2463), java.lang.Object(ARRAY(i1301)), i1302, i1303, i1304, 0) | =(matching1, 0)
2452_0_binarySearch_InvokeMethod(EOS(STATIC_2452), java.lang.Object(ARRAY(i1312)), i1313, i543, i568, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315, java.lang.Object(ARRAY(i1312)), i1313, i1168, i1315) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(i1312)), i1313, i543, i568, java.lang.Object(ARRAY(i1312)), i1313, i1314, i1315)
2453_0_binarySearch_InvokeMethod(EOS(STATIC_2453), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322, java.lang.Object(ARRAY(i1319)), i1320, i1168, i1322) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(i1319)), i1320, i1321, i1322)
2462_0_binarySearch_Return(EOS(STATIC_2462), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, matching1) → 2463_0_binarySearch_Return(EOS(STATIC_2463), java.lang.Object(ARRAY(i1337)), i1338, i1339, i1340, 1) | =(matching1, 1)
2463_0_binarySearch_Return(EOS(STATIC_2463), java.lang.Object(ARRAY(i1368)), i1369, i1374, i1370, i1373) → 2481_0_binarySearch_Return(EOS(STATIC_2481), i1373)
2537_0_binarySearch_InvokeMethod(EOS(STATIC_2537), java.lang.Object(ARRAY(i1485)), i1486, i543, i568, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315) → 2299_0_binarySearch_InvokeMethod(EOS(STATIC_2299), java.lang.Object(ARRAY(i1485)), i1486, i543, i568, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1488, java.lang.Object(ARRAY(i1485)), i1486, i1488, i1484, java.lang.Object(ARRAY(i1485)), i1486, i1487, i1315)
2541_0_binarySearch_InvokeMethod(EOS(STATIC_2541), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i568, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315) → 2389_0_binarySearch_InvokeMethod(EOS(STATIC_2389), java.lang.Object(ARRAY(i1492)), i1493, i1494, i1495, java.lang.Object(ARRAY(i1492)), i1493, i1495, i568, java.lang.Object(ARRAY(i1492)), i1493, i1494, i1315)
2548_0_binarySearch_InvokeMethod(EOS(STATIC_2548), java.lang.Object(ARRAY(i1504)), i1505, i543, i568, java.lang.Object(ARRAY(i1504)), i1505, i1506, i1507, java.lang.Object(ARRAY(i1504)), i1505, i1321, i1507) → 2452_0_binarySearch_InvokeMethod(EOS(STATIC_2452), java.lang.Object(ARRAY(i1504)), i1505, i543, i568, java.lang.Object(ARRAY(i1504)), i1505, i1506, i1507, java.lang.Object(ARRAY(i1504)), i1505, i1321, i1507)
2550_0_binarySearch_InvokeMethod(EOS(STATIC_2550), java.lang.Object(ARRAY(i1511)), i1512, i1513, i1514, java.lang.Object(ARRAY(i1511)), i1512, i1321, i1514) → 2453_0_binarySearch_InvokeMethod(EOS(STATIC_2453), java.lang.Object(ARRAY(i1511)), i1512, i1513, i1514, java.lang.Object(ARRAY(i1511)), i1512, i1321, i1514)
2556_0_binarySearch_Return(EOS(STATIC_2556), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1373) → 2463_0_binarySearch_Return(EOS(STATIC_2463), java.lang.Object(ARRAY(i1529)), i1530, i1531, i1532, i1373)

Combined rules. Obtained 7 conditional rules for P and 20 conditional rules for R.

P rules:
1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x0)), x1, x2, x3, x2) → 2002_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1), x2), java.lang.Object(ARRAY(x0)), x1, x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0)), x1, x2, -(+(x2, /(-(x3, x2), 2)), 1)) | &&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2))))
2002_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(EOS(STATIC_1912), java.lang.Object(ARRAY(x0)), x1, x2, x3, 0), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x0)), x1, +(x6, 1), x5, +(x6, 1)), java.lang.Object(ARRAY(x0)), x1, +(x6, 1), x5) | >(+(x6, 1), 0)
2002_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(EOS(STATIC_1972), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x0)), x1, arith[3], x6, arith[3]), java.lang.Object(ARRAY(x0)), x1, arith[3], x6) | FALSE
2002_1_binarySearch_InvokeMethod(2312_0_binarySearch_Return(EOS(STATIC_2312), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x7, x2) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x0)), x1, arith[3], x5, arith[3]), java.lang.Object(ARRAY(x0)), x1, arith[3], x5) | FALSE
2002_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return(EOS(STATIC_2394), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3, +(x4, 1)), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3) | >(+(x4, 1), 0)
2002_1_binarySearch_InvokeMethod(2405_0_binarySearch_Return(EOS(STATIC_2405), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x1)), x2, arith[3], x3, arith[3]), java.lang.Object(ARRAY(x1)), x2, arith[3], x3) | FALSE
2002_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(EOS(STATIC_2481), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4, java.lang.Object(ARRAY(x1)), x2, x5, x6) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(EOS(STATIC_1905), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3, +(x4, 1)), java.lang.Object(ARRAY(x1)), x2, +(x4, 1), x3) | >(+(x4, 1), 0)
R rules:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(EOS(STATIC_2107), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2002_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(EOS(STATIC_2141), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(EOS(STATIC_2402), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x3) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x2, x3), java.lang.Object(ARRAY(x0)), x1, x4, x3) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(EOS(STATIC_1912), java.lang.Object(ARRAY(x0)), x1, x2, x3, 0), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 0)
2346_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(EOS(STATIC_2239), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(EOS(STATIC_2309), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(EOS(STATIC_2474), java.lang.Object(ARRAY(x0)), x1, x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), java.lang.Object(ARRAY(x0)), x1, x4, x2) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(EOS(STATIC_2107), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(EOS(STATIC_2141), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, java.lang.Object(ARRAY(x0)), x4), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2478_0_binarySearch_InvokeMethod(EOS(STATIC_2478), java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2312_0_binarySearch_Return(EOS(STATIC_2312), java.lang.Object(ARRAY(x0)), x1, x2, x3, 1), java.lang.Object(ARRAY(x0)), x1, x5, x2) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 1)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(EOS(STATIC_1972), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, 1), java.lang.Object(ARRAY(x0)), x1, x2, x3) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return(EOS(STATIC_2394), 0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 0)
2346_1_binarySearch_InvokeMethod(2405_0_binarySearch_Return(EOS(STATIC_2405), 1), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2481_0_binarySearch_Return(EOS(STATIC_2481), 1)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(EOS(STATIC_2481), x0), java.lang.Object(ARRAY(x1)), x2, x3, x4) → 2481_0_binarySearch_Return(EOS(STATIC_2481), x0)

Filtered ground terms:

1905_0_binarySearch_Load(x1, x2, x3, x4, x5, x6) → 1905_0_binarySearch_Load(x2, x3, x4, x5, x6)
Cond_2002_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_2002_1_binarySearch_InvokeMethod2(x1, x3, x4, x5, x6, x7, x8, x9, x10)
2481_0_binarySearch_Return(x1, x2) → 2481_0_binarySearch_Return(x2)
Cond_2002_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_2002_1_binarySearch_InvokeMethod1(x1, x3, x4, x5, x6, x7, x8, x9, x10)
2394_0_binarySearch_Return(x1, x2) → 2394_0_binarySearch_Return
1912_0_binarySearch_Return(x1, x2, x3, x4, x5, x6) → 1912_0_binarySearch_Return(x2, x3, x4, x5)
Cond_1905_0_binarySearch_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_1905_0_binarySearch_Load(x1, x3, x4, x5, x6, x7)
2405_0_binarySearch_Return(x1, x2) → 2405_0_binarySearch_Return
1972_0_binarySearch_Return(x1, x2, x3, x4, x5, x6, x7) → 1972_0_binarySearch_Return(x2, x3, x4, x5, x6)
2312_0_binarySearch_Return(x1, x2, x3, x4, x5, x6) → 2312_0_binarySearch_Return(x2, x3, x4, x5)
2478_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2478_0_binarySearch_InvokeMethod(x2, x3, x4, x5)
2141_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7, x8) → 2141_0_binarySearch_ArrayAccess(x2, x3, x4, x5, x6, x7, x8)
2107_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7, x8) → 2107_0_binarySearch_ArrayAccess(x2, x3, x4, x5, x6, x7, x8)
2474_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2474_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2309_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2309_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2239_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2239_0_binarySearch_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9)
2402_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2402_0_binarySearch_InvokeMethod(x2, x3, x4, x5)

Filtered duplicate args:

1905_0_binarySearch_Load(x1, x2, x3, x4, x5) → 1905_0_binarySearch_Load(x1, x2, x4, x5)
Cond_1905_0_binarySearch_Load(x1, x2, x3, x4, x5, x6) → Cond_1905_0_binarySearch_Load(x1, x2, x3, x5, x6)
2002_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → 2002_1_binarySearch_InvokeMethod(x1, x4, x5, x6, x7, x8, x9)
Cond_2002_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_2002_1_binarySearch_InvokeMethod(x1, x2, x5, x6)
Cond_2002_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2002_1_binarySearch_InvokeMethod1(x1, x4, x5, x6, x7, x8, x9)
Cond_2002_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2002_1_binarySearch_InvokeMethod2(x1, x4, x5, x6, x7, x8, x9)
2474_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2474_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2239_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2239_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2309_0_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → 2309_0_binarySearch_InvokeMethod(x3, x4, x5, x6, x7, x8)
2107_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7) → 2107_0_binarySearch_ArrayAccess(x2, x3, x4, x6, x7)
2141_0_binarySearch_ArrayAccess(x1, x2, x3, x4, x5, x6, x7) → 2141_0_binarySearch_ArrayAccess(x2, x3, x4, x6, x7)

Filtered unneeded arguments:

Cond_1905_0_binarySearch_Load(x1, x2, x3, x4, x5) → Cond_1905_0_binarySearch_Load(x1, x2, x4, x5)
2002_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → 2002_1_binarySearch_InvokeMethod(x1, x2, x3, x4)
2346_1_binarySearch_InvokeMethod(x1, x2, x3, x4, x5) → 2346_1_binarySearch_InvokeMethod(x1)
Cond_2002_1_binarySearch_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_2002_1_binarySearch_InvokeMethod1(x1, x2, x3, x4)
Cond_2002_1_binarySearch_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_2002_1_binarySearch_InvokeMethod2(x1, x2, x3, x4)
1905_0_binarySearch_Load(x1, x2, x3, x4) → 1905_0_binarySearch_Load(x1, x3, x4)
1912_0_binarySearch_Return(x1, x2, x3, x4) → 1912_0_binarySearch_Return(x1)

Combined rules. Obtained 4 conditional rules for P and 20 conditional rules for R.

P rules:
1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x3, x2) → 2002_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0))) | &&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2))))
2002_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), x5, +(x6, 1))) | >(x6, -1)
2002_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))) | >(x4, -1)
2002_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 2346_1_binarySearch_InvokeMethod(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))) | >(x4, -1)
R rules:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2002_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2239_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2309_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2141_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2478_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2312_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2405_0_binarySearch_Return) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0)) → 2481_0_binarySearch_Return(x0)

Performed bisimulation on rules. Used the following equivalence classes: {[2402_0_binarySearch_InvokeMethod_4, 2478_0_binarySearch_InvokeMethod_4, 2312_0_binarySearch_Return_4]=2402_0_binarySearch_InvokeMethod_4, [2474_0_binarySearch_InvokeMethod_6, 2239_0_binarySearch_InvokeMethod_6, 2309_0_binarySearch_InvokeMethod_6]=2474_0_binarySearch_InvokeMethod_6, [2107_0_binarySearch_ArrayAccess_5, 2141_0_binarySearch_ArrayAccess_5]=2107_0_binarySearch_ArrayAccess_5, [2394_0_binarySearch_Return, 2405_0_binarySearch_Return]=2394_0_binarySearch_Return}

Finished conversion. Obtained 9 rules for P and 12 rules for R. System has predefined symbols.

P rules:
1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x3, x2) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2)))), java.lang.Object(ARRAY(x0)), x3, x2)
COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0)))
COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2)
2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6, -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0)))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x5, +(x6, 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4, -1), 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1)))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4, -1), 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1)))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
R rules:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0)) → 2481_0_binarySearch_Return(x0)

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0)) → 2481_0_binarySearch_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
(1): COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1]) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]), x3[1], x2[1] + x3[1] - x2[1] / 2, java.lang.Object(ARRAY(x0[1])))
(2): COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2] + x3[2] - x2[2] / 2 - 1, x2[2])
(3): 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(x6[3] > -1, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
(4): COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], x6[4] + 1)
(5): 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(x4[5] > -1, 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
(6): COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], x4[6] + 1)
(7): 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(x4[7] > -1, 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
(8): COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], x4[8] + 1)

(0) -> (1), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →^* java.lang.Object(ARRAY(x0[1]))∧x3[0] →^* x3[1]∧x2[0] →^* x2[1])

(0) -> (2), if (x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2 ∧java.lang.Object(ARRAY(x0[0])) →^* java.lang.Object(ARRAY(x0[2]))∧x3[0] →^* x3[2]∧x2[0] →^* x2[2])

(1) -> (3), if (1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →^* 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))∧x3[1] →^* x5[3]∧x2[1] + x3[1] - x2[1] / 2 →^* x6[3]∧java.lang.Object(ARRAY(x0[1])) →^* java.lang.Object(ARRAY(x0[3])))

(1) -> (5), if (1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →^* 2394_0_binarySearch_Return∧x3[1] →^* x3[5]∧x2[1] + x3[1] - x2[1] / 2 →^* x4[5]∧java.lang.Object(ARRAY(x0[1])) →^* java.lang.Object(ARRAY(x1[5])))

(1) -> (7), if (1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), x2[1] + x3[1] - x2[1] / 2 - 1, x2[1]) →^* 2481_0_binarySearch_Return(0)∧x3[1] →^* x3[7]∧x2[1] + x3[1] - x2[1] / 2 →^* x4[7]∧java.lang.Object(ARRAY(x0[1])) →^* java.lang.Object(ARRAY(x1[7])))

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(3) -> (4), if (x6[3] > -1 ∧1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))) →^* 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3] →^* x5[4]∧x6[3] →^* x6[4]∧java.lang.Object(ARRAY(x0[3])) →^* java.lang.Object(ARRAY(x0[4])))

(4) -> (0), if (java.lang.Object(ARRAY(x0[4])) →^* java.lang.Object(ARRAY(x0[0]))∧x5[4] →^* x3[0]∧x6[4] + 1 →^* x2[0])

(5) -> (6), if (x4[5] > -1 ∧x3[5] →^* x3[6]∧x4[5] →^* x4[6]∧java.lang.Object(ARRAY(x1[5])) →^* java.lang.Object(ARRAY(x1[6])))

(6) -> (0), if (java.lang.Object(ARRAY(x1[6])) →^* java.lang.Object(ARRAY(x0[0]))∧x3[6] →^* x3[0]∧x4[6] + 1 →^* x2[0])

(7) -> (8), if (x4[7] > -1 ∧x3[7] →^* x3[8]∧x4[7] →^* x4[8]∧java.lang.Object(ARRAY(x1[7])) →^* java.lang.Object(ARRAY(x1[8])))

(8) -> (0), if (java.lang.Object(ARRAY(x1[8])) →^* java.lang.Object(ARRAY(x0[0]))∧x3[8] →^* x3[0]∧x4[8] + 1 →^* x2[0])

The set Q consists of the following terms:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0)))
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x0, x1, java.lang.Object(ARRAY(x2)), x3, x4, x5), x6, x7, java.lang.Object(ARRAY(x2)))
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x0, x1, x2, java.lang.Object(ARRAY(x3)), x4), x5, x6, java.lang.Object(ARRAY(x3)))
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3))
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))))
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x0, x1, java.lang.Object(ARRAY(x2)), x3, x4, x5))
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x0, x1, x2, java.lang.Object(ARRAY(x3)), x4))
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4))
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0))

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: true Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@3c55e637 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x3, x2) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2)))), java.lang.Object(ARRAY(x0)), x3, x2) the following chains were created:

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1]) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1]))) which results in the following constraint:
(1)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x3[0]=x3[1]∧x2[0]=x2[1] ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)
We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(7)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (7) using rules (I), (II), (IV) which results in the following new constraint:
(8)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77 + (-1)Bound*bni_77] + [(-1)bni_77]x2[0] + [bni_77]x3[0] ≥ 0∧[(-1)bso_78] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)

For Pair COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0))) the following chains were created:

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1]) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1]))) which results in the following constraint:
(13)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x3[0]=x3[1]∧x2[0]=x2[1] ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1])≥2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))∧(U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥))

We simplified constraint (13) using rules (I), (II), (III) which results in the following new constraint:
(14)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0]), x3[0], +(x2[0], /(-(x3[0], x2[0]), 2)), java.lang.Object(ARRAY(x0[0])))∧(U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79 + (-1)Bound*bni_79] + [(-1)bni_79]x2[0] + [bni_79]x3[0] ≥ 0∧[2 + (-1)bso_80] + x2[0] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79] ≥ 0∧[bni_79] ≥ 0∧0 ≥ 0∧[(-1)bni_79 + (-1)Bound*bni_79] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_80] ≥ 0)

For Pair COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2) the following chains were created:

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(19)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (19) using rules (I), (II), (III) which results in the following new constraint:
(20)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81 + (-1)Bound*bni_81] + [(-1)bni_81]x2[0] + [bni_81]x3[0] ≥ 0∧[(-1)bso_82] + x3[0] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81] ≥ 0∧[bni_81] ≥ 0∧0 ≥ 0∧[(-1)bni_81 + (-1)Bound*bni_81] ≥ 0∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧[(-1)bso_82] ≥ 0)

For Pair 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6, -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1)) which results in the following constraint:
(25)    (>(x6[3], -1)=TRUE∧1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))=1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3]=x5[4]∧x6[3]=x6[4]∧java.lang.Object(ARRAY(x0[3]))=java.lang.Object(ARRAY(x0[4])) ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥))

We simplified constraint (25) using rules (I), (II), (IV) which results in the following new constraint:
(26)    (>(x6[3], -1)=TRUE ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧[(-1)bni_83 + (-1)Bound*bni_83] + [(2)bni_83]x6[3] + [bni_83]x5[3] ≥ 0∧[(-1)bso_84] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧0 ≥ 0∧[(2)bni_83] ≥ 0∧[bni_83] ≥ 0∧[(-1)bni_83 + (-1)Bound*bni_83] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_84] ≥ 0)

For Pair COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x5, +(x6, 1)) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1)), 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) which results in the following constraint:
(31)    (>(x6[3], -1)=TRUE∧1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3])))=1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4])))∧x5[3]=x5[4]∧x6[3]=x6[4]∧java.lang.Object(ARRAY(x0[3]))=java.lang.Object(ARRAY(x0[4]))∧java.lang.Object(ARRAY(x0[4]))=java.lang.Object(ARRAY(x0[0]))∧x5[4]=x3[0]∧+(x6[4], 1)=x2[0] ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥))

We simplified constraint (31) using rules (I), (II), (III), (IV) which results in the following new constraint:
(32)    (>(x6[3], -1)=TRUE ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[3])), x5[3], +(x6[3], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧[(-1)bni_85 + (-1)Bound*bni_85] + [(2)bni_85]x6[3] + [bni_85]x5[3] ≥ 0∧[(-1)bso_86] + [2]x6[3] ≥ 0)

We simplified constraint (35) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧0 ≥ 0∧[(2)bni_85] ≥ 0∧[bni_85] ≥ 0∧[(-1)bni_85 + (-1)Bound*bni_85] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_86] ≥ 0∧[1] ≥ 0)

For Pair 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4, -1), 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1)) which results in the following constraint:
(37)    (>(x4[5], -1)=TRUE∧x3[5]=x3[6]∧x4[5]=x4[6]∧java.lang.Object(ARRAY(x1[5]))=java.lang.Object(ARRAY(x1[6])) ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥))

We simplified constraint (37) using rules (I), (II), (IV) which results in the following new constraint:
(38)    (>(x4[5], -1)=TRUE ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [(2)bni_87]x4[5] + [bni_87]x3[5] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧0 ≥ 0∧[(2)bni_87] ≥ 0∧[bni_87] ≥ 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_88] ≥ 0)

For Pair COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1)) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1)), 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) which results in the following constraint:
(43)    (>(x4[5], -1)=TRUE∧x3[5]=x3[6]∧x4[5]=x4[6]∧java.lang.Object(ARRAY(x1[5]))=java.lang.Object(ARRAY(x1[6]))∧java.lang.Object(ARRAY(x1[6]))=java.lang.Object(ARRAY(x0[0]))∧x3[6]=x3[0]∧+(x4[6], 1)=x2[0] ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥))

We simplified constraint (43) using rules (I), (II), (III), (IV) which results in the following new constraint:
(44)    (>(x4[5], -1)=TRUE ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[5])), x3[5], +(x4[5], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧[(-1)bni_89 + (-1)Bound*bni_89] + [(2)bni_89]x4[5] + [bni_89]x3[5] ≥ 0∧[(-1)bso_90] + [2]x4[5] ≥ 0)

We simplified constraint (47) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧0 ≥ 0∧[(2)bni_89] ≥ 0∧[bni_89] ≥ 0∧[(-1)bni_89 + (-1)Bound*bni_89] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_90] ≥ 0∧[1] ≥ 0)

For Pair 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4, -1), 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1)) which results in the following constraint:
(49)    (>(x4[7], -1)=TRUE∧x3[7]=x3[8]∧x4[7]=x4[8]∧java.lang.Object(ARRAY(x1[7]))=java.lang.Object(ARRAY(x1[8])) ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥))

We simplified constraint (49) using rules (I), (II), (IV) which results in the following new constraint:
(50)    (>(x4[7], -1)=TRUE ⇒ 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))∧(U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [(2)bni_91]x4[7] + [bni_91]x3[7] ≥ 0∧[(-1)bso_92] ≥ 0)

We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(54)    (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧0 ≥ 0∧[(2)bni_91] ≥ 0∧[bni_91] ≥ 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_92] ≥ 0)

For Pair COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1)) the following chains were created:

We consider the chain 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))), COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1)), 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) which results in the following constraint:
(55)    (>(x4[7], -1)=TRUE∧x3[7]=x3[8]∧x4[7]=x4[8]∧java.lang.Object(ARRAY(x1[7]))=java.lang.Object(ARRAY(x1[8]))∧java.lang.Object(ARRAY(x1[8]))=java.lang.Object(ARRAY(x0[0]))∧x3[8]=x3[0]∧+(x4[8], 1)=x2[0] ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥))

We simplified constraint (55) using rules (I), (II), (III), (IV) which results in the following new constraint:
(56)    (>(x4[7], -1)=TRUE ⇒ COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥NonInfC∧COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[7])), x3[7], +(x4[7], 1))∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x4[7] + [bni_93]x3[7] ≥ 0∧[(-1)bso_94] + [2]x4[7] ≥ 0)

We simplified constraint (59) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(60)    (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧0 ≥ 0∧[(2)bni_93] ≥ 0∧[bni_93] ≥ 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_94] ≥ 0∧[1] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x3, x2) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3, x2), >(x0, +(x2, /(-(x3, x2), 2)))), <=(0, +(x2, /(-(x3, x2), 2)))), java.lang.Object(ARRAY(x0)), x3, x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(-1)bni_77] ≥ 0∧[bni_77] ≥ 0∧0 ≥ 0∧[(-1)bni_77 + (-1)Bound*bni_77] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_78] ≥ 0)
COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2), x3, +(x2, /(-(x3, x2), 2)), java.lang.Object(ARRAY(x0)))
- (0 ≥ 0 ⇒ (U^Increasing(2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))), ≥)∧[(-1)bni_79] ≥ 0∧[bni_79] ≥ 0∧0 ≥ 0∧[(-1)bni_79 + (-1)Bound*bni_79] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_80] ≥ 0)
COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x3, x2) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), -(+(x2, /(-(x3, x2), 2)), 1), x2)
- (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)bni_81] ≥ 0∧[bni_81] ≥ 0∧0 ≥ 0∧[(-1)bni_81 + (-1)Bound*bni_81] ≥ 0∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧[(-1)bso_82] ≥ 0)
2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6, -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))), ≥)∧0 ≥ 0∧[(2)bni_83] ≥ 0∧[bni_83] ≥ 0∧[(-1)bni_83 + (-1)Bound*bni_83] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_84] ≥ 0)
COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))), x5, x6, java.lang.Object(ARRAY(x0))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0)), x5, +(x6, 1))
- (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))), ≥)∧0 ≥ 0∧[(2)bni_85] ≥ 0∧[bni_85] ≥ 0∧[(-1)bni_85 + (-1)Bound*bni_85] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_86] ≥ 0∧[1] ≥ 0)
2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4, -1), 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))), ≥)∧0 ≥ 0∧[(2)bni_87] ≥ 0∧[bni_87] ≥ 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_88] ≥ 0)
COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
- (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))), ≥)∧0 ≥ 0∧[(2)bni_89] ≥ 0∧[bni_89] ≥ 0∧[(-1)bni_89 + (-1)Bound*bni_89] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_90] ≥ 0∧[1] ≥ 0)
2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4, -1), 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))), ≥)∧0 ≥ 0∧[(2)bni_91] ≥ 0∧[bni_91] ≥ 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_92] ≥ 0)
COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3, x4, java.lang.Object(ARRAY(x1))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1)), x3, +(x4, 1))
- (0 ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))), ≥)∧0 ≥ 0∧[(2)bni_93] ≥ 0∧[bni_93] ≥ 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_94] ≥ 0∧[1] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(2002_1_binarySearch_InvokeMethod(x₁, x₂, x₃, x₄)) = 0
POL(2402_0_binarySearch_InvokeMethod(x₁, x₂, x₃, x₄)) = 0
POL(java.lang.Object(x₁)) = 0
POL(ARRAY(x₁)) = 0
POL(2474_0_binarySearch_InvokeMethod(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(2107_0_binarySearch_ArrayAccess(x₁, x₂, x₃, x₄, x₅)) = 0
POL(2346_1_binarySearch_InvokeMethod(x₁)) = 0
POL(1912_0_binarySearch_Return(x₁)) = 0
POL(2481_0_binarySearch_Return(x₁)) = 0
POL(0) = 0
POL(1) = 0
POL(1972_0_binarySearch_Return(x₁, x₂, x₃, x₄, x₅)) = 0
POL(2394_0_binarySearch_Return) = 0
POL(1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₂ + [-1]x₁
POL(COND_1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃ + [-1]x₂ + [2]x₁
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = 0
POL(>(x₁, x₂)) = 0
POL(+(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(2) = 0
POL(<=(x₁, x₂)) = 0
POL(2002_1_BINARYSEARCH_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [2]x₃ + x₂ + [-1]x₁
POL(1905_0_binarySearch_Load(x₁, x₂, x₃)) = [2] + [2]x₃ + x₂
POL(COND_2002_1_BINARYSEARCH_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [2]x₄ + x₃ + [-1]x₂
POL(-1) = 0
POL(COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [2]x₄ + x₃ + [-1]x₂
POL(COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [2]x₄ + x₃ + [-1]x₂

The following pairs are in P_>:

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x3[1], x2[1]) → 2002_1_BINARYSEARCH_INVOKEMETHOD(1905_0_binarySearch_Load(java.lang.Object(ARRAY(x0[1])), -(+(x2[1], /(-(x3[1], x2[1]), 2)), 1), x2[1]), x3[1], +(x2[1], /(-(x3[1], x2[1]), 2)), java.lang.Object(ARRAY(x0[1])))

The following pairs are in P_bound:

2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))

The following pairs are in P_≥:

1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(>(x6[3], -1), 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], +(x6[4], 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(>(x4[5], -1), 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], +(x4[6], 1))
2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(>(x4[7], -1), 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], +(x4[8], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ → FALSE¹
&&(FALSE, FALSE)¹ → FALSE¹

(9) Complex Obligation (AND)

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x4, x5, java.lang.Object(ARRAY(x0)), x1, x6, x3)
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5), x6, x7, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x6, x7, java.lang.Object(ARRAY(x0)), x1, x4, x2)
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4), x5, x6, java.lang.Object(ARRAY(x0))) → 2474_0_binarySearch_InvokeMethod(x5, x6, java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x3)
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0)))) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x2, x3, java.lang.Object(ARRAY(x0)), x1, x4, x5)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x4, x2)
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x1, x2, x3, java.lang.Object(ARRAY(x0)), x4)) → 2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(0)
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return) → 2481_0_binarySearch_Return(1)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0)) → 2481_0_binarySearch_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(x3[0] >= x2[0] && x0[0] > x2[0] + x3[0] - x2[0] / 2 && 0 <= x2[0] + x3[0] - x2[0] / 2, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
(2): COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2] + x3[2] - x2[2] / 2 - 1, x2[2])
(3): 2002_1_BINARYSEARCH_INVOKEMETHOD(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD(x6[3] > -1, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[3]))), x5[3], x6[3], java.lang.Object(ARRAY(x0[3])))
(4): COND_2002_1_BINARYSEARCH_INVOKEMETHOD(TRUE, 1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0[4]))), x5[4], x6[4], java.lang.Object(ARRAY(x0[4]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[4])), x5[4], x6[4] + 1)
(5): 2002_1_BINARYSEARCH_INVOKEMETHOD(2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(x4[5] > -1, 2394_0_binarySearch_Return, x3[5], x4[5], java.lang.Object(ARRAY(x1[5])))
(6): COND_2002_1_BINARYSEARCH_INVOKEMETHOD1(TRUE, 2394_0_binarySearch_Return, x3[6], x4[6], java.lang.Object(ARRAY(x1[6]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[6])), x3[6], x4[6] + 1)
(7): 2002_1_BINARYSEARCH_INVOKEMETHOD(2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7]))) → COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(x4[7] > -1, 2481_0_binarySearch_Return(0), x3[7], x4[7], java.lang.Object(ARRAY(x1[7])))
(8): COND_2002_1_BINARYSEARCH_INVOKEMETHOD2(TRUE, 2481_0_binarySearch_Return(0), x3[8], x4[8], java.lang.Object(ARRAY(x1[8]))) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x1[8])), x3[8], x4[8] + 1)

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(4) -> (0), if (java.lang.Object(ARRAY(x0[4])) →^* java.lang.Object(ARRAY(x0[0]))∧x5[4] →^* x3[0]∧x6[4] + 1 →^* x2[0])

(6) -> (0), if (java.lang.Object(ARRAY(x1[6])) →^* java.lang.Object(ARRAY(x0[0]))∧x3[6] →^* x3[0]∧x4[6] + 1 →^* x2[0])

(8) -> (0), if (java.lang.Object(ARRAY(x1[8])) →^* java.lang.Object(ARRAY(x0[0]))∧x3[8] →^* x3[0]∧x4[8] + 1 →^* x2[0])

(5) -> (6), if (x4[5] > -1 ∧x3[5] →^* x3[6]∧x4[5] →^* x4[6]∧java.lang.Object(ARRAY(x1[5])) →^* java.lang.Object(ARRAY(x1[6])))

(7) -> (8), if (x4[7] > -1 ∧x3[7] →^* x3[8]∧x4[7] →^* x4[8]∧java.lang.Object(ARRAY(x1[7])) →^* java.lang.Object(ARRAY(x1[8])))

(11) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(13) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@2cefe7f3 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) the following chains were created:

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(1)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (1) using rules (I), (II), (III), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(8)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_GCD) which results in the following new constraint:
(9)    (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

For Pair 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) the following chains were created:

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(10)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (10) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(11)    (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (11) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(12)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (12) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(13)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (13) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(14)    (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(15)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(16)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(17)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_GCD) which results in the following new constraint:
(18)    (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
- (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
- (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃, x₄)) = [2] + [-1]x₄ + x₃ + x₂ + x₁
POL(java.lang.Object(x₁)) = [-1] + x₁
POL(ARRAY(x₁)) = [-1]
POL(1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃)) = [-1]x₃ + x₂ + [-1]x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(1) = [1]
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(0) = 0

Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(Term^CSAR-Mode @ Context)

POL(/(x₁, 2)¹ @ {+_2/1}) = max{x₁, [-1]x₁} + [-1]
POL(/(x₁, 2)^-1 @ {+_2/1}) = max{x₁, [-1]x₁} + [-1]
POL(/(x₁, 2)¹ @ {1905_0_BINARYSEARCH_LOAD_3/1, -_2/0, +_2/1}) = max{x₁, [-1]x₁} + [-1]

The following pairs are in P_>:

1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])

The following pairs are in P_bound:

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])

The following pairs are in P_≥:

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

/¹ →
&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
&&(FALSE, FALSE)¹ → FALSE¹

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2] + x3[2] - x2[2] / 2 - 1, x2[2])

The set Q consists of the following terms:
2002_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3), x4, x5, java.lang.Object(ARRAY(x0)))
2002_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x0, x1, java.lang.Object(ARRAY(x2)), x3, x4, x5), x6, x7, java.lang.Object(ARRAY(x2)))
2002_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x0, x1, x2, java.lang.Object(ARRAY(x3)), x4), x5, x6, java.lang.Object(ARRAY(x3)))
2346_1_binarySearch_InvokeMethod(2402_0_binarySearch_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x3))
2346_1_binarySearch_InvokeMethod(1912_0_binarySearch_Return(java.lang.Object(ARRAY(x0))))
2346_1_binarySearch_InvokeMethod(2474_0_binarySearch_InvokeMethod(x0, x1, java.lang.Object(ARRAY(x2)), x3, x4, x5))
2346_1_binarySearch_InvokeMethod(2107_0_binarySearch_ArrayAccess(x0, x1, x2, java.lang.Object(ARRAY(x3)), x4))
2346_1_binarySearch_InvokeMethod(1972_0_binarySearch_Return(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4))
2346_1_binarySearch_InvokeMethod(2394_0_binarySearch_Return)
2346_1_binarySearch_InvokeMethod(2481_0_binarySearch_Return(x0))

(17) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(18) TRUE

(19) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(20) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

(2) -> (0), if (java.lang.Object(ARRAY(x0[2])) →^* java.lang.Object(ARRAY(x0[0]))∧x2[2] + x3[2] - x2[2] / 2 - 1 →^* x3[0]∧x2[2] →^* x2[0])

(24) IDPNonInfProof (SOUND transformation)

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(1)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (1) using rules (I), (II), (III), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), -(+(x2[0], /(-(x3[0], x2[0]), 2)), 1), x2[0])∧(U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] + [-1]x2[0] + x3[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x2[0] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[bni_23 + (-1)Bound*bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(8)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23 + bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_GCD) which results in the following new constraint:
(9)    (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23 + bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)

We consider the chain 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]), COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2]) which results in the following constraint:
(10)    (&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2))))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[2]))∧x3[0]=x3[2]∧x2[0]=x2[2] ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (10) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(11)    (<=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE∧>=(x3[0], x2[0])=TRUE∧>(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))=TRUE ⇒ 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥NonInfC∧1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])≥COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])∧(U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥))

We simplified constraint (11) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(12)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (12) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(13)    (x2[0] + [-1] + max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0∧x3[0] + [-1]x2[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]max{x3[0] + [-1]x2[0], [-1]x3[0] + x2[0]} ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (13) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(14)    (x3[0] + [-1]x2[0] ≥ 0∧[2]x3[0] + [-2]x2[0] ≥ 0∧[-1] + x3[0] ≥ 0∧x0[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[0] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(15)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x2[0] + [-1] + x3[0] ≥ 0∧x0[0] + [-1]x2[0] + [-1]x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(16)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(17)    (x3[0] ≥ 0∧[2]x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_GCD) which results in the following new constraint:
(18)    (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
- (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])), ≥)∧[(-1)Bound*bni_23 + bni_23] + [bni_23]x3[0] ≥ 0∧[(-1)bso_27] ≥ 0)
1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])
- (x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0 ⇒ (U^Increasing(COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x3[0] ≥ 0∧[2 + (-1)bso_29] ≥ 0)

POL(TRUE) = [3]
POL(FALSE) = [3]
POL(COND_1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃, x₄)) = [-1]x₄ + x₃ + [-1]x₂
POL(java.lang.Object(x₁)) = [-1]
POL(ARRAY(x₁)) = [-1] + [-1]x₁
POL(1905_0_BINARYSEARCH_LOAD(x₁, x₂, x₃)) = [2] + [-1]x₃ + x₂ + [-1]x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(1) = [1]
POL(&&(x₁, x₂)) = [1]
POL(>=(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(0) = 0

Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(Term^CSAR-Mode @ Context)

POL(/(x₁, 2)¹ @ {+_2/1}) = max{x₁, [-1]x₁} + [-1]
POL(/(x₁, 2)^-1 @ {+_2/1}) = max{x₁, [-1]x₁} + [-1]
POL(/(x₁, 2)¹ @ {1905_0_BINARYSEARCH_LOAD_3/1, -_2/0, +_2/1}) = max{x₁, [-1]x₁} + [-1]

The following pairs are in P_>:

1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])

The following pairs are in P_bound:

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])
1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[0])), x3[0], x2[0]) → COND_1905_0_BINARYSEARCH_LOAD(&&(&&(>=(x3[0], x2[0]), >(x0[0], +(x2[0], /(-(x3[0], x2[0]), 2)))), <=(0, +(x2[0], /(-(x3[0], x2[0]), 2)))), java.lang.Object(ARRAY(x0[0])), x3[0], x2[0])

The following pairs are in P_≥:

COND_1905_0_BINARYSEARCH_LOAD(TRUE, java.lang.Object(ARRAY(x0[2])), x3[2], x2[2]) → 1905_0_BINARYSEARCH_LOAD(java.lang.Object(ARRAY(x0[2])), -(+(x2[2], /(-(x3[2], x2[2]), 2)), 1), x2[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

/¹ →
TRUE¹ → &&(TRUE, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(25) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(26) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(27) TRUE

(28) 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: UsedFieldsAnalysis

(29) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 30 rules for P and 0 rules for R.

P rules:
1247_0_createArray_Load(EOS(STATIC_1247), java.lang.Object(ARRAY(i79)), i316, i316) → 1254_0_createArray_ArrayLength(EOS(STATIC_1254), java.lang.Object(ARRAY(i79)), i316, i316, java.lang.Object(ARRAY(i79)))
1254_0_createArray_ArrayLength(EOS(STATIC_1254), java.lang.Object(ARRAY(i79)), i316, i316, java.lang.Object(ARRAY(i79))) → 1257_0_createArray_GE(EOS(STATIC_1257), java.lang.Object(ARRAY(i79)), i316, i316, i79) | >=(i79, 0)
1257_0_createArray_GE(EOS(STATIC_1257), java.lang.Object(ARRAY(i79)), i316, i316, i79) → 1265_0_createArray_GE(EOS(STATIC_1265), java.lang.Object(ARRAY(i79)), i316, i316, i79)
1265_0_createArray_GE(EOS(STATIC_1265), java.lang.Object(ARRAY(i79)), i316, i316, i79) → 1275_0_createArray_Load(EOS(STATIC_1275), java.lang.Object(ARRAY(i79)), i316) | <(i316, i79)
1275_0_createArray_Load(EOS(STATIC_1275), java.lang.Object(ARRAY(i79)), i316) → 1282_0_createArray_Load(EOS(STATIC_1282), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)))
1282_0_createArray_Load(EOS(STATIC_1282), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79))) → 1290_0_createArray_InvokeMethod(EOS(STATIC_1290), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316)
1290_0_createArray_InvokeMethod(EOS(STATIC_1290), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316) → 1299_0_random_FieldAccess(EOS(STATIC_1299), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316)
1299_0_random_FieldAccess(EOS(STATIC_1299), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316) → 1315_0_random_FieldAccess(EOS(STATIC_1315), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77)))
1315_0_random_FieldAccess(EOS(STATIC_1315), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77))) → 1323_0_random_ArrayAccess(EOS(STATIC_1323), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77)), i315)
1323_0_random_ArrayAccess(EOS(STATIC_1323), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77)), i315) → 1330_0_random_ArrayAccess(EOS(STATIC_1330), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77)), i315)
1330_0_random_ArrayAccess(EOS(STATIC_1330), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i77)), i315) → 1340_0_random_Store(EOS(STATIC_1340), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383) | <(i315, i77)
1340_0_random_Store(EOS(STATIC_1340), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383) → 1348_0_random_FieldAccess(EOS(STATIC_1348), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383)
1348_0_random_FieldAccess(EOS(STATIC_1348), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383) → 1355_0_random_ConstantStackPush(EOS(STATIC_1355), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, i315)
1355_0_random_ConstantStackPush(EOS(STATIC_1355), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, i315) → 1362_0_random_IntArithmetic(EOS(STATIC_1362), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, i315, 1)
1362_0_random_IntArithmetic(EOS(STATIC_1362), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, i315, matching1) → 1368_0_random_FieldAccess(EOS(STATIC_1368), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, +(i315, 1)) | &&(>(i315, 0), =(matching1, 1))
1368_0_random_FieldAccess(EOS(STATIC_1368), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383, i329) → 1374_0_random_Load(EOS(STATIC_1374), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383)
1374_0_random_Load(EOS(STATIC_1374), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383) → 1384_0_random_InvokeMethod(EOS(STATIC_1384), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, o383)
1384_0_random_InvokeMethod(EOS(STATIC_1384), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub)) → 1391_0_random_InvokeMethod(EOS(STATIC_1391), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub))
1391_0_random_InvokeMethod(EOS(STATIC_1391), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub)) → 1396_0_length_Load(EOS(STATIC_1396), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub), java.lang.Object(o411sub))
1396_0_length_Load(EOS(STATIC_1396), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub), java.lang.Object(o411sub)) → 1411_0_length_FieldAccess(EOS(STATIC_1411), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(o411sub), java.lang.Object(o411sub))
1411_0_length_FieldAccess(EOS(STATIC_1411), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) → 1414_0_length_FieldAccess(EOS(STATIC_1414), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) | &&(>=(i361, 0), >=(i362, 0))
1414_0_length_FieldAccess(EOS(STATIC_1414), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(java.lang.String(o420sub, i361)), java.lang.Object(java.lang.String(o420sub, i361))) → 1424_0_length_Return(EOS(STATIC_1424), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(java.lang.String(o420sub, i361)))
1424_0_length_Return(EOS(STATIC_1424), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316, java.lang.Object(java.lang.String(o420sub, i361))) → 1431_0_random_Return(EOS(STATIC_1431), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316)
1431_0_random_Return(EOS(STATIC_1431), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316) → 1437_0_createArray_ArrayAccess(EOS(STATIC_1437), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316)
1437_0_createArray_ArrayAccess(EOS(STATIC_1437), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316) → 1447_0_createArray_ArrayAccess(EOS(STATIC_1447), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316)
1447_0_createArray_ArrayAccess(EOS(STATIC_1447), java.lang.Object(ARRAY(i79)), i316, java.lang.Object(ARRAY(i79)), i316) → 1459_0_createArray_Inc(EOS(STATIC_1459), java.lang.Object(ARRAY(i79)), i316) | <(i316, i79)
1459_0_createArray_Inc(EOS(STATIC_1459), java.lang.Object(ARRAY(i79)), i316) → 1471_0_createArray_JMP(EOS(STATIC_1471), java.lang.Object(ARRAY(i79)), +(i316, 1)) | >=(i316, 0)
1471_0_createArray_JMP(EOS(STATIC_1471), java.lang.Object(ARRAY(i79)), i376) → 1483_0_createArray_Load(EOS(STATIC_1483), java.lang.Object(ARRAY(i79)), i376)
1483_0_createArray_Load(EOS(STATIC_1483), java.lang.Object(ARRAY(i79)), i376) → 1239_0_createArray_Load(EOS(STATIC_1239), java.lang.Object(ARRAY(i79)), i376)
1239_0_createArray_Load(EOS(STATIC_1239), java.lang.Object(ARRAY(i79)), i316) → 1247_0_createArray_Load(EOS(STATIC_1247), java.lang.Object(ARRAY(i79)), i316, i316)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

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

Filtered ground terms:

1247_0_createArray_Load(x1, x2, x3, x4) → 1247_0_createArray_Load(x2, x3, x4)
EOS(x1) → EOS
Cond_1247_0_createArray_Load(x1, x2, x3, x4, x5) → Cond_1247_0_createArray_Load(x1, x3, x4, x5)

Filtered duplicate args:

1247_0_createArray_Load(x1, x2, x3) → 1247_0_createArray_Load(x1, x3)
Cond_1247_0_createArray_Load(x1, x2, x3, x4) → Cond_1247_0_createArray_Load(x1, x2, x4)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
1247_0_createArray_Load(java.lang.Object(ARRAY(x0)), x1) → 1247_0_createArray_Load(java.lang.Object(ARRAY(x0)), +(x1, 1)) | &&(&&(>(x1, -1), <(x1, x0)), >(x0, -1))
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

P rules:
1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1)
COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1))
R rules:

(30) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1247_0_CREATEARRAY_LOAD(x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1, java.lang.Object(ARRAY(x0[0])), x1[0])
(1): COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), x1[1] + 1)

(0) -> (1), if (x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1 ∧java.lang.Object(ARRAY(x0[0])) →^* java.lang.Object(ARRAY(x0[1]))∧x1[0] →^* x1[1])

(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →^* java.lang.Object(ARRAY(x0[0]))∧x1[1] + 1 →^* x1[0])

The set Q is empty.

(31) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@5e19b12e Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1) the following chains were created:

We consider the chain 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0]), COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1)) which results in the following constraint:
(1)    (&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x1[0]=x1[1] ⇒ 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], -1)=TRUE∧>(x1[0], -1)=TRUE∧<(x1[0], x0[0])=TRUE ⇒ 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    ([1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

For Pair COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1)) the following chains were created:

We consider the chain COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1)) which results in the following constraint:
(7)    (COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥NonInfC∧COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))∧(U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1)
- ([1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1))
- ((U^Increasing(1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(1247_0_CREATEARRAY_LOAD(x₁, x₂)) = [-1] + [-1]x₂ + x₁
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁)) = x₁
POL(COND_1247_0_CREATEARRAY_LOAD(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]

The following pairs are in P_>:

COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))

The following pairs are in P_bound:

1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])

The following pairs are in P_≥:

1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_1247_0_CREATEARRAY_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])

There are no usable rules.

(32) Complex Obligation (AND)

(33) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(34) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(35) TRUE

(36) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_1247_0_CREATEARRAY_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 1247_0_CREATEARRAY_LOAD(java.lang.Object(ARRAY(x0[1])), x1[1] + 1)

The set Q is empty.

(37) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Complex Obligation (AND)

(10) Obligation:

(11) IDependencyGraphProof (EQUIVALENT transformation)

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Obligation:

(17) IDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) IDependencyGraphProof (EQUIVALENT transformation)

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) IDPNonInfProof (SOUND transformation)

(25) Obligation:

(26) IDependencyGraphProof (EQUIVALENT transformation)

(27) TRUE

(28) Obligation:

(29) SCCToIDPv1Proof (SOUND transformation)

(30) Obligation:

(31) IDPNonInfProof (SOUND transformation)

(32) Complex Obligation (AND)

(33) Obligation:

(34) IDependencyGraphProof (EQUIVALENT transformation)

(35) TRUE

(36) Obligation:

(37) IDependencyGraphProof (EQUIVALENT transformation)

(38) TRUE