from englishVocabulary import *


def binarySearch (data, x):
    lower = -1
    upper = len(data)  
    # Schleifeninvariante
    # data[lower] <= x < data[upper]  (*)
    #
    # Gilt das? Nun ja,
    # wir tun mal so, als sei data[-1] = -infinity
    # und data[n] = +infinity.
    # Mit dieser Konvention stimmt Bedingung (*)
    # zu diesem Zeitpunkt
    while (upper - lower > 1):
        lookup = (upper + lower) // 2
        if (data[lookup] <= x):
            lower = lookup 
            # dann gilt data[lower] = data[lookup] <= x
            # und (*) stimmt immer noch
        else:
            # jetzt gilt also data[lookup] > x weil wir im "Else" sind
            upper = lookup 
            # daher gilt jetzt data[upper] = data[lookup] > x
            # also gilt (*) immer noch.
    return lower
    # jetzt gilt also
    # lower = upper-1. Warum?
    # upper - lower ist entweder 0 oder 1. Denn falls groesser
    # waere while nicht zu ende.
    # Negativ kann's nicht sein weil upper >= lower immer gilt
    # Kann upper = lower sein?
    # Naja, wir wissen data[lower] <= x < data[upper]
    # Also data[lower] < data[upper]
    # also insbesondere !=, und damit lower != upper