# fórmulas serão listas: primeiro o conectivo principal (se houver) depois a subfórmula principal da esquerda, depois (se houve) a da direita

# exemplo:
fi = ("conj", ("Hugo está de camiseta",), ("neg", ("Hugo está de fraque",)))

def é_atômica(fórmula):
    return len(fórmula) == 1

def é_negação(fórmula):
    return (not é_atômica(fórmula)) and fórmula[0] == "neg"

def sub(fórmula):
    if é_atômica(fórmula):
        return {fórmula}
    if é_negação(fórmula):
        return {fórmula}.union(sub(fórmula[1]))
    return {fórmula}.union(sub(fórmula[1])).union(sub(fórmula[2]))

def compr(fórmula):
    if é_atômica(fórmula):
        return 1
    if é_negação(fórmula):
        return 3 + compr(fórmula[1])
    return 3 + compr(fórmula[1]) + compr(fórmula[2])

def ocorre(letra, fórmula, posição):
    if é_atômica(fórmula):
        return fórmula == (letra,) and posição == 0

    if é_negação(fórmula):
        return ocorre(letra, fórmula[1], posição - 2)

    return ocorre(letra,fórmula[1],posição - 1) or ocorre(letra, fórmula[2], posição - 2 - compr(fórmula[1]))

def humana(fórmula):
    """Retorna uma string legível representando a fórmula"""
    if é_atômica(fórmula):
        return fórmula[0]
    if é_negação(fórmula):
        return f"(¬ {humana(fórmula[1])})"
    match fórmula[0]:
        case "conj": conectivo_humana = "∧"
        case "disj": conectivo_humana = "∨"
        case "impl": conectivo_humana = "⟶"
        case "biimpl": conectivo_humana = "⟷"
    return f"({humana(fórmula[1])} {conectivo_humana} {humana(fórmula[2])})"