Returns a NFA that reads the language recognized by the
    input DFA where all the symbols in **symbols_to_project**
    are projected out of the alphabet.

    Projection in a DFA is the operation that existentially
    removes from a word all occurrence of symbols in a set X.
    Given a dfa :math:`A = (Σ, S, s_0 , ρ, F )`, we can define an
    NFA :math:`A_{πX}`
    that recognizes the language :math:`πX(L(A))` as

    :math:`A_{πX}= ( Σ−X, S, S_0 , ρ_X , F )`

    where

    • :math:`S_0 = \{s | (s_0 , s) ∈ ε_X \}`
    • :math:`(s,a,s_y ) ∈ ρ_X` iff there exist :math:`(t, t_y)` s.t.
      :math:`(s,t) ∈ ε_X , t_y = ρ(t,a)` and :math:`(t_y , s_y )
      ∈ ε_X`

    :param dict dfa: input DFA;
    :param set symbols_to_remove: set containing symbols ∈ dfa[
           'alphabet'] to be projected out from DFA.
    :return: *(dict)* representing a NFA.

def dfa_projection(dfa: dict, symbols_to_remove: set) -> dict:
    """ Returns a NFA that reads the language recognized by the
    input DFA where all the symbols in **symbols_to_project**
    are projected out of the alphabet.

    Projection in a DFA is the operation that existentially
    removes from a word all occurrence of symbols in a set X.
    Given a dfa :math:`A = (Σ, S, s_0 , ρ, F )`, we can define an
    NFA :math:`A_{πX}`
    that recognizes the language :math:`πX(L(A))` as

    :math:`A_{πX}= ( Σ−X, S, S_0 , ρ_X , F )`

    where

    • :math:`S_0 = \{s | (s_0 , s) ∈ ε_X \}`
    • :math:`(s,a,s_y ) ∈ ρ_X` iff there exist :math:`(t, t_y)` s.t.
      :math:`(s,t) ∈ ε_X , t_y = ρ(t,a)` and :math:`(t_y , s_y )
      ∈ ε_X`

    :param dict dfa: input DFA;
    :param set symbols_to_remove: set containing symbols ∈ dfa[
           'alphabet'] to be projected out from DFA.
    :return: *(dict)* representing a NFA.
    """
    nfa = {
        'alphabet': dfa['alphabet'].difference(symbols_to_remove),
        'states': dfa['states'].copy(),
        'initial_states': {dfa['initial_state']},
        'accepting_states': dfa['accepting_states'].copy(),
        'transitions': dict()
    }

    current_nfa_transitions = None
    current_e_x = None
    e_x = dict()  # equivalence relation dictionary

    # while no more changes are possible
    while current_nfa_transitions != nfa['transitions'] or current_e_x != e_x:
        current_nfa_transitions = nfa['transitions'].copy()
        current_e_x = deepcopy(e_x)
        for (state, a) in dfa['transitions']:
            next_state = dfa['transitions'][state, a]
            if a in symbols_to_remove:
                # mark next_state as equivalent to state
                e_x.setdefault(state, set()).add(next_state)

                app_set = set()
                for equivalent in e_x[state]:
                    # mark states equivalent to next_states also to state
                    if equivalent in e_x:
                        app_set.update(e_x[equivalent])
                    # add all transitions of equivalent states to state
                    for act in nfa['alphabet']:
                        if (equivalent, act) in dfa['transitions']:
                            equivalent_next = dfa['transitions'][
                                equivalent, act]
                            nfa['transitions'].setdefault(
                                (state, act), set()).add(equivalent_next)
                            # if equivalent_next has equivalent states
                            if equivalent_next in e_x:
                                # the transition leads also to these states
                                nfa['transitions'][state, act].update(
                                    e_x[equivalent_next])
                e_x[state].update(app_set)
            else:
                # add the transition to the NFA
                nfa['transitions'].setdefault((state, a), set()).add(
                    next_state)
                # if next_state has equivalent states
                if next_state in e_x:
                    # the same transition arrive also to all these other states
                    nfa['transitions'][state, a].update(e_x[next_state])

    # Add all state equivalent to the initial one to NFA initial states set
    if dfa['initial_state'] in e_x:
        nfa['initial_states'].update(e_x[dfa['initial_state']])

    return nfa