1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Fri Sep 23 16:22:11 2011 +0200
     1.3 @@ -0,0 +1,1275 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +\isanewline
    1.10 +\isanewline
    1.11 +%
    1.12 +\endisadelimtheory
    1.13 +%
    1.14 +\isatagtheory
    1.15 +\isacommand{theory}\isamarkupfalse%
    1.16 +\ Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform\ \isakeyword{imports}\ Isac\ \isakeyword{begin}%
    1.17 +\endisatagtheory
    1.18 +{\isafoldtheory}%
    1.19 +%
    1.20 +\isadelimtheory
    1.21 +%
    1.22 +\endisadelimtheory
    1.23 +%
    1.24 +\begin{isamarkuptext}%
    1.25 +We stepwise build Inverse_Z_Transform.thy as an exercise.
    1.26 +  Because subsection "Stepwise Check the Program" requires Inverse_Z_Transform.thy 
    1.27 +  as a subtheory of Isac.thy, the setup has been changed from
    1.28 +  "theory Inverse_Z_Transform imports Isac begin.." to the above.
    1.29 +
    1.30 +  ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
    1.31 +  Here in this theory there are the internal names twice, for instance we have
    1.32 +  (Thm.derivation_name \isa{rule{\isadigit{1}}} = "Build_Inverse_Z_Transform.rule1") = true;
    1.33 +  but actually in us will be "Inverse_Z_Transform.rule1"%
    1.34 +\end{isamarkuptext}%
    1.35 +\isamarkuptrue%
    1.36 +%
    1.37 +\isadelimML
    1.38 +%
    1.39 +\endisadelimML
    1.40 +%
    1.41 +\isatagML
    1.42 +\isacommand{ML}\isamarkupfalse%
    1.43 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}val\ thy\ {\isaliteral{3D}{\isacharequal}}\ %
    1.44 +\isaantiq
    1.45 +theory\ Isac{}%
    1.46 +\endisaantiq
    1.47 +{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
    1.48 +\endisatagML
    1.49 +{\isafoldML}%
    1.50 +%
    1.51 +\isadelimML
    1.52 +%
    1.53 +\endisadelimML
    1.54 +%
    1.55 +\isamarkupsection{trials towards Z transform%
    1.56 +}
    1.57 +\isamarkuptrue%
    1.58 +%
    1.59 +\begin{isamarkuptext}%
    1.60 +===============================%
    1.61 +\end{isamarkuptext}%
    1.62 +\isamarkuptrue%
    1.63 +%
    1.64 +\isamarkupsubsection{terms%
    1.65 +}
    1.66 +\isamarkuptrue%
    1.67 +%
    1.68 +\isadelimML
    1.69 +%
    1.70 +\endisadelimML
    1.71 +%
    1.72 +\isatagML
    1.73 +\isacommand{ML}\isamarkupfalse%
    1.74 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    1.75 +%
    1.76 +\isaantiq
    1.77 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}{}%
    1.78 +\endisaantiq
    1.79 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    1.80 +%
    1.81 +\isaantiq
    1.82 +term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{}%
    1.83 +\endisaantiq
    1.84 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    1.85 +%
    1.86 +\isaantiq
    1.87 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{}%
    1.88 +\endisaantiq
    1.89 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    1.90 +%
    1.91 +\isaantiq
    1.92 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
    1.93 +\endisaantiq
    1.94 +{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}\ {\isaliteral{5D}{\isacharbrackright}}\ denotes\ lists\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
    1.95 +%
    1.96 +\isaantiq
    1.97 +term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
    1.98 +\endisaantiq
    1.99 +{\isaliteral{3B}{\isacharsemicolon}}Isac\isanewline
   1.100 +%
   1.101 +\isaantiq
   1.102 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
   1.103 +\endisaantiq
   1.104 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.105 +term{\isadigit{2}}str\ %
   1.106 +\isaantiq
   1.107 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
   1.108 +\endisaantiq
   1.109 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.110 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.111 +\isacommand{ML}\isamarkupfalse%
   1.112 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.113 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.114 +%
   1.115 +\isaantiq
   1.116 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{22}{\isachardoublequote}}{}%
   1.117 +\endisaantiq
   1.118 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.119 +%
   1.120 +\isaantiq
   1.121 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{22}{\isachardoublequote}}{}%
   1.122 +\endisaantiq
   1.123 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.124 +%
   1.125 +\isaantiq
   1.126 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{22}{\isachardoublequote}}{}%
   1.127 +\endisaantiq
   1.128 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.129 +%
   1.130 +\isaantiq
   1.131 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
   1.132 +\endisaantiq
   1.133 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.134 +term{\isadigit{2}}str\ %
   1.135 +\isaantiq
   1.136 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
   1.137 +\endisaantiq
   1.138 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.139 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.140 +\endisatagML
   1.141 +{\isafoldML}%
   1.142 +%
   1.143 +\isadelimML
   1.144 +%
   1.145 +\endisadelimML
   1.146 +%
   1.147 +\isamarkupsubsection{rules%
   1.148 +}
   1.149 +\isamarkuptrue%
   1.150 +\isacommand{axiomatization}\isamarkupfalse%
   1.151 +\ \isakeyword{where}\ \isanewline
   1.152 +\ \ rule{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C64656C74613E}{\isasymdelta}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
   1.153 +\ \ rule{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
   1.154 +\ \ rule{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ \isanewline
   1.155 +\ \ rule{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
   1.156 +\ \ rule{\isadigit{5}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
   1.157 +\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   1.158 +%
   1.159 +\isadelimML
   1.160 +%
   1.161 +\endisadelimML
   1.162 +%
   1.163 +\isatagML
   1.164 +\isacommand{ML}\isamarkupfalse%
   1.165 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.166 +%
   1.167 +\isaantiq
   1.168 +thm\ rule{\isadigit{1}}{}%
   1.169 +\endisaantiq
   1.170 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.171 +%
   1.172 +\isaantiq
   1.173 +thm\ rule{\isadigit{2}}{}%
   1.174 +\endisaantiq
   1.175 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.176 +%
   1.177 +\isaantiq
   1.178 +thm\ rule{\isadigit{3}}{}%
   1.179 +\endisaantiq
   1.180 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.181 +%
   1.182 +\isaantiq
   1.183 +thm\ rule{\isadigit{4}}{}%
   1.184 +\endisaantiq
   1.185 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.186 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.187 +\endisatagML
   1.188 +{\isafoldML}%
   1.189 +%
   1.190 +\isadelimML
   1.191 +%
   1.192 +\endisadelimML
   1.193 +%
   1.194 +\isamarkupsubsection{apply rules%
   1.195 +}
   1.196 +\isamarkuptrue%
   1.197 +%
   1.198 +\isadelimML
   1.199 +%
   1.200 +\endisadelimML
   1.201 +%
   1.202 +\isatagML
   1.203 +\isacommand{ML}\isamarkupfalse%
   1.204 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.205 +val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
   1.206 +\ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.207 +\isaantiq
   1.208 +thm\ rule{\isadigit{3}}{}%
   1.209 +\endisaantiq
   1.210 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.211 +\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.212 +\isaantiq
   1.213 +thm\ rule{\isadigit{4}}{}%
   1.214 +\endisaantiq
   1.215 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.216 +\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.217 +\isaantiq
   1.218 +thm\ rule{\isadigit{1}}{}%
   1.219 +\endisaantiq
   1.220 +{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline
   1.221 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.222 +\isanewline
   1.223 +val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.224 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.225 +term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}attention\ rule{\isadigit{1}}\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.226 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.227 +\isacommand{ML}\isamarkupfalse%
   1.228 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.229 +val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
   1.230 +\isaantiq
   1.231 +theory\ Isac{}%
   1.232 +\endisaantiq
   1.233 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.234 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.235 +\isacommand{ML}\isamarkupfalse%
   1.236 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.237 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.238 +\isaantiq
   1.239 +thm\ rule{\isadigit{3}}{}%
   1.240 +\endisaantiq
   1.241 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.242 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.243 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.244 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.245 +\isacommand{ML}\isamarkupfalse%
   1.246 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.247 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.248 +\isaantiq
   1.249 +thm\ rule{\isadigit{4}}{}%
   1.250 +\endisaantiq
   1.251 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.252 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.253 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.254 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.255 +\isacommand{ML}\isamarkupfalse%
   1.256 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.257 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
   1.258 +\isaantiq
   1.259 +thm\ rule{\isadigit{1}}{}%
   1.260 +\endisaantiq
   1.261 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.262 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.263 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.264 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.265 +\isacommand{ML}\isamarkupfalse%
   1.266 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.267 +terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.268 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.269 +\endisatagML
   1.270 +{\isafoldML}%
   1.271 +%
   1.272 +\isadelimML
   1.273 +%
   1.274 +\endisadelimML
   1.275 +%
   1.276 +\isamarkupsection{Prepare steps in CTP-based programming language%
   1.277 +}
   1.278 +\isamarkuptrue%
   1.279 +%
   1.280 +\begin{isamarkuptext}%
   1.281 +===================================================%
   1.282 +\end{isamarkuptext}%
   1.283 +\isamarkuptrue%
   1.284 +%
   1.285 +\isamarkupsubsection{prepare expression%
   1.286 +}
   1.287 +\isamarkuptrue%
   1.288 +%
   1.289 +\isadelimML
   1.290 +%
   1.291 +\endisadelimML
   1.292 +%
   1.293 +\isatagML
   1.294 +\isacommand{ML}\isamarkupfalse%
   1.295 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.296 +val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
   1.297 +\isaantiq
   1.298 +theory\ Isac{}%
   1.299 +\endisaantiq
   1.300 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.301 +val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}%
   1.302 +\isaantiq
   1.303 +term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}%
   1.304 +\endisaantiq
   1.305 +{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.306 +\isanewline
   1.307 +val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.308 +val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.309 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.310 +\endisatagML
   1.311 +{\isafoldML}%
   1.312 +%
   1.313 +\isadelimML
   1.314 +%
   1.315 +\endisadelimML
   1.316 +\isanewline
   1.317 +\isanewline
   1.318 +\isacommand{axiomatization}\isamarkupfalse%
   1.319 +\ \isakeyword{where}\isanewline
   1.320 +\ \ ruleZY{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   1.321 +%
   1.322 +\isadelimML
   1.323 +\isanewline
   1.324 +%
   1.325 +\endisadelimML
   1.326 +%
   1.327 +\isatagML
   1.328 +\isacommand{ML}\isamarkupfalse%
   1.329 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.330 +val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
   1.331 +\isaantiq
   1.332 +theory\ Isac{}%
   1.333 +\endisaantiq
   1.334 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.335 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
   1.336 +\isaantiq
   1.337 +thm\ ruleZY{}%
   1.338 +\endisaantiq
   1.339 +\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.340 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
   1.341 +\isaantiq
   1.342 +thm\ ruleZY{}%
   1.343 +\endisaantiq
   1.344 +\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.345 +\isanewline
   1.346 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.347 +\isaantiq
   1.348 +theory\ Isac{}%
   1.349 +\endisaantiq
   1.350 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.351 +term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ TODO{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.352 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.353 +\isaantiq
   1.354 +theory\ Isac{}%
   1.355 +\endisaantiq
   1.356 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.357 +term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.358 +\isanewline
   1.359 +val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ expr{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.360 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.361 +\endisatagML
   1.362 +{\isafoldML}%
   1.363 +%
   1.364 +\isadelimML
   1.365 +%
   1.366 +\endisadelimML
   1.367 +%
   1.368 +\isamarkupsubsection{solve equation%
   1.369 +}
   1.370 +\isamarkuptrue%
   1.371 +%
   1.372 +\begin{isamarkuptext}%
   1.373 +this type of equation if too general for the present program%
   1.374 +\end{isamarkuptext}%
   1.375 +\isamarkuptrue%
   1.376 +%
   1.377 +\isadelimML
   1.378 +%
   1.379 +\endisadelimML
   1.380 +%
   1.381 +\isatagML
   1.382 +\isacommand{ML}\isamarkupfalse%
   1.383 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.384 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Minisubplb{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2D}{\isacharminus}}init{\isaliteral{2D}{\isacharminus}}rootp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}bl{\isaliteral{2E}{\isachardot}}sml\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.385 +val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.386 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.387 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.388 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ TODO{\isaliteral{3A}{\isacharcolon}}\ ISAC\ determines\ type\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.389 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.390 +\endisatagML
   1.391 +{\isafoldML}%
   1.392 +%
   1.393 +\isadelimML
   1.394 +%
   1.395 +\endisadelimML
   1.396 +%
   1.397 +\begin{isamarkuptext}%
   1.398 +Does the Equation Match the Specification ?%
   1.399 +\end{isamarkuptext}%
   1.400 +\isamarkuptrue%
   1.401 +%
   1.402 +\isadelimML
   1.403 +%
   1.404 +\endisadelimML
   1.405 +%
   1.406 +\isatagML
   1.407 +\isacommand{ML}\isamarkupfalse%
   1.408 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.409 +match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.410 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.411 +\isacommand{ML}\isamarkupfalse%
   1.412 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.413 +\isanewline
   1.414 +\isacommand{ML}\isamarkupfalse%
   1.415 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.416 +val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.417 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}specification{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.418 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}equality{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.419 +\ \ \ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}bound\ variable{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.420 +\ \ \ {\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}identifier\ for\ solution{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.421 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}liste\ der\ theoreme\ die\ zum\ lösen\ benötigt\ werden{\isaliteral{2C}{\isacharcomma}}\ aus\ isac{\isaliteral{2C}{\isacharcomma}}\ keine\ spezielle\ methode\ {\isaliteral{28}{\isacharparenleft}}no\ met{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.422 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
   1.423 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}pqFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.424 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.425 +\endisatagML
   1.426 +{\isafoldML}%
   1.427 +%
   1.428 +\isadelimML
   1.429 +%
   1.430 +\endisadelimML
   1.431 +%
   1.432 +\begin{isamarkuptext}%
   1.433 +Does the Other Equation Match the Specification ?%
   1.434 +\end{isamarkuptext}%
   1.435 +\isamarkuptrue%
   1.436 +%
   1.437 +\isadelimML
   1.438 +%
   1.439 +\endisadelimML
   1.440 +%
   1.441 +\isatagML
   1.442 +\isacommand{ML}\isamarkupfalse%
   1.443 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.444 +match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}pqFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.445 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.446 +\endisatagML
   1.447 +{\isafoldML}%
   1.448 +%
   1.449 +\isadelimML
   1.450 +%
   1.451 +\endisadelimML
   1.452 +%
   1.453 +\begin{isamarkuptext}%
   1.454 +Solve Equation Stepwise%
   1.455 +\end{isamarkuptext}%
   1.456 +\isamarkuptrue%
   1.457 +%
   1.458 +\isadelimML
   1.459 +%
   1.460 +\endisadelimML
   1.461 +%
   1.462 +\isatagML
   1.463 +\isacommand{ML}\isamarkupfalse%
   1.464 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.465 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.466 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.467 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.468 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.469 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.470 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.471 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.472 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.473 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.474 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.475 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.476 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline
   1.477 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}nxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}Check{\isaliteral{5F}{\isacharunderscore}}elementwise\ {\isaliteral{22}{\isachardoublequote}}Assumptions{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.478 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline
   1.479 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ f{\isadigit{2}}str\ f{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.480 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ sqrt\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{6}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ sqrt\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{6}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}\ TODO\ sqrt{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.481 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
   1.482 +val\ SOME\ f\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.483 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.484 +\endisatagML
   1.485 +{\isafoldML}%
   1.486 +%
   1.487 +\isadelimML
   1.488 +%
   1.489 +\endisadelimML
   1.490 +%
   1.491 +\isamarkupsubsection{partial fraction decomposition%
   1.492 +}
   1.493 +\isamarkuptrue%
   1.494 +%
   1.495 +\isamarkupsubsubsection{solution of the equation%
   1.496 +}
   1.497 +\isamarkuptrue%
   1.498 +%
   1.499 +\isadelimML
   1.500 +%
   1.501 +\endisadelimML
   1.502 +%
   1.503 +\isatagML
   1.504 +\isacommand{ML}\isamarkupfalse%
   1.505 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.506 +val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.507 +term{\isadigit{2}}str\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.508 +atomty\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.509 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.510 +\endisatagML
   1.511 +{\isafoldML}%
   1.512 +%
   1.513 +\isadelimML
   1.514 +%
   1.515 +\endisadelimML
   1.516 +%
   1.517 +\isamarkupsubsubsection{get solutions out of list%
   1.518 +}
   1.519 +\isamarkuptrue%
   1.520 +%
   1.521 +\begin{isamarkuptext}%
   1.522 +in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$%
   1.523 +\end{isamarkuptext}%
   1.524 +\isamarkuptrue%
   1.525 +%
   1.526 +\isadelimML
   1.527 +%
   1.528 +\endisadelimML
   1.529 +%
   1.530 +\isatagML
   1.531 +\isacommand{ML}\isamarkupfalse%
   1.532 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.533 +val\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline
   1.534 +\ \ \ \ \ \ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}\ {\isaliteral{24}{\isachardollar}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Nil{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.535 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.536 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.537 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.538 +\isanewline
   1.539 +\isacommand{ML}\isamarkupfalse%
   1.540 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Solutions\ as\ Denominator\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Denominator{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ z\ {\isaliteral{2D}{\isacharminus}}\ Zeropoint{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ Denominator{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{2D}{\isacharminus}}Zeropoint{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.541 +val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.542 +val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.543 +val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.544 +val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.545 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.546 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.547 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.548 +\endisatagML
   1.549 +{\isafoldML}%
   1.550 +%
   1.551 +\isadelimML
   1.552 +%
   1.553 +\endisadelimML
   1.554 +%
   1.555 +\isamarkupsubsubsection{build expression%
   1.556 +}
   1.557 +\isamarkuptrue%
   1.558 +%
   1.559 +\begin{isamarkuptext}%
   1.560 +in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)%
   1.561 +\end{isamarkuptext}%
   1.562 +\isamarkuptrue%
   1.563 +%
   1.564 +\isadelimML
   1.565 +%
   1.566 +\endisadelimML
   1.567 +%
   1.568 +\isatagML
   1.569 +\isacommand{ML}\isamarkupfalse%
   1.570 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.571 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}The\ Main\ Denominator\ is\ the\ multiplikation\ of\ the\ partial\ fraction\ denominators{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.572 +val\ denominator{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.573 +val\ SOME\ numerator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.574 +\isanewline
   1.575 +val\ expr{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.576 +term{\isadigit{2}}str\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.577 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.578 +\endisatagML
   1.579 +{\isafoldML}%
   1.580 +%
   1.581 +\isadelimML
   1.582 +%
   1.583 +\endisadelimML
   1.584 +%
   1.585 +\isamarkupsubsubsection{Ansatz - create partial fractions out of our expression%
   1.586 +}
   1.587 +\isamarkuptrue%
   1.588 +%
   1.589 +\isadelimML
   1.590 +%
   1.591 +\endisadelimML
   1.592 +%
   1.593 +\isatagML
   1.594 +\isacommand{ML}\isamarkupfalse%
   1.595 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.596 +\endisatagML
   1.597 +{\isafoldML}%
   1.598 +%
   1.599 +\isadelimML
   1.600 +%
   1.601 +\endisadelimML
   1.602 +\isanewline
   1.603 +\isanewline
   1.604 +\isacommand{axiomatization}\isamarkupfalse%
   1.605 +\ \isakeyword{where}\isanewline
   1.606 +\ \ ansatz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
   1.607 +\ \ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n\ \ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   1.608 +%
   1.609 +\isadelimML
   1.610 +\isanewline
   1.611 +%
   1.612 +\endisadelimML
   1.613 +%
   1.614 +\isatagML
   1.615 +\isacommand{ML}\isamarkupfalse%
   1.616 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.617 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}we\ use\ our\ ansatz{\isadigit{2}}\ to\ rewrite\ our\ expression\ and\ get\ an\ equilation\ with\ our\ expression\ on\ the\ left\ and\ the\ partial\ fractions\ of\ it\ on\ the\ right\ side{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.618 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %
   1.619 +\isaantiq
   1.620 +theory\ Isac{}%
   1.621 +\endisaantiq
   1.622 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %
   1.623 +\isaantiq
   1.624 +thm\ ansatz{\isadigit{2}}{}%
   1.625 +\endisaantiq
   1.626 +\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.627 +term{\isadigit{2}}str\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ atomty\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.628 +val\ eq{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}expr{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.629 +term{\isadigit{2}}str\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.630 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.631 +\isacommand{ML}\isamarkupfalse%
   1.632 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.633 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}eliminate\ the\ demoninators\ by\ multiplying\ the\ left\ and\ the\ right\ side\ with\ the\ main\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.634 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %
   1.635 +\isaantiq
   1.636 +theory\ Isac{}%
   1.637 +\endisaantiq
   1.638 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %
   1.639 +\isaantiq
   1.640 +thm\ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{}%
   1.641 +\endisaantiq
   1.642 +\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.643 +term{\isadigit{2}}str\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.644 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.645 +\isacommand{ML}\isamarkupfalse%
   1.646 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.647 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplificatoin{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.648 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.649 +\isaantiq
   1.650 +theory\ Isac{}%
   1.651 +\endisaantiq
   1.652 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.653 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3F}{\isacharquery}}A\ {\isaliteral{3F}{\isacharquery}}B\ not\ simplified{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.654 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.655 +\isacommand{ML}\isamarkupfalse%
   1.656 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.657 +val\ SOME\ fract{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
   1.658 +\ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}A\ B\ {\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.659 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fract{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.660 +\isaantiq
   1.661 +theory\ Isac{}%
   1.662 +\endisaantiq
   1.663 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fract{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.664 +term{\isadigit{2}}str\ fract{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ A\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2A}{\isacharasterisk}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.665 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}term{\isadigit{2}}str\ fract{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ would\ be\ more\ traditional{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.666 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.667 +\isacommand{ML}\isamarkupfalse%
   1.668 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.669 +val\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ eq{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.670 +val\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ fract{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}A\ B\ {\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.671 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.672 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}MANDATORY{\isaliteral{3A}{\isacharcolon}}\ simplify\ {\isaliteral{28}{\isacharparenleft}}and\ remove\ denominator{\isaliteral{29}{\isacharparenright}}\ otherwise\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.673 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.674 +\isaantiq
   1.675 +theory\ Isac{}%
   1.676 +\endisaantiq
   1.677 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.678 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.679 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.680 +\isacommand{ML}\isamarkupfalse%
   1.681 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.682 +\endisatagML
   1.683 +{\isafoldML}%
   1.684 +%
   1.685 +\isadelimML
   1.686 +%
   1.687 +\endisadelimML
   1.688 +%
   1.689 +\isamarkupsubsubsection{get first koeffizient%
   1.690 +}
   1.691 +\isamarkuptrue%
   1.692 +%
   1.693 +\isadelimML
   1.694 +%
   1.695 +\endisadelimML
   1.696 +%
   1.697 +\isatagML
   1.698 +\isacommand{ML}\isamarkupfalse%
   1.699 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.700 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}substitude\ z\ with\ the\ first\ zeropoint\ to\ get\ A{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.701 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}terms{\isaliteral{5F}{\isacharunderscore}}\ %
   1.702 +\isaantiq
   1.703 +theory\ Isac{}%
   1.704 +\endisaantiq
   1.705 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.706 +term{\isadigit{2}}str\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.707 +\isanewline
   1.708 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.709 +\isaantiq
   1.710 +theory\ Isac{}%
   1.711 +\endisaantiq
   1.712 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.713 +term{\isadigit{2}}str\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.714 +\isanewline
   1.715 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2A}{\isacharasterisk}}\ A\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ A{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.716 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.717 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}solve\ the\ simple\ linear\ equilation\ for\ A\ TODO{\isaliteral{3A}{\isacharcolon}}\ return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.718 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.719 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.720 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.721 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.722 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.723 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.724 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.725 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.726 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.727 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.728 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.729 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.730 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.731 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.732 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.733 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.734 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.735 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.736 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.737 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.738 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.739 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.740 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.741 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.742 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.743 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.744 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.745 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
   1.746 +f{\isadigit{2}}str\ fa{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.747 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.748 +\endisatagML
   1.749 +{\isafoldML}%
   1.750 +%
   1.751 +\isadelimML
   1.752 +%
   1.753 +\endisadelimML
   1.754 +%
   1.755 +\isamarkupsubsubsection{get second koeffizient%
   1.756 +}
   1.757 +\isamarkuptrue%
   1.758 +%
   1.759 +\isadelimML
   1.760 +%
   1.761 +\endisadelimML
   1.762 +%
   1.763 +\isatagML
   1.764 +\isacommand{ML}\isamarkupfalse%
   1.765 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.766 +\isanewline
   1.767 +\isacommand{ML}\isamarkupfalse%
   1.768 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.769 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}substitude\ z\ with\ the\ second\ zeropoint\ to\ get\ B{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.770 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}terms{\isaliteral{5F}{\isacharunderscore}}\ %
   1.771 +\isaantiq
   1.772 +theory\ Isac{}%
   1.773 +\endisaantiq
   1.774 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.775 +term{\isadigit{2}}str\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.776 +\isanewline
   1.777 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
   1.778 +\isaantiq
   1.779 +theory\ Isac{}%
   1.780 +\endisaantiq
   1.781 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.782 +term{\isadigit{2}}str\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.783 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.784 +\isacommand{ML}\isamarkupfalse%
   1.785 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.786 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}solve\ the\ simple\ linear\ equilation\ for\ B\ TODO{\isaliteral{3A}{\isacharcolon}}\ return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.787 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{3}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ B{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.788 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.789 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.790 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.791 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.792 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.793 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.794 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.795 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.796 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.797 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.798 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.799 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.800 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.801 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.802 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.803 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.804 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.805 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.806 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.807 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.808 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.809 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.810 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.811 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.812 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.813 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.814 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.815 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.816 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
   1.817 +f{\isadigit{2}}str\ fb{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.818 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.819 +\isanewline
   1.820 +\isacommand{ML}\isamarkupfalse%
   1.821 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}check\ koeffizients{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.822 +if\ f{\isadigit{2}}str\ fa\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ else\ error\ {\isaliteral{22}{\isachardoublequote}}part{\isaliteral{2E}{\isachardot}}fract{\isaliteral{2E}{\isachardot}}\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.823 +if\ f{\isadigit{2}}str\ fb\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}B\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ else\ error\ {\isaliteral{22}{\isachardoublequote}}part{\isaliteral{2E}{\isachardot}}fract{\isaliteral{2E}{\isachardot}}\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.824 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.825 +\endisatagML
   1.826 +{\isafoldML}%
   1.827 +%
   1.828 +\isadelimML
   1.829 +%
   1.830 +\endisadelimML
   1.831 +%
   1.832 +\isamarkupsubsubsection{substitute expression with solutions%
   1.833 +}
   1.834 +\isamarkuptrue%
   1.835 +%
   1.836 +\isadelimML
   1.837 +%
   1.838 +\endisadelimML
   1.839 +%
   1.840 +\isatagML
   1.841 +\isacommand{ML}\isamarkupfalse%
   1.842 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.843 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.844 +\isacommand{ML}\isamarkupfalse%
   1.845 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.846 +\endisatagML
   1.847 +{\isafoldML}%
   1.848 +%
   1.849 +\isadelimML
   1.850 +%
   1.851 +\endisadelimML
   1.852 +%
   1.853 +\isamarkupsection{Implement the Specification and the Method%
   1.854 +}
   1.855 +\isamarkuptrue%
   1.856 +%
   1.857 +\begin{isamarkuptext}%
   1.858 +==============================================%
   1.859 +\end{isamarkuptext}%
   1.860 +\isamarkuptrue%
   1.861 +%
   1.862 +\isamarkupsubsection{Define the Field Descriptions for the specification%
   1.863 +}
   1.864 +\isamarkuptrue%
   1.865 +\isacommand{consts}\isamarkupfalse%
   1.866 +\isanewline
   1.867 +\ \ filterExpression\ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ una{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   1.868 +\ \ stepResponse\ \ \ \ \ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ una{\isaliteral{22}{\isachardoublequoteclose}}%
   1.869 +\isamarkupsubsection{Define the Specification%
   1.870 +}
   1.871 +\isamarkuptrue%
   1.872 +%
   1.873 +\isadelimML
   1.874 +%
   1.875 +\endisadelimML
   1.876 +%
   1.877 +\isatagML
   1.878 +\isacommand{ML}\isamarkupfalse%
   1.879 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.880 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
   1.881 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
   1.882 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.883 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
   1.884 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
   1.885 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.886 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.887 +\isacommand{ML}\isamarkupfalse%
   1.888 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.889 +\isacommand{ML}\isamarkupfalse%
   1.890 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.891 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
   1.892 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
   1.893 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.894 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.895 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.896 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.897 +\ \ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ preds\ in\ where{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ \isanewline
   1.898 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.899 +\isanewline
   1.900 +show{\isaliteral{5F}{\isacharunderscore}}ptyps{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.901 +get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.902 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.903 +\endisatagML
   1.904 +{\isafoldML}%
   1.905 +%
   1.906 +\isadelimML
   1.907 +%
   1.908 +\endisadelimML
   1.909 +%
   1.910 +\isamarkupsubsection{Define Name and Signature for the Method%
   1.911 +}
   1.912 +\isamarkuptrue%
   1.913 +\isacommand{consts}\isamarkupfalse%
   1.914 +\isanewline
   1.915 +\ \ InverseZTransform\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}bool{\isaliteral{2C}{\isacharcomma}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   1.916 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}%
   1.917 +\isamarkupsubsection{Setup Parent Nodes in Hierarchy of Method%
   1.918 +}
   1.919 +\isamarkuptrue%
   1.920 +%
   1.921 +\isadelimML
   1.922 +%
   1.923 +\endisadelimML
   1.924 +%
   1.925 +\isatagML
   1.926 +\isacommand{ML}\isamarkupfalse%
   1.927 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.928 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
   1.929 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
   1.930 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.931 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.932 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.933 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
   1.934 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
   1.935 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.936 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.937 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.938 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.939 +\isacommand{ML}\isamarkupfalse%
   1.940 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.941 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
   1.942 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
   1.943 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
   1.944 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.945 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.946 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.947 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.948 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.949 +\ \ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}\isanewline
   1.950 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.951 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
   1.952 +\isacommand{ML}\isamarkupfalse%
   1.953 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.954 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
   1.955 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
   1.956 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
   1.957 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.958 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
   1.959 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.960 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.961 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   1.962 +\ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
   1.963 +\ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
   1.964 +\ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
   1.965 +\ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
   1.966 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.967 +\isanewline
   1.968 +show{\isaliteral{5F}{\isacharunderscore}}mets{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.969 +get{\isaliteral{5F}{\isacharunderscore}}met\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   1.970 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
   1.971 +\endisatagML
   1.972 +{\isafoldML}%
   1.973 +%
   1.974 +\isadelimML
   1.975 +%
   1.976 +\endisadelimML
   1.977 +%
   1.978 +\isamarkupsection{Program in CTP-based language%
   1.979 +}
   1.980 +\isamarkuptrue%
   1.981 +%
   1.982 +\begin{isamarkuptext}%
   1.983 +=================================%
   1.984 +\end{isamarkuptext}%
   1.985 +\isamarkuptrue%
   1.986 +%
   1.987 +\isamarkupsubsection{Stepwise extend Program%
   1.988 +}
   1.989 +\isamarkuptrue%
   1.990 +%
   1.991 +\isadelimML
   1.992 +%
   1.993 +\endisadelimML
   1.994 +%
   1.995 +\isatagML
   1.996 +\isacommand{ML}\isamarkupfalse%
   1.997 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
   1.998 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
   1.999 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1000 +{\isaliteral{22}{\isachardoublequote}}\ Xeq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1001 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1002 +\isacommand{ML}\isamarkupfalse%
  1.1003 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1004 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
  1.1005 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1006 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1007 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1008 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1009 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1010 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}NONE{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1011 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1012 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1013 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1014 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1015 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1016 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1017 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1018 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1019 +\isacommand{ML}\isamarkupfalse%
  1.1020 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1021 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
  1.1022 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1023 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1024 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1025 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1026 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1027 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1028 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1029 +\isacommand{ML}\isamarkupfalse%
  1.1030 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1031 +parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1032 +val\ sc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}inst{\isaliteral{5F}{\isacharunderscore}}abs\ thy{\isaliteral{29}{\isacharparenright}}\ o\ term{\isaliteral{5F}{\isacharunderscore}}of\ o\ the\ o\ {\isaliteral{28}{\isacharparenleft}}parse\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1033 +atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1034 +\isanewline
  1.1035 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1036 +\isacommand{ML}\isamarkupfalse%
  1.1037 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1038 +term{\isadigit{2}}str\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1039 +atomty\ sc\isanewline
  1.1040 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1041 +\endisatagML
  1.1042 +{\isafoldML}%
  1.1043 +%
  1.1044 +\isadelimML
  1.1045 +%
  1.1046 +\endisadelimML
  1.1047 +%
  1.1048 +\isamarkupsubsection{Store Final Version of Program for Execution%
  1.1049 +}
  1.1050 +\isamarkuptrue%
  1.1051 +%
  1.1052 +\isadelimML
  1.1053 +%
  1.1054 +\endisadelimML
  1.1055 +%
  1.1056 +\isatagML
  1.1057 +\isacommand{ML}\isamarkupfalse%
  1.1058 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1059 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
  1.1060 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
  1.1061 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
  1.1062 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1063 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1064 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1065 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1066 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1067 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1068 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
  1.1069 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1070 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1071 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
  1.1072 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
  1.1073 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1074 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1075 +\endisatagML
  1.1076 +{\isafoldML}%
  1.1077 +%
  1.1078 +\isadelimML
  1.1079 +%
  1.1080 +\endisadelimML
  1.1081 +%
  1.1082 +\isamarkupsubsection{Check the Program%
  1.1083 +}
  1.1084 +\isamarkuptrue%
  1.1085 +%
  1.1086 +\isamarkupsubsubsection{Check the formalization%
  1.1087 +}
  1.1088 +\isamarkuptrue%
  1.1089 +%
  1.1090 +\isadelimML
  1.1091 +%
  1.1092 +\endisadelimML
  1.1093 +%
  1.1094 +\isatagML
  1.1095 +\isacommand{ML}\isamarkupfalse%
  1.1096 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1097 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ {\isaliteral{28}{\isacharparenleft}}X\ \ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
  1.1098 +\ \ {\isaliteral{22}{\isachardoublequote}}stepResponse\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1099 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
  1.1100 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1101 +\isanewline
  1.1102 +val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}filterExpression{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1103 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{2E}{\isachardot}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1104 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}stepResponse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1105 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Free\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
  1.1106 +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ prep{\isaliteral{5F}{\isacharunderscore}}ori\ fmz\ thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}ppc\ o\ get{\isaliteral{5F}{\isacharunderscore}}pbt{\isaliteral{29}{\isacharparenright}}\ pI{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1107 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1108 +\endisatagML
  1.1109 +{\isafoldML}%
  1.1110 +%
  1.1111 +\isadelimML
  1.1112 +%
  1.1113 +\endisadelimML
  1.1114 +%
  1.1115 +\isamarkupsubsubsection{Stepwise check the program%
  1.1116 +}
  1.1117 +\isamarkuptrue%
  1.1118 +%
  1.1119 +\isadelimML
  1.1120 +%
  1.1121 +\endisadelimML
  1.1122 +%
  1.1123 +\isatagML
  1.1124 +\isacommand{ML}\isamarkupfalse%
  1.1125 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1126 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1127 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1128 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1129 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ {\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
  1.1130 +\ \ {\isaliteral{22}{\isachardoublequote}}stepResponse\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1131 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
  1.1132 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1133 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
  1.1134 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1135 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1136 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1137 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1138 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1139 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1140 +\isacommand{ML}\isamarkupfalse%
  1.1141 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1142 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1143 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1144 +\isacommand{ML}\isamarkupfalse%
  1.1145 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1146 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1147 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1148 +\isacommand{ML}\isamarkupfalse%
  1.1149 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1150 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1151 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1152 +\isacommand{ML}\isamarkupfalse%
  1.1153 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1154 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1155 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1156 +\isacommand{ML}\isamarkupfalse%
  1.1157 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1158 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1159 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1160 +\isacommand{ML}\isamarkupfalse%
  1.1161 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1162 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
  1.1163 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1164 +\isacommand{ML}\isamarkupfalse%
  1.1165 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1166 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1167 +\isacommand{ML}\isamarkupfalse%
  1.1168 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1169 +\isanewline
  1.1170 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1171 +\isacommand{ML}\isamarkupfalse%
  1.1172 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1173 +\isanewline
  1.1174 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1175 +\isacommand{ML}\isamarkupfalse%
  1.1176 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1177 +\isanewline
  1.1178 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1179 +\isacommand{ML}\isamarkupfalse%
  1.1180 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1181 +\isanewline
  1.1182 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1183 +\isanewline
  1.1184 +\isacommand{ML}\isamarkupfalse%
  1.1185 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1186 +\isanewline
  1.1187 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1188 +\isacommand{ML}\isamarkupfalse%
  1.1189 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1190 +\isanewline
  1.1191 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1192 +\isanewline
  1.1193 +\isacommand{ML}\isamarkupfalse%
  1.1194 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1195 +\isanewline
  1.1196 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1197 +\isacommand{ML}\isamarkupfalse%
  1.1198 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1199 +\isanewline
  1.1200 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
  1.1201 +\isacommand{ML}\isamarkupfalse%
  1.1202 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1203 +\isanewline
  1.1204 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1205 +\endisatagML
  1.1206 +{\isafoldML}%
  1.1207 +%
  1.1208 +\isadelimML
  1.1209 +%
  1.1210 +\endisadelimML
  1.1211 +%
  1.1212 +\isamarkupsection{Write Tests for Crucial Details%
  1.1213 +}
  1.1214 +\isamarkuptrue%
  1.1215 +%
  1.1216 +\begin{isamarkuptext}%
  1.1217 +===================================%
  1.1218 +\end{isamarkuptext}%
  1.1219 +\isamarkuptrue%
  1.1220 +%
  1.1221 +\isadelimML
  1.1222 +%
  1.1223 +\endisadelimML
  1.1224 +%
  1.1225 +\isatagML
  1.1226 +\isacommand{ML}\isamarkupfalse%
  1.1227 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1228 +\isanewline
  1.1229 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1230 +\endisatagML
  1.1231 +{\isafoldML}%
  1.1232 +%
  1.1233 +\isadelimML
  1.1234 +%
  1.1235 +\endisadelimML
  1.1236 +%
  1.1237 +\isamarkupsection{Integrate Program into Knowledge%
  1.1238 +}
  1.1239 +\isamarkuptrue%
  1.1240 +%
  1.1241 +\isadelimML
  1.1242 +%
  1.1243 +\endisadelimML
  1.1244 +%
  1.1245 +\isatagML
  1.1246 +\isacommand{ML}\isamarkupfalse%
  1.1247 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
  1.1248 +\isanewline
  1.1249 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
  1.1250 +\endisatagML
  1.1251 +{\isafoldML}%
  1.1252 +%
  1.1253 +\isadelimML
  1.1254 +%
  1.1255 +\endisadelimML
  1.1256 +\isanewline
  1.1257 +%
  1.1258 +\isadelimtheory
  1.1259 +\isanewline
  1.1260 +%
  1.1261 +\endisadelimtheory
  1.1262 +%
  1.1263 +\isatagtheory
  1.1264 +\isacommand{end}\isamarkupfalse%
  1.1265 +%
  1.1266 +\endisatagtheory
  1.1267 +{\isafoldtheory}%
  1.1268 +%
  1.1269 +\isadelimtheory
  1.1270 +%
  1.1271 +\endisadelimtheory
  1.1272 +\isanewline
  1.1273 +\isanewline
  1.1274 +\end{isabellebody}%
  1.1275 +%%% Local Variables:
  1.1276 +%%% mode: latex
  1.1277 +%%% TeX-master: "root"
  1.1278 +%%% End: