docs: 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