test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex
1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Feb 20 18:31:00 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Mar 07 15:29:02 2012 +0100
1.3 @@ -22,13 +22,13 @@
1.4 %
1.5 \begin{isamarkuptext}%
1.6 We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
1.7 - exercise. Because subsection~\ref{sec:stepcheck} requires
1.8 + exercise. Because Subsection~\ref{sec:stepcheck} requires
1.9 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
1.10 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
1.11 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
1.12 \par \noindent
1.13 \begin{center}
1.14 - \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
1.15 + \textbf{Attention with the names of identifiers when going into internals!}
1.16 \end{center}
1.17 Here in this theory there are the internal names twice, for instance we have
1.18 \ttfamily (Thm.derivation\_name \isa{rule{\isadigit{1}}} =
1.19 @@ -306,13 +306,13 @@
1.20 %
1.21 \endisadelimML
1.22 %
1.23 -\isamarkupsection{Prepare Steps for CTP-based programming Language\label{sec:prepstep}%
1.24 +\isamarkupsection{Prepare Steps for TP-based programming Language\label{sec:prepstep}%
1.25 }
1.26 \isamarkuptrue%
1.27 %
1.28 \begin{isamarkuptext}%
1.29 -\par \noindent The following sections are challanging with the CTP-based
1.30 - possibilities of building the programm. The goal is realized in
1.31 +\par \noindent The following sections are challenging with the CTP-based
1.32 + possibilities of building the program. The goal is realized in
1.33 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
1.34 \par The reader is advised to jump between the subsequent subsections and
1.35 the respective steps in Section~\ref{prog-steps}. By comparing
1.36 @@ -327,7 +327,7 @@
1.37 %
1.38 \begin{isamarkuptext}%
1.39 \noindent We try two different notations and check which of them
1.40 - isabelle can handle best.%
1.41 + Isabelle can handle best.%
1.42 \end{isamarkuptext}%
1.43 \isamarkuptrue%
1.44 %
1.45 @@ -366,7 +366,7 @@
1.46 \isamarkuptrue%
1.47 %
1.48 \begin{isamarkuptext}%
1.49 -\noindent The partial fraction decomposion is only possible ig we
1.50 +\noindent The partial fraction decomposition is only possible if we
1.51 get the bound variable out of the numerator. Therefor we divide
1.52 the expression by $z$. Follow up the Calculation at
1.53 Section~\ref{sec:calc:ztrans} line number 02.%
1.54 @@ -483,8 +483,8 @@
1.55 \isamarkuptrue%
1.56 %
1.57 \begin{isamarkuptext}%
1.58 -\noindent The selv written functions in e.g. \texttt{get\_denominator}
1.59 - should become a constant for the isabelle parser:%
1.60 +\noindent The self written functions in e.g. \texttt{get\_denominator}
1.61 + should become a constant for the Isabelle parser:%
1.62 \end{isamarkuptext}%
1.63 \isamarkuptrue%
1.64 \isacommand{consts}\isamarkupfalse%
1.65 @@ -499,7 +499,7 @@
1.66 \par \noindent ATTENTION: From now on \ttfamily
1.67 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
1.68 it only works due to re-building {\sisac} several times (indicated
1.69 - explicityl).%
1.70 + explicitly).%
1.71 \end{isamarkuptext}%
1.72 \isamarkuptrue%
1.73 %
1.74 @@ -539,8 +539,8 @@
1.75 %
1.76 \begin{isamarkuptext}%
1.77 \noindent \ttfamily get\_numerator \normalfont should also become a
1.78 - constant for the isabelle parser, follow up the \texttt{const}
1.79 - decleration above.%
1.80 + constant for the Isabelle parser, follow up the \texttt{const}
1.81 + declaration above.%
1.82 \end{isamarkuptext}%
1.83 \isamarkuptrue%
1.84 %
1.85 @@ -573,7 +573,7 @@
1.86 \endisadelimML
1.87 %
1.88 \begin{isamarkuptext}%
1.89 -\noindent We discovered severell problems by implementing the
1.90 +\noindent We discovered several problems by implementing the
1.91 \ttfamily get\_numerator \normalfont function. Remember when
1.92 putting new functions to {\sisac}, put them in a thy file and rebuild
1.93 {\sisac}, also put them in the ruleset for the script!%
1.94 @@ -587,7 +587,7 @@
1.95 \begin{isamarkuptext}%
1.96 \noindent We have to find the zeros of the term, therefor we use our
1.97 \ttfamily get\_denominator \normalfont function from the step before
1.98 - and try to solve the second order eqeuation. (Follow up the Calculation
1.99 + and try to solve the second order equation. (Follow up the Calculation
1.100 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
1.101 equation is too general for the present program.
1.102 \par We know that this equation can be categorized as \em univariate
1.103 @@ -619,7 +619,7 @@
1.104 %
1.105 \begin{isamarkuptext}%
1.106 \noindent Check if the given equation matches the specification of this
1.107 - quation type.%
1.108 + equation type.%
1.109 \end{isamarkuptext}%
1.110 \isamarkuptrue%
1.111 %
1.112 @@ -673,7 +673,7 @@
1.113 %
1.114 \begin{isamarkuptext}%
1.115 \noindent Check if the (other) given equation matches the
1.116 - specification of this quation type.%
1.117 + specification of this equation type.%
1.118 \end{isamarkuptext}%
1.119 \isamarkuptrue%
1.120 %
1.121 @@ -743,7 +743,7 @@
1.122 \isamarkuptrue%
1.123 %
1.124 \begin{isamarkuptext}%
1.125 -\noindent We go on with the decomposion of our expression. Follow up the
1.126 +\noindent We go on with the decomposition of our expression. Follow up the
1.127 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
1.128 Subproblem~1.%
1.129 \end{isamarkuptext}%
1.130 @@ -781,9 +781,11 @@
1.131 \isamarkuptrue%
1.132 %
1.133 \begin{isamarkuptext}%
1.134 -\noindent In {\sisac}'s CTP-based programming language:
1.135 - \ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
1.136 - can be usefull.%
1.137 +\noindent In {\sisac}'s TP-based programming language:
1.138 +\begin{verbatim}
1.139 + let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
1.140 +\end{verbatim}
1.141 + can be useful.%
1.142 \end{isamarkuptext}%
1.143 \isamarkuptrue%
1.144 %
1.145 @@ -807,13 +809,13 @@
1.146 \endisadelimML
1.147 %
1.148 \begin{isamarkuptext}%
1.149 -\noindent The ansatz for the \em Partial Fraction Decomposion \normalfont
1.150 +\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
1.151 requires to get the denominators of the partial fractions out of the
1.152 Solutions as:
1.153 \begin{itemize}
1.154 - \item $ \text{Denominator} _{1} = z - \text{Zeropoint}_{1}$
1.155 - \item $ \text{Denominator} _{2} = z - \text{Zeropoint}_{2}$
1.156 - \item \ldots
1.157 + \item $Denominator_{1}=z-Zeropoint_{1}$
1.158 + \item $Denominator_{2}=z-Zeropoint_{2}$
1.159 + \item \ldots
1.160 \end{itemize}%
1.161 \end{isamarkuptext}%
1.162 \isamarkuptrue%
1.163 @@ -896,8 +898,8 @@
1.164 \noindent This function needs to be packed such that it can be evaluated
1.165 by the Lucas-Interpreter. Therefor we moved the function to the
1.166 corresponding \ttfamily Equation.thy \normalfont in our case
1.167 - \ttfamily PartialFractions.thy \normalfont. The neccessary steps
1.168 - are quit the same as we have done with \ttfamliy get\_denominator
1.169 + \ttfamily PartialFractions.thy \normalfont. The necessary steps
1.170 + are quit the same as we have done with \ttfamily get\_denominator
1.171 \normalfont before.%
1.172 \end{isamarkuptext}%
1.173 \isamarkuptrue%
1.174 @@ -932,92 +934,104 @@
1.175 \endisadelimML
1.176 %
1.177 \begin{isamarkuptext}%
1.178 -\noindent The tracing output of the calc tree after apllying this
1.179 - function was \ttfamily 24 / factors\_from\_solution
1.180 - [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
1.181 - val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
1.182 - indicate, that the Lucas-Interpreter (LIP) does not know how to
1.183 - evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew
1.184 - that there is something wrong or missing.%
1.185 +\noindent The tracing output of the calc tree after applying this
1.186 + function was:
1.187 +\begin{verbatim}
1.188 + 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
1.189 +\end{verbatim}
1.190 + and the next step:
1.191 +\begin{verbatim}
1.192 + val nxt = ("Empty_Tac", ...): tac'_)
1.193 +\end{verbatim}
1.194 + These observations indicate, that the Lucas-Interpreter (LIP)
1.195 + does not know how to evaluate \ttfamily factors\_from\_solution
1.196 + \normalfont, so we knew that there is something wrong or missing.%
1.197 \end{isamarkuptext}%
1.198 \isamarkuptrue%
1.199 %
1.200 \begin{isamarkuptext}%
1.201 -\noindent First we isolate the difficulty in the program as follows:\\
1.202 - \ttfamily \par \noindent
1.203 - "(L\_L::bool list) = (SubProblem (PolyEq',"\^\\
1.204 - "[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\
1.205 - "[BOOL equ, REAL zzz]);"\^\\
1.206 - "(facs::real) = factors\_from\_solution L\_L;"\^\\
1.207 - "(foo::real) = Take facs"\^\\
1.208 +\noindent First we isolate the difficulty in the program as follows:
1.209 +\begin{verbatim}
1.210 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
1.211 + " [abcFormula, degree_2, polynomial, " ^
1.212 + " univariate,equation], " ^
1.213 + " [no_met]) " ^
1.214 + " [BOOL equ, REAL zzz]); " ^
1.215 + " (facs::real) = factors_from_solution L_L; " ^
1.216 + " (foo::real) = Take facs " ^
1.217 +\end{verbatim}
1.218 +
1.219 + \par \noindent And see the tracing output:
1.220 +
1.221 +\begin{verbatim}
1.222 + [(([], Frm), Problem (Isac, [inverse,
1.223 + Z_Transform,
1.224 + SignalProcessing])),
1.225 + (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
1.226 + (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
1.227 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
1.228 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.229 + (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
1.230 + (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
1.231 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
1.232 + (([3,2], Res), z = 1 / 2 | z = -1 / 4),
1.233 + (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
1.234 + (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
1.235 + (([3], Res), [ z = 1 / 2, z = -1 / 4]),
1.236 + (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
1.237 +\end{verbatim}
1.238 +
1.239 + \par \noindent In particular that:
1.240 +
1.241 +\begin{verbatim}
1.242 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.243 +\end{verbatim}
1.244 + \par \noindent Shows the equation which has been created in
1.245 + the program by:
1.246 +\begin{verbatim}
1.247 + "(denom::real) = get_denominator funterm; " ^
1.248 + (* get_denominator *)
1.249 + "(equ::bool) = (denom = (0::real)); " ^
1.250 +\end{verbatim}
1.251
1.252 - \normalfont \par \noindent And see the tracing output:\\
1.253 - \ttfamily \par \noindent \lbrack\\
1.254 - ((\lbrack\rbrack, Frm), Problem
1.255 - (Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\
1.256 - ((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\
1.257 - ((\lbrack 1\rbrack, Res),
1.258 - ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\
1.259 - ((\lbrack 2\rbrack, Res),
1.260 - ?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\
1.261 - ((\lbrack 3\rbrack, Pbl),
1.262 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
1.263 - ((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\
1.264 - ((\lbrack 3,1\rbrack, Res),
1.265 - z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\
1.266 - z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\
1.267 - ((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\
1.268 - ((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.269 - ((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.270 - ((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\
1.271 - ((\lbrack 4\rbrack, Frm),
1.272 - factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\
1.273 - \rbrack\\
1.274 -
1.275 - \normalfont \noindent In particular that:\\
1.276 - \ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl),
1.277 - solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\
1.278 - \normalfont \par \noindent Shows the equation which has been created in
1.279 - the program by: \ttfamily \\
1.280 -
1.281 - \noindent "(denom::real) = get\_denominator funterm;"\^
1.282 - ~(*get\_denominator*)\\
1.283 - "(equ::bool) = (denom = (0::real));"\^\\
1.284 -
1.285 - \noindent get\_denominator \normalfont has been evaluated successfully,
1.286 + \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully,
1.287 but not\\ \ttfamily factors\_from\_solution.\normalfont
1.288 So we stepwise compare with an analogous case, \ttfamily get\_denominator
1.289 \normalfont successfully done above: We know that LIP evaluates
1.290 expressions in the program by use of the \emph{srls}, so we try to get
1.291 the original \emph{srls}.\\
1.292
1.293 - \noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily
1.294 - = get\_met \lbrack "SignalProcessing",
1.295 - "Z\_Transform","inverse"\rbrack;\\
1.296 +\begin{verbatim}
1.297 + val {srls,...} = get_met ["SignalProcessing",
1.298 + "Z_Transform",
1.299 + "inverse"];
1.300 +\end{verbatim}
1.301
1.302 - \par \noindent \normalfont Create 2 good example terms\\
1.303 - \ttfamily \par \noindent val SOME t1 =\\
1.304 - parseNEW ctxt "get\_denominator ((111::real) / 222)";
1.305 - \par \noindent val SOME t2 =\\
1.306 - parseNEW ctxt "factors\_from\_solution \lbrack(z::real)
1.307 - = 1/2, z = -1/4\rbrack";\\
1.308 + \par \noindent Create 2 good example terms:
1.309
1.310 - \par \noindent \normalfont Rewrite the terms using srls:\\
1.311 +\begin{verbatim}
1.312 +val SOME t1 =
1.313 + parseNEW ctxt "get_denominator ((111::real) / 222)";
1.314 +val SOME t2 =
1.315 + parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
1.316 +\end{verbatim}
1.317 +
1.318 + \par \noindent Rewrite the terms using srls:\\
1.319 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
1.320 rewrite\_set\_ thy true srls t2;\\
1.321 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
1.322 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
1.323 - \emph{srls}:\\
1.324 -
1.325 - \par \noindent \ttfamily val srls = Rls \lbrace id =
1.326 - "srls\_InverseZTransform", rules =\\
1.327 - \lbrack Calc("Rational.get\_numerator",\\
1.328 - eval\_get\_numerator "Rational.get\_numerator"),\\
1.329 - Calc("Partial\_Fractions.factors\_from\_solution",\\
1.330 - eval\_factors\_from\_solution
1.331 - "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
1.332 -
1.333 - \par \noindent \normalfont Here everthing is perfect. So the error can
1.334 + \emph{srls}:
1.335 +\begin{verbatim}
1.336 + val srls =
1.337 + Rls{id = "srls_InverseZTransform",
1.338 + rules = [Calc("Rational.get_numerator",
1.339 + eval_get_numerator "Rational.get_numerator"),
1.340 + Calc("Partial_Fractions.factors_from_solution",
1.341 + eval_factors_from_solution
1.342 + "Partial_Fractions.factors_from_solution")]}
1.343 +\end{verbatim}
1.344 + \par \noindent Here everthing is perfect. So the error can
1.345 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
1.346 \normalfont We try to check the code with an existing test; since the
1.347 \emph{code} is in
1.348 @@ -1028,7 +1042,7 @@
1.349 \normalfont\end{center}
1.350 \par \noindent After updating the function \ttfamily
1.351 factors\_from\_solution \normalfont to a new version and putting a
1.352 - testcase to \ttfamily Partial\_Fractions.sml \normalfont we tried again
1.353 + test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
1.354 to evaluate the term with the same result.
1.355 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
1.356 everything is working fine. Also we checked that the test \ttfamily
1.357 @@ -1037,12 +1051,13 @@
1.358 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml"
1.359 \normalfont \end{center}
1.360 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of
1.361 - {\sisac} by evaluating\\
1.362 + {\sisac} by evaluating
1.363
1.364 - \par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace;
1.365 - \normalfont \\
1.366 +\begin{verbatim}
1.367 + val thy = \hyperlink{theory.Isac}{\mbox{\isa{Isac}}};
1.368 +\end{verbatim}
1.369
1.370 - \par \noindent \normalfont After rebuilding {\sisac} again it worked.%
1.371 + After rebuilding {\sisac} again it worked.%
1.372 \end{isamarkuptext}%
1.373 \isamarkuptrue%
1.374 %
1.375 @@ -1051,7 +1066,7 @@
1.376 \isamarkuptrue%
1.377 %
1.378 \begin{isamarkuptext}%
1.379 -\noindent In {\sisac}'s CTP-based programming language we can build
1.380 +\noindent In {\sisac}'s TP-based programming language we can build
1.381 expressions by:\\
1.382 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont%
1.383 \end{isamarkuptext}%
1.384 @@ -1065,7 +1080,7 @@
1.385 \isacommand{ML}\isamarkupfalse%
1.386 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.387 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.388 -\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ The\ main\ denominator\ is\ the\ multiplikation\ of\ the\ denominators\ of\isanewline
1.389 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ The\ main\ denominator\ is\ the\ multiplication\ of\ the\ denominators\ of\isanewline
1.390 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ all\ partial\ fractions{\isaliteral{2E}{\isachardot}}\isanewline
1.391 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.392 \ \ \ \isanewline
1.393 @@ -1089,7 +1104,7 @@
1.394 \isamarkuptrue%
1.395 %
1.396 \begin{isamarkuptext}%
1.397 -\noindent We use the Ansatz of the Partial Fraction Decomposen for our
1.398 +\noindent We use the Ansatz of the Partial Fraction Decomposition for our
1.399 expression 2nd order. Follow up the calculation in
1.400 Section~\ref{sec:calc:ztrans} Step~03.%
1.401 \end{isamarkuptext}%
1.402 @@ -1110,11 +1125,11 @@
1.403 \endisadelimML
1.404 %
1.405 \begin{isamarkuptext}%
1.406 -\noindent We define two aximatizations, the first one is the main ansatz,
1.407 - the next one is just an eqivalent transformation of the resulting
1.408 +\noindent We define two axiomatization, the first one is the main ansatz,
1.409 + the next one is just an equivalent transformation of the resulting
1.410 equation. Both axiomatizations were moved to \ttfamily
1.411 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
1.412 - programms it is possible to use the rulesets and the machine will find
1.413 + programs it is possible to use the rulesets and the machine will find
1.414 the correct ansatz and equivalent transformation itself.%
1.415 \end{isamarkuptext}%
1.416 \isamarkuptrue%
1.417 @@ -1124,7 +1139,7 @@
1.418 \ \ equival{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}nd{\isaliteral{5F}{\isacharunderscore}}order{\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}}n\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2A}{\isacharasterisk}}b\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2A}{\isacharasterisk}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.419 \begin{isamarkuptext}%
1.420 \noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
1.421 - our expression and get an equilation with our expression on the left
1.422 + our expression and get an equation with our expression on the left
1.423 and the partial fractions of it on the right hand side.%
1.424 \end{isamarkuptext}%
1.425 \isamarkuptrue%
1.426 @@ -1159,7 +1174,7 @@
1.427 \endisadelimML
1.428 %
1.429 \begin{isamarkuptext}%
1.430 -\noindent Eliminate the demoninators by multiplying the left and the
1.431 +\noindent Eliminate the denominators by multiplying the left and the
1.432 right hand side of the equation with the main denominator. This is an
1.433 simple equivalent transformation. Later on we use an own ruleset
1.434 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
1.435 @@ -1225,9 +1240,9 @@
1.436 \endisadelimML
1.437 %
1.438 \begin{isamarkuptext}%
1.439 -\noindent In Example~\ref{eg:gap} of my thesis I'm describin a problem about
1.440 +\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
1.441 simplifications. The problem that we would like to have only a specific degree
1.442 - of simplification occours right here, in the next step.%
1.443 + of simplification occurs right here, in the next step.%
1.444 \end{isamarkuptext}%
1.445 \isamarkuptrue%
1.446 %
1.447 @@ -1363,7 +1378,7 @@
1.448 \endisadelimML
1.449 %
1.450 \begin{isamarkuptext}%
1.451 -\noindent We apply the ruleset\lodts%
1.452 +\noindent We apply the ruleset\ldots%
1.453 \end{isamarkuptext}%
1.454 \isamarkuptrue%
1.455 %
1.456 @@ -1410,20 +1425,20 @@
1.457 %
1.458 \endisadelimML
1.459 %
1.460 -\isamarkupsubsubsection{Get the First Koeffizient%
1.461 +\isamarkupsubsubsection{Get the First Coefficient%
1.462 }
1.463 \isamarkuptrue%
1.464 %
1.465 \begin{isamarkuptext}%
1.466 -\noindent Now it's up to get the two koeffizients A and B, which will be
1.467 - the numerators of our partial fractions. Continiue following up the
1.468 +\noindent Now it's up to get the two coefficients A and B, which will be
1.469 + the numerators of our partial fractions. Continue following up the
1.470 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.%
1.471 \end{isamarkuptext}%
1.472 \isamarkuptrue%
1.473 %
1.474 \begin{isamarkuptext}%
1.475 -\noindent To get the first koeffizient we substitude $z$ with the first
1.476 - zeropoint we determined in section~\ref{sec:solveq}.%
1.477 +\noindent To get the first coefficient we substitute $z$ with the first
1.478 + zero-point we determined in Section~\ref{sec:solveq}.%
1.479 \end{isamarkuptext}%
1.480 \isamarkuptrue%
1.481 %
1.482 @@ -1452,7 +1467,7 @@
1.483 \ \ 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.484 \ \ 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.485 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.486 -\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Solve\ the\ simple\ linear\ equilation\ for\ A\ TODO{\isaliteral{3A}{\isacharcolon}}\isanewline
1.487 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Solve\ the\ simple\ linear\ equation\ for\ A{\isaliteral{3A}{\isacharcolon}}\isanewline
1.488 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{27}{\isacharprime}}s\isanewline
1.489 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.490 \ \ 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.491 @@ -1517,7 +1532,7 @@
1.492 %
1.493 \endisadelimML
1.494 %
1.495 -\isamarkupsubsubsection{Get Second Koeffizient%
1.496 +\isamarkupsubsubsection{Get Second Coefficient%
1.497 }
1.498 \isamarkuptrue%
1.499 %
1.500 @@ -1542,8 +1557,8 @@
1.501 \endisadelimML
1.502 %
1.503 \begin{isamarkuptext}%
1.504 -\noindent To get the second koeffizient we substitude $z$ with the second
1.505 - zeropoint we determined in section~\ref{sec:solveq}.%
1.506 +\noindent To get the second coefficient we substitute $z$ with the second
1.507 + zero-point we determined in Section~\ref{sec:solveq}.%
1.508 \end{isamarkuptext}%
1.509 \isamarkuptrue%
1.510 %
1.511 @@ -1637,7 +1652,7 @@
1.512 \begin{isamarkuptext}%
1.513 \noindent Now everything we need for solving the problem has been
1.514 tested out. We now start by creating new nodes for our methods and
1.515 - further on our new programm in the interpreter.%
1.516 + further on our new program in the interpreter.%
1.517 \end{isamarkuptext}%
1.518 \isamarkuptrue%
1.519 %
1.520 @@ -1648,7 +1663,7 @@
1.521 %
1.522 \begin{isamarkuptext}%
1.523 \noindent We define the fields \em filterExpression \normalfont and
1.524 - \em stepResponse \normalfont both as quations, they represent the in- and
1.525 + \em stepResponse \normalfont both as equations, they represent the in- and
1.526 output of the program.%
1.527 \end{isamarkuptext}%
1.528 \isamarkuptrue%
1.529 @@ -1662,7 +1677,7 @@
1.530 %
1.531 \begin{isamarkuptext}%
1.532 \noindent The next step is defining the specifications as nodes in the
1.533 - designated part. We have to create the hierachy node by node and start
1.534 + designated part. We have to create the hierarchy node by node and start
1.535 with \em SignalProcessing \normalfont and go on by creating the node
1.536 \em Z\_Transform\normalfont.%
1.537 \end{isamarkuptext}%
1.538 @@ -1691,8 +1706,8 @@
1.539 %
1.540 \begin{isamarkuptext}%
1.541 \noindent For the suddenly created node we have to define the input
1.542 - and output parameters. We already prepaired their definition in
1.543 - section~\ref{sec:deffdes}.%
1.544 + and output parameters. We already prepared their definition in
1.545 + Section~\ref{sec:deffdes}.%
1.546 \end{isamarkuptext}%
1.547 \isamarkuptrue%
1.548 %
1.549 @@ -1862,8 +1877,8 @@
1.550 \endisadelimML
1.551 %
1.552 \begin{isamarkuptext}%
1.553 -\noindent If yes we can get the method by steping backwards through
1.554 - the hierachy.%
1.555 +\noindent If yes we can get the method by stepping backwards through
1.556 + the hierarchy.%
1.557 \end{isamarkuptext}%
1.558 \isamarkuptrue%
1.559 %
1.560 @@ -1883,13 +1898,13 @@
1.561 %
1.562 \endisadelimML
1.563 %
1.564 -\isamarkupsection{Program in CTP-based language \label{prog-steps}%
1.565 +\isamarkupsection{Program in TP-based language \label{prog-steps}%
1.566 }
1.567 \isamarkuptrue%
1.568 %
1.569 \begin{isamarkuptext}%
1.570 -\noindent We start stepwise expanding our programm. The script is a
1.571 - simple string containing severell manipulation instructions.
1.572 +\noindent We start stepwise expanding our program. The script is a
1.573 + simple string containing several manipulation instructions.
1.574 \par The first script we try contains no instruction, we only test if
1.575 building scripts that way work.%
1.576 \end{isamarkuptext}%
1.577 @@ -1907,7 +1922,7 @@
1.578 \isacommand{ML}\isamarkupfalse%
1.579 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.580 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.581 -\ \ \ \ {\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.582 +\ \ \ \ {\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.583 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ Xeq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.584 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.585 \endisatagML
1.586 @@ -1931,16 +1946,16 @@
1.587 \isacommand{ML}\isamarkupfalse%
1.588 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.589 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.590 -\ \ \ \ {\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.591 +\ \ \ \ {\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.592 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.593 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\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}}\isanewline
1.594 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.595 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.596 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.597 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.598 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.599 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.600 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline
1.601 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.602 -\ \ \ \ {\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}}\isanewline
1.603 +\ \ \ \ {\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}}\isanewline
1.604 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.605 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline
1.606 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.607 @@ -1948,23 +1963,23 @@
1.608 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.609 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ NONE\isanewline
1.610 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.611 -\ \ \ \ {\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.612 +\ \ \ \ {\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.613 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.614 \ \ \ \ \ {\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}}\isanewline
1.615 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.616 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.617 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.618 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.619 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.620 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.621 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline
1.622 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.623 -\ \ \ \ {\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}}\isanewline
1.624 +\ \ \ \ {\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}}\isanewline
1.625 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.626 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline
1.627 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.628 -\ \ \ \ {\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}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.629 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.630 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.631 -\ \ \ \ {\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.632 +\ \ \ \ {\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}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.633 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.634 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.635 +\ \ \ \ {\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.636 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.637 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.638 \endisatagML
1.639 @@ -1975,7 +1990,7 @@
1.640 \endisadelimML
1.641 %
1.642 \begin{isamarkuptext}%
1.643 -\noindent To solve the equation it is neccessary to drop the left hand
1.644 +\noindent To solve the equation it is necessary to drop the left hand
1.645 side, now we only need the denominator of the right hand side. The first
1.646 equation solves the zeros of our expression.%
1.647 \end{isamarkuptext}%
1.648 @@ -1989,11 +2004,11 @@
1.649 \isacommand{ML}\isamarkupfalse%
1.650 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.651 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.652 -\ \ \ \ {\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.653 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.654 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.655 -\ \ \ \ {\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}}\isanewline
1.656 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
1.657 +\ \ \ \ {\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.658 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.659 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.660 +\ \ \ \ {\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}}\isanewline
1.661 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.662 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.663 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving\isanewline
1.664 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.665 @@ -2021,23 +2036,23 @@
1.666 \isacommand{ML}\isamarkupfalse%
1.667 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.668 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.669 -\ \ \ \ {\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}}\ \isanewline
1.670 -\ \ \ \ {\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.671 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
1.672 -\ \ \ \ {\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}}\ \isanewline
1.673 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.674 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.675 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
1.676 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline
1.677 +\ \ \ \ {\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}}\isanewline
1.678 +\ \ \ \ {\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.679 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.680 +\ \ \ \ {\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}}\isanewline
1.681 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.682 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.683 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.684 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.685 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.686 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\isanewline
1.687 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.688 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}equ{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.689 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.690 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.691 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.692 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.693 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.694 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}equ{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.695 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.696 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.697 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.698 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.699 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.700 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.701 \isanewline
1.702 \ \ parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.703 @@ -2064,45 +2079,45 @@
1.704 \isatagML
1.705 \isacommand{ML}\isamarkupfalse%
1.706 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.707 -\ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.708 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.709 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.710 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
1.711 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.712 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.713 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.714 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.715 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.716 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.717 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
1.718 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
1.719 +\ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.720 +\ \ \ \ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.721 +\ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.722 +\ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.723 +\ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
1.724 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.725 +\ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.726 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.727 +\ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.728 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.729 +\ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.730 +\ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
1.731 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
1.732 \isaantiq
1.733 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS{}%
1.734 \endisaantiq
1.735 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.736 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.737 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.738 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
1.739 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.740 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.741 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
1.742 \isaantiq
1.743 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}NIL{}%
1.744 \endisaantiq
1.745 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.746 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.747 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.748 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.749 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}argument{\isaliteral{5F}{\isacharunderscore}}in\ {\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.750 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.751 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.752 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.753 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.754 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.755 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline
1.756 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.757 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.758 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.759 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.760 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr\isanewline
1.761 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.762 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.763 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.764 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.765 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}argument{\isaliteral{5F}{\isacharunderscore}}in\ {\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.766 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.767 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.768 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.769 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.770 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.771 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline
1.772 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.773 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.774 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.775 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.776 +\ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.777 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.778 \endisatagML
1.779 {\isafoldML}%
1.780 @@ -2118,7 +2133,7 @@
1.781 \begin{isamarkuptext}%
1.782 \noindent After we also tested how to write scripts and run them,
1.783 we start creating the final version of our script and store it into
1.784 - the method for which we created a node in section~\ref{sec:cparentnode}
1.785 + the method for which we created a node in Section~\ref{sec:cparentnode}
1.786 Note that we also did this stepwise, but we didn't kept every
1.787 subversion.%
1.788 \end{isamarkuptext}%
1.789 @@ -2180,8 +2195,8 @@
1.790 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.791 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs\ {\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.792 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ \isanewline
1.793 -\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ prepare\ equliation\ for\ a\ {\isaliteral{2D}{\isacharminus}}\ eq{\isaliteral{5F}{\isacharunderscore}}a\isanewline
1.794 -\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ therfor\ subsitude\ z\ with\ solution\ {\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ z{\isadigit{1}}\isanewline
1.795 +\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ prepare\ equation\ for\ a\ {\isaliteral{2D}{\isacharminus}}\ eq{\isaliteral{5F}{\isacharunderscore}}a\isanewline
1.796 +\ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ therefor\ substitute\ z\ with\ solution\ {\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ z{\isadigit{1}}\isanewline
1.797 \ \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.798 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs\ {\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{2}}\ L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.799 \ \isanewline
1.800 @@ -2205,16 +2220,14 @@
1.801 \isanewline
1.802 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.803 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}pbz{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ eqr{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.804 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.805 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}B{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.806 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.807 \isanewline
1.808 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.809 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.810 \isanewline
1.811 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}iztrans{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.812 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ inverse{\isaliteral{5F}{\isacharunderscore}}z\ False{\isaliteral{29}{\isacharparenright}}\ iztrans{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.813 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ iztrans{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.814 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}n\ {\isaliteral{3D}{\isacharequal}}\ iztrans{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\ \isanewline
1.815 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z\ {\isaliteral{3D}{\isacharequal}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.816 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ inverse{\isaliteral{5F}{\isacharunderscore}}z\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.817 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ n{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ n{\isaliteral{5F}{\isacharunderscore}}eq\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
1.818 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
1.819 \ \ \ \ {\isaliteral{29}{\isacharparenright}}\isanewline
1.820 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.821 @@ -2241,7 +2254,7 @@
1.822 %
1.823 \begin{isamarkuptext}%
1.824 \noindent First we want to check the formalization of the in and
1.825 - output of our programm.%
1.826 + output of our program.%
1.827 \end{isamarkuptext}%
1.828 \isamarkuptrue%
1.829 %
1.830 @@ -2295,7 +2308,7 @@
1.831 \isamarkuptrue%
1.832 %
1.833 \begin{isamarkuptext}%
1.834 -\noindent We start to stepwise execute our new programm in a calculation
1.835 +\noindent We start to stepwise execute our new program in a calculation
1.836 tree and check if every node implements that what we have wanted.%
1.837 \end{isamarkuptext}%
1.838 \isamarkuptrue%
1.839 @@ -2355,32 +2368,34 @@
1.840 \noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1.841 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1.842 the following points:\begin{itemize}
1.843 - \item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\
1.844 - \ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 /
1.845 - (-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\
1.846 + \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1.847 +\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1.848 The calculation is ok but no \ttfamily next \normalfont step found:
1.849 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1.850 \item What shows \ttfamily trace\_script := true; \normalfont we read
1.851 - bottom up\ldots\\
1.852 - \ttfamily @@@next leaf 'SubProbfrom\\
1.853 - (PolyEq',\\
1.854 - \lbrack abcFormula, degree\_2, polynomial, univariate,
1.855 - equation\rbrack,\\
1.856 - no\_meth)\\
1.857 - \lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\
1.858 - (PolyEq',\\
1.859 - [abcFormula, degree\_2, polynomial, univariate, equation],\\
1.860 - no\_meth)\\
1.861 - \lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0),
1.862 - REAL z\rbrack'\normalfont\\
1.863 + bottom up\ldots
1.864 + \begin{verbatim}
1.865 + @@@next leaf 'SubProblem
1.866 + (PolyEq',[abcFormula, degree_2, polynomial,
1.867 + univariate, equation], no_meth)
1.868 + [BOOL equ, REAL z]'
1.869 + ---> STac 'SubProblem (PolyEq',
1.870 + [abcFormula, degree_2, polynomial,
1.871 + univariate, equation], no_meth)
1.872 + [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]'
1.873 + \end{verbatim}
1.874 We see the SubProblem with correct arguments from searching next
1.875 step (program text !!!--->!!! STac (script tactic) with arguments
1.876 evaluated.)
1.877 \item Do we have the right Script \ldots difference in the
1.878 - argumentsdifference in the arguments\ldots\\
1.879 - \ttfamily val Script s =\\
1.880 - (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
1.881 - writeln (term2str s);\normalfont\\
1.882 + arguments in the arguments\ldots
1.883 + \begin{verbatim}
1.884 + val Script s =
1.885 + (#scr o get_met) ["SignalProcessing",
1.886 + "Z_Transform",
1.887 + "inverse"];
1.888 + writeln (term2str s);
1.889 + \end{verbatim}
1.890 \ldots shows the right script. Difference in the arguments.
1.891 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1.892 no\_meth by [no\_meth] \normalfont in Script
1.893 @@ -2410,7 +2425,7 @@
1.894 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1.895 considered the following points:\begin{itemize}
1.896 \item Difference in the arguments
1.897 - \item Comparison with subsection~ref{sec:solveq}: There solving this
1.898 + \item Comparison with Subsection~\ref{sec:solveq}: There solving this
1.899 equation works, so there must be some difference in the arguments
1.900 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1.901 instead of \ttfamily [no\_met] \normalfont ;-)
1.902 @@ -2448,14 +2463,16 @@
1.903 \item Was there an error message? NO -- ok
1.904 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
1.905 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
1.906 - \item What is the returned formula:
1.907 - \ttfamily print\_depth 999; f; print\_depth 999;\\
1.908 - \lbrace Find = \lbrack Correct "solutions z\_i"\rbrack,
1.909 - With = \lbrack\rbrack,\\
1.910 - Given = \lbrack Correct "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)",
1.911 - Correct "solveFor z"\rbrack,\\
1.912 - Where = \lbrack \ldots \rbrack,
1.913 - Relate = \lbrack\rbrack\rbrace $ \normalfont\\
1.914 + \item What is the returned formula:
1.915 +\begin{verbatim}
1.916 +print_depth 999; f; print_depth 999;
1.917 +{ Find = [ Correct "solutions z_i"],
1.918 + With = [],
1.919 + Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1.920 + Correct "solveFor z"],
1.921 + Where = [...],
1.922 + Relate = [] }
1.923 +\end{verbatim}
1.924 \normalfont The only False is the reason: the Where (the precondition) is
1.925 False for good reasons: The precondition seems to check for linear
1.926 equations, not for the one we want to solve! Removed this error by
1.927 @@ -2595,27 +2612,116 @@
1.928 \end{isamarkuptext}%
1.929 \isamarkuptrue%
1.930 %
1.931 -\isadelimML
1.932 -%
1.933 -\endisadelimML
1.934 -%
1.935 -\isatagML
1.936 -\isacommand{ML}\isamarkupfalse%
1.937 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.938 -\ \ trace{\isaliteral{5F}{\isacharunderscore}}script\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.939 -\ \ 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.940 -\ \ show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.941 -{\isaliteral{2A7D}{\isacharverbatimclose}}%
1.942 -\endisatagML
1.943 -{\isafoldML}%
1.944 -%
1.945 -\isadelimML
1.946 -%
1.947 -\endisadelimML
1.948 -\isanewline
1.949 +\isamarkupsection{Improve and Transfer into Knowledge%
1.950 +}
1.951 +\isamarkuptrue%
1.952 +%
1.953 +\begin{isamarkuptext}%
1.954 +We want to improve the very long program \ttfamily InverseZTransform
1.955 + \normalfont by modularisation: partial fraction decomposition shall
1.956 + become a sub-problem.
1.957 +
1.958 + We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
1.959 + \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
1.960 + \normalfont and then modularise. In this case TODO problems?!?
1.961 +
1.962 + We chose another way and go bottom up: first we build the sub-problem in
1.963 + \ttfamily Partial\_Fractions.thy \normalfont with the term:
1.964 +
1.965 + $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$
1.966 +
1.967 + \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
1.968 + and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
1.969 + \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1.970 + \normalfont and the respective tests to:
1.971 + \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}%
1.972 +\end{isamarkuptext}%
1.973 +\isamarkuptrue%
1.974 +%
1.975 +\isamarkupsubsection{Transfer to Partial\_Fractions.thy%
1.976 +}
1.977 +\isamarkuptrue%
1.978 +%
1.979 +\begin{isamarkuptext}%
1.980 +First we transfer both, knowledge and tests into:
1.981 + \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1.982 + in order to immediately have the test results.
1.983 +
1.984 + We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
1.985 + ansatz\_2nd\_order \normalfont and rule-sets --- no problem.
1.986 +
1.987 + Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac"
1.988 + \normalfont is easy.
1.989 +
1.990 + But then we copy from:\\
1.991 + (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1.992 + \normalfont\\ to\\
1.993 + (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
1.994 + \normalfont\\ and cut out the respective part from the program. First we ensure that
1.995 + the string is correct. When we insert the string into (2)
1.996 + \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.%
1.997 +\end{isamarkuptext}%
1.998 +\isamarkuptrue%
1.999 +%
1.1000 +\isamarkupsubsubsection{'Programming' in ISAC's TP-based Language%
1.1001 +}
1.1002 +\isamarkuptrue%
1.1003 +%
1.1004 +\begin{isamarkuptext}%
1.1005 +At the present state writing programs in {\sisac} is particularly cumbersome.
1.1006 + So we give hints how to cope with the many obstacles. Below we describe the
1.1007 + steps we did in making (2) run.
1.1008 +
1.1009 + \begin{enumerate}
1.1010 + \item We check if the \textbf{string} containing the program is correct.
1.1011 + \item We check if the \textbf{types in the program} are correct.
1.1012 + For this purpose we start start with the first and last lines
1.1013 + \begin{verbatim}
1.1014 + "PartFracScript (f_f::real) (v_v::real) = " ^
1.1015 + " (let X = Take f_f; " ^
1.1016 + " pbz = ((Substitute []) X) " ^
1.1017 + " in pbz)"
1.1018 + \end{verbatim}
1.1019 + The last but one line helps not to bother with ';'.
1.1020 + \item Then we add line by line. Already the first line causes the error.
1.1021 + So we investigate it by
1.1022 + \begin{verbatim}
1.1023 + val ctxt = ProofContext.init_global @ { theory } ;
1.1024 + val SOME t =
1.1025 + parseNEW ctxt "(num_orig::real) =
1.1026 + get_numerator(rhs f_f)";
1.1027 + \end{verbatim}
1.1028 + and see a type clash: \ttfamily rhs \normalfont from (1) requires type
1.1029 + \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real).
1.1030 + \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
1.1031 + \item Type-checking can be very tedious. One might even inspect the
1.1032 + parse-tree of the program with {\sisac}'s specific debug tools:
1.1033 + \begin{verbatim}
1.1034 + val {scr = Script t,...} =
1.1035 + get_met ["simplification",
1.1036 + "of_rationals",
1.1037 + "to_partial_fraction"];
1.1038 + atomty_thy @ { theory } t ;
1.1039 + \end{verbatim}
1.1040 + \item We check if the \textbf{semantics of the program} by stepwise evaluation
1.1041 + of the program. Evaluation is done by the Lucas-Interpreter, which works
1.1042 + using the knowledge in theory Isac; so we have to re-build Isac. And the
1.1043 + test are performed simplest in a file which is loaded with Isac.
1.1044 + See \ttfamily tests/../partial\_fractions.sml \normalfont.
1.1045 + \end{enumerate}%
1.1046 +\end{isamarkuptext}%
1.1047 +\isamarkuptrue%
1.1048 +%
1.1049 +\isamarkupsubsection{Transfer to Inverse\_Z\_Transform.thy%
1.1050 +}
1.1051 +\isamarkuptrue%
1.1052 +%
1.1053 +\begin{isamarkuptext}%
1.1054 +Unfortunately it was not possible to complete this task. Because we ran out of time\ldots%
1.1055 +\end{isamarkuptext}%
1.1056 +\isamarkuptrue%
1.1057 %
1.1058 \isadelimtheory
1.1059 -\isanewline
1.1060 %
1.1061 \endisadelimtheory
1.1062 %