23 The key observation is that our version of the Sulzmann and Lu's algorithm

    23 The key observation is that our version of the Sulzmann and Lu's algorithm

    24 \cite{Sulzmann2014} represents 

    24 \cite{Sulzmann2014} represents 

    25 derivative terms in a way that allows efficient de-duplication,

    25 derivative terms in a way that allows efficient de-duplication,

    26 and we do not make use of an equivalence checker that exploits the ACI-equivalent

    26 and we do not make use of an equivalence checker that exploits the ACI-equivalent

    27 terms.

    27 terms.

    28 

    29 

    29 Central to this thesis is the work by Sulzmann and Lu \cite{Sulzmann2014}.

    30 Central to this thesis is the work by Sulzmann and Lu \cite{Sulzmann2014}.

    30 They first introduced the elegant and simple idea of injection-based lexing

    31 They first introduced the elegant and simple idea of injection-based lexing

    31 and bit-coded lexing.

    32 and bit-coded lexing.

    32 In a follow-up work \cite{Sulzmann2014b}, Sulzmann and Steenhoven

    33 In a follow-up work \cite{Sulzmann2014b}, Sulzmann and Steenhoven