LGformel.py

def getBin(x):
    return list(reversed([int(i) for i in bin(x)[2:]]))

def getExtendedBin(x, n):
    bin = getBin(x)
    binLen = len(bin)
    for i in range(binLen, n):
        bin += [0]
    return bin

def testGet(n, c):
    return [c + str(i) for i in range(n)]

def getW(a, b, max):
    #n = 4
    #aL, bL = testGet(n, 'a'), testGet(n, 'b')
    #aL, bL = getBin(a), getBin(b)
    aLLen = len(getBin(max))
    #aL = getBin(a, aLLen)
    aL = getExtendedBin(a, aLLen)
    #aL = getBin(a)
    #aLLen = len(aL)
    bL = getExtendedBin(b, aLLen)
    res = []
    #return [aL[i] + bL[i] for i in range(aLLen)]
    for i in range(aLLen):
        res += [aL[i]]
        res += [bL[i]]
    return res

def nextState(currentState, j):
    # I will name (p) state by 6
    #l = [[0, 1, 0], [0, 2, 1], [1, 0, 0], [1, 6, 1], [2, 6, 0], [2, 3, 1], [3, 4, 0], [3, 5, 1], [4, 6, 0], [4, 3, 1], [5, 3, 0], [5, 6, 1], [6, 6, 0], [6, 6, 1]] # src, dest, transition
    l = [[1, 0], [2, 1], [0, 0], [6, 1], [6, 0], [3, 1], [4, 0], [5, 1], [6, 0], [3, 1], [3, 0], [6, 1], [6, 0], [6, 1]] # dest, transition
    lLen = len(l)
    for lIndex in range(lLen):
        src = lIndex // 2
        #src, dest, transition = l[lIndex]
        dest, transition = l[lIndex]
        if src == currentState and transition == j:
            return dest
    print("THIS SHOULDN'T OCCUR")

def automate(a, b, max):
    w = getW(a, b, max)
    print(w)
    currentState = 0
    wLen = len(w)
    for wIndex in range(wLen):
        wi = w[wIndex]
        currentState = nextState(currentState, wi)
    return currentState in [0, 3]

n = 0
while True:
    print("Working on n=" + str(n))
    max = 2**(n)-1 # used to be n+1 - THIS DOESN'T MAKE EXAUSTIVE
    for a in range(0, max):
        for b in range(0, max):
            first = (a + b) % (2**n) == 0
            second = automate(a, b, max)
            #if (first and not second) or (second and not first):
            if first != second:
                print("Contre-exemple: " + str(a) + " " + str(b) + " " + str(first) + " " + str(second))
    n += 1
    #if n == 3:
    #    break