docs: def dfa_minimization(dfa: dict) -> dict:
      """ Returns the minimization of the DFA in input through a
      greatest fix-point method.
  
      Given a completed DFA :math:`A = (Σ, S, s_0 , ρ, F )` there
      exists a single minimal DFA :math:`A_m`
      which is equivalent to A, i.e. reads the same language
      :math:`L(A) = L(A_m)` and with a minimal number of states.
      To construct such a DFA we exploit bisimulation as a suitable
      equivalence relation between states.
  
      A bisimulation relation :math:`E ∈ S × S` is a relation
      between states that satisfies the following condition:
      if :math:`(s, t) ∈ E` then:
  
       • s ∈ F iff t ∈ F;
       • For all :math:`(s_X,a)` such that :math:`ρ(s, a) = s_X`,
         there exists :math:`t_X` such that :math:`ρ(t, a) = t_X`
         and :math:`(s_X , t_X ) ∈ E`;
       • For all :math:`(t_X,a)` such that :math:`ρ(t, a) = t_X` ,
         there exists :math:`s_X` such that :math:`ρ(s, a) = s_X`
         and :math:`(s_X , t_X ) ∈ E`.
  
      :param dict dfa: input DFA.
      :return: *(dict)* representing the minimized DFA.
      """
      dfa = dfa_completion(deepcopy(dfa))
  
      ################################################################
      ### Greatest-fixpoint
  
      z_current = set()
      z_next = set()
  
      # First bisimulation condition check (can be done just once)
      # s ∈ F iff t ∈ F
      for state_s in dfa['states']:
          for state_t in dfa['states']:
              if (
                              state_s in dfa['accepting_states']
                      and state_t in dfa['accepting_states']
              ) or (
                              state_s not in dfa['accepting_states']
                      and state_t not in dfa['accepting_states']
              ):
                  z_next.add((state_s, state_t))
  
      # Second and third condition of bisimularity check
      while z_current != z_next:
          z_current = z_next
          z_next = z_current.copy()
          for (state_1, state_2) in z_current:
              # for all s0,a s.t. ρ(s, a) = s_0 , there exists t 0
              # s.t. ρ(t, a) = t 0 and (s_0 , t 0 ) ∈ Z i ;
              for a in dfa['alphabet']:
                  if (state_1, a) in dfa['transitions'] \
                          and (state_2, a) in dfa['transitions']:
                      if (
                              dfa['transitions'][state_1, a],
                              dfa['transitions'][state_2, a]
                      ) not in z_current:
                          z_next.remove((state_1, state_2))
                          break
                  else:
                      # action a not possible in state element[0]
                      # or element[1]
                      z_next.remove((state_1, state_2))
                      break
  
      ################################################################
      ### Equivalence Sets
  
      equivalence = dict()
      for (state_1, state_2) in z_current:
          equivalence.setdefault(state_1, set()).add(state_2)
  
      ################################################################
      ### Minimal DFA construction
  
      dfa_min = {
          'alphabet': dfa['alphabet'].copy(),
          'states': set(),
          'initial_state': dfa['initial_state'],
          'accepting_states': set(),
          'transitions': dfa['transitions'].copy()
      }
  
      # select one element for each equivalence set
      for equivalence_set in equivalence.values():
          if dfa_min['states'].isdisjoint(equivalence_set):
              e = equivalence_set.pop()
              dfa_min['states'].add(e)  # TODO highlight this instruction
              equivalence_set.add(e)
  
      dfa_min['accepting_states'] = \
          dfa_min['states'].intersection(dfa['accepting_states'])
  
      for t in dfa['transitions']:
          if t[0] not in dfa_min['states']:
              dfa_min['transitions'].pop(t)
          elif dfa['transitions'][t] not in dfa_min['states']:
              dfa_min['transitions'][t] = \
                  equivalence[dfa['transitions'][t]]. \
                      intersection(dfa_min['states']).pop()
  
      return dfa_min