\BOOKMARK [0][-]{chapter.1}{Einleitung}{}% 1 \BOOKMARK [1][-]{section.1.1}{Eins - Eins}{chapter.1}% 2 \BOOKMARK [2][-]{subsection.1.1.1}{Eins - Eins - Eins}{section.1.1}% 3 \BOOKMARK [0][-]{chapter.2}{Z3 theorem solver}{}% 4 \BOOKMARK [1][-]{section.2.1}{Z3 basics}{chapter.2}% 5 \BOOKMARK [0][-]{chapter.3}{Elimination of internal variables of automatons that including non-linear parts}{}% 6 \BOOKMARK [1][-]{section.3.1}{Exemplified workflow of matching internal variables }{chapter.3}% 7 \BOOKMARK [2][-]{subsection.3.1.1}{Automatons for comparison}{section.3.1}% 8 \BOOKMARK [2][-]{subsection.3.1.2}{First step of the procedure. Detecting non-linear equations.}{section.3.1}% 9 \BOOKMARK [2][-]{subsection.3.1.3}{Second step of the procedure. Calculation of non linear coefficients.}{section.3.1}% 10 \BOOKMARK [2][-]{subsection.3.1.4}{Unfolding and simulation}{section.3.1}% 11 \BOOKMARK [0][-]{chapter.4}{Code Listings}{}% 12 \BOOKMARK [0][-]{chapter.5}{Zusammenfassung und Ausblick}{}% 13 \BOOKMARK [0][-]{figure.caption.11}{Literaturverzeichnis}{}% 14 \BOOKMARK [0][-]{appendix.A}{z.B. Programmdokumentation}{}% 15