changeset 42368 | 3afe632cd527 |
parent 42365 | 872589b4852c |
child 42369 | 3fa947c99a28 |
1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Feb 13 17:40:30 2012 +0100 1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue Feb 14 22:55:03 2012 +0100 1.3 @@ -21,18 +21,26 @@ 1.4 \endisadelimtheory 1.5 % 1.6 \begin{isamarkuptext}% 1.7 -We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise. 1.8 - Because subsection "Stepwise Check the Program" requires 1.9 - \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed 1.10 - from "theory Inverse_Z_Transform imports Isac begin.." to the above. 1.11 - 1.12 - ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS: 1.13 +We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an 1.14 + exercise. Because subsection~\ref{sec:stepcheck} requires 1.15 + \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily 1.16 + Isac.thy\normalfont, the setup has been changed from \ttfamily theory 1.17 + Inverse\_Z\_Transform imports Isac \normalfont to the above one. 1.18 + \par \noindent 1.19 + \begin{center} 1.20 + \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS} 1.21 + \end{center} 1.22 Here in this theory there are the internal names twice, for instance we have 1.23 - (Thm.derivation_name \isa{rule{\isadigit{1}}} = "Build_Inverse_Z_Transform.rule1") = true; 1.24 - but actually in us will be "Inverse_Z_Transform.rule1"% 1.25 + \ttfamily (Thm.derivation\_name \isa{rule{\isadigit{1}}} = "Build\_Inverse\_Z\_Transform.rule1") = true; 1.26 + \normalfont 1.27 + but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont% 1.28 \end{isamarkuptext}% 1.29 \isamarkuptrue% 1.30 % 1.31 +\isamarkupsection{Trials towards the Z-Transform\label{sec:trials}% 1.32 +} 1.33 +\isamarkuptrue% 1.34 +% 1.35 \isadelimML 1.36 % 1.37 \endisadelimML 1.38 @@ -51,19 +59,15 @@ 1.39 % 1.40 \endisadelimML 1.41 % 1.42 -\isamarkupsection{trials towards Z transform% 1.43 +\isamarkupsubsection{Notations and Terms% 1.44 } 1.45 \isamarkuptrue% 1.46 % 1.47 \begin{isamarkuptext}% 1.48 -===============================% 1.49 +\noindent Try which notations we are able to use.% 1.50 \end{isamarkuptext}% 1.51 \isamarkuptrue% 1.52 % 1.53 -\isamarkupsubsection{terms% 1.54 -} 1.55 -\isamarkuptrue% 1.56 -% 1.57 \isadelimML 1.58 % 1.59 \endisadelimML 1.60 @@ -71,66 +75,83 @@ 1.61 \isatagML 1.62 \isacommand{ML}\isamarkupfalse% 1.63 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.64 -% 1.65 +\ \ % 1.66 \isaantiq 1.67 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}{}% 1.68 \endisaantiq 1.69 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.70 -% 1.71 +\ \ % 1.72 \isaantiq 1.73 term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{}% 1.74 \endisaantiq 1.75 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.76 -% 1.77 +\ \ % 1.78 \isaantiq 1.79 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{}% 1.80 \endisaantiq 1.81 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.82 -% 1.83 +\ \ % 1.84 \isaantiq 1.85 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}% 1.86 \endisaantiq 1.87 {\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}\ {\isaliteral{5D}{\isacharbrackright}}\ denotes\ lists\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.88 -% 1.89 +\ \ % 1.90 \isaantiq 1.91 term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}% 1.92 \endisaantiq 1.93 {\isaliteral{3B}{\isacharsemicolon}}Isac\isanewline 1.94 -% 1.95 +\ \ % 1.96 \isaantiq 1.97 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}% 1.98 \endisaantiq 1.99 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.100 -term{\isadigit{2}}str\ % 1.101 +\ \ term{\isadigit{2}}str\ % 1.102 \isaantiq 1.103 term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}% 1.104 \endisaantiq 1.105 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.106 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.107 +{\isaliteral{2A7D}{\isacharverbatimclose}}% 1.108 +\endisatagML 1.109 +{\isafoldML}% 1.110 +% 1.111 +\isadelimML 1.112 +% 1.113 +\endisadelimML 1.114 +% 1.115 +\begin{isamarkuptext}% 1.116 +\noindent Try which symbols we are able to use and how we generate them.% 1.117 +\end{isamarkuptext}% 1.118 +\isamarkuptrue% 1.119 +% 1.120 +\isadelimML 1.121 +% 1.122 +\endisadelimML 1.123 +% 1.124 +\isatagML 1.125 \isacommand{ML}\isamarkupfalse% 1.126 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.127 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.128 -% 1.129 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.130 +\ \ % 1.131 \isaantiq 1.132 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{22}{\isachardoublequote}}{}% 1.133 \endisaantiq 1.134 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.135 -% 1.136 +\ \ % 1.137 \isaantiq 1.138 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{22}{\isachardoublequote}}{}% 1.139 \endisaantiq 1.140 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.141 -% 1.142 +\ \ % 1.143 \isaantiq 1.144 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{22}{\isachardoublequote}}{}% 1.145 \endisaantiq 1.146 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.147 -% 1.148 +\ \ % 1.149 \isaantiq 1.150 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}% 1.151 \endisaantiq 1.152 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.153 -term{\isadigit{2}}str\ % 1.154 +\ \ term{\isadigit{2}}str\ % 1.155 \isaantiq 1.156 term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}% 1.157 \endisaantiq 1.158 @@ -143,7 +164,7 @@ 1.159 % 1.160 \endisadelimML 1.161 % 1.162 -\isamarkupsubsection{rules% 1.163 +\isamarkupsubsection{Rules% 1.164 } 1.165 \isamarkuptrue% 1.166 \isacommand{axiomatization}\isamarkupfalse% 1.167 @@ -153,7 +174,12 @@ 1.168 \ \ rule{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ \isanewline 1.169 \ \ rule{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline 1.170 \ \ rule{\isadigit{5}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline 1.171 -\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline 1.172 +\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}% 1.173 +\begin{isamarkuptext}% 1.174 +\noindent Check the rules for their correct notation. 1.175 + (See the machine output.)% 1.176 +\end{isamarkuptext}% 1.177 +\isamarkuptrue% 1.178 % 1.179 \isadelimML 1.180 % 1.181 @@ -162,22 +188,22 @@ 1.182 \isatagML 1.183 \isacommand{ML}\isamarkupfalse% 1.184 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.185 -% 1.186 +\ \ % 1.187 \isaantiq 1.188 thm\ rule{\isadigit{1}}{}% 1.189 \endisaantiq 1.190 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.191 -% 1.192 +\ \ % 1.193 \isaantiq 1.194 thm\ rule{\isadigit{2}}{}% 1.195 \endisaantiq 1.196 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.197 -% 1.198 +\ \ % 1.199 \isaantiq 1.200 thm\ rule{\isadigit{3}}{}% 1.201 \endisaantiq 1.202 {\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.203 -% 1.204 +\ \ % 1.205 \isaantiq 1.206 thm\ rule{\isadigit{4}}{}% 1.207 \endisaantiq 1.208 @@ -190,7 +216,112 @@ 1.209 % 1.210 \endisadelimML 1.211 % 1.212 -\isamarkupsubsection{apply rules% 1.213 +\isamarkupsubsection{Apply Rules% 1.214 +} 1.215 +\isamarkuptrue% 1.216 +% 1.217 +\begin{isamarkuptext}% 1.218 +\noindent We try to apply the rules to a given expression.% 1.219 +\end{isamarkuptext}% 1.220 +\isamarkuptrue% 1.221 +% 1.222 +\isadelimML 1.223 +% 1.224 +\endisadelimML 1.225 +% 1.226 +\isatagML 1.227 +\isacommand{ML}\isamarkupfalse% 1.228 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.229 +\ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline 1.230 +\ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.231 +\isaantiq 1.232 +thm\ rule{\isadigit{3}}{}% 1.233 +\endisaantiq 1.234 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline 1.235 +\ \ \ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.236 +\isaantiq 1.237 +thm\ rule{\isadigit{4}}{}% 1.238 +\endisaantiq 1.239 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline 1.240 +\ \ \ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.241 +\isaantiq 1.242 +thm\ rule{\isadigit{1}}{}% 1.243 +\endisaantiq 1.244 +{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline 1.245 +\ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.246 +\isanewline 1.247 +\ \ val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.248 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.249 +\ \ term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.250 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline 1.251 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Attention\ rule{\isadigit{1}}\ is\ applied\ before\ the\ expression\ is\ \isanewline 1.252 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ checked\ for\ rule{\isadigit{4}}\ which\ would\ be\ correct{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}\isanewline 1.253 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.254 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.255 +\isanewline 1.256 +\isacommand{ML}\isamarkupfalse% 1.257 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}% 1.258 +\isaantiq 1.259 +theory\ Isac{}% 1.260 +\endisaantiq 1.261 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.262 +\isacommand{ML}\isamarkupfalse% 1.263 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.264 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.265 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.266 +\isaantiq 1.267 +thm\ rule{\isadigit{3}}{}% 1.268 +\endisaantiq 1.269 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.270 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.271 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.272 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.273 +\isanewline 1.274 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.275 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.276 +\isaantiq 1.277 +thm\ rule{\isadigit{4}}{}% 1.278 +\endisaantiq 1.279 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.280 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.281 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.282 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.283 +\isanewline 1.284 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.285 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.286 +\isaantiq 1.287 +thm\ rule{\isadigit{1}}{}% 1.288 +\endisaantiq 1.289 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.290 +\ \ term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.291 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.292 +\ \ term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.293 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.294 +\isacommand{ML}\isamarkupfalse% 1.295 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.296 +\endisatagML 1.297 +{\isafoldML}% 1.298 +% 1.299 +\isadelimML 1.300 +% 1.301 +\endisadelimML 1.302 +% 1.303 +\isamarkupsection{Prepare Steps for CTP-based programming Language\label{sec:prepstep}% 1.304 +} 1.305 +\isamarkuptrue% 1.306 +% 1.307 +\begin{isamarkuptext}% 1.308 +\par \noindent The following sections are challanging with the CTP-based 1.309 + possibilities of building the programm. The goal is realized in 1.310 + Section~\ref{spec-meth} and Section~\ref{prog-steps}. 1.311 + \par The reader is advised to jump between the subsequent subsections and 1.312 + the respective steps in Section~\ref{prog-steps}. By comparing 1.313 + Section~\ref{sec:calc:ztrans} the calculation can be comprehended step 1.314 + by step.% 1.315 +\end{isamarkuptext}% 1.316 +\isamarkuptrue% 1.317 +% 1.318 +\isamarkupsubsection{Prepare Expression\label{prep-expr}% 1.319 } 1.320 \isamarkuptrue% 1.321 % 1.322 @@ -201,68 +332,21 @@ 1.323 \isatagML 1.324 \isacommand{ML}\isamarkupfalse% 1.325 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.326 -val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline 1.327 -\ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.328 -\isaantiq 1.329 -thm\ rule{\isadigit{3}}{}% 1.330 -\endisaantiq 1.331 -{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline 1.332 -\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.333 -\isaantiq 1.334 -thm\ rule{\isadigit{4}}{}% 1.335 -\endisaantiq 1.336 -{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline 1.337 -\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.338 -\isaantiq 1.339 -thm\ rule{\isadigit{1}}{}% 1.340 -\endisaantiq 1.341 -{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline 1.342 -\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.343 -\isanewline 1.344 -val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.345 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.346 -term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}attention\ rule{\isadigit{1}}\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.347 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.348 -\isacommand{ML}\isamarkupfalse% 1.349 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.350 -val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}% 1.351 +\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ % 1.352 \isaantiq 1.353 theory\ Isac{}% 1.354 \endisaantiq 1.355 -{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.356 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.357 -\isacommand{ML}\isamarkupfalse% 1.358 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.359 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.360 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.361 +\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}% 1.362 \isaantiq 1.363 -thm\ rule{\isadigit{3}}{}% 1.364 +term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}% 1.365 \endisaantiq 1.366 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.367 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.368 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.369 -\isacommand{ML}\isamarkupfalse% 1.370 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.371 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.372 -\isaantiq 1.373 -thm\ rule{\isadigit{4}}{}% 1.374 -\endisaantiq 1.375 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.376 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.377 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.378 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.379 -\isacommand{ML}\isamarkupfalse% 1.380 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.381 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ % 1.382 -\isaantiq 1.383 -thm\ rule{\isadigit{1}}{}% 1.384 -\endisaantiq 1.385 -{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.386 -term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.387 -term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.388 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.389 -\isacommand{ML}\isamarkupfalse% 1.390 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.391 -terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.392 +{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.393 +\isanewline 1.394 +\ \ val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.395 +\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.396 +\ \ val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.397 +\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.398 {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.399 \endisatagML 1.400 {\isafoldML}% 1.401 @@ -271,54 +355,17 @@ 1.402 % 1.403 \endisadelimML 1.404 % 1.405 -\isamarkupsection{Prepare steps for CTP-based programming language% 1.406 +\isamarkupsubsubsection{Prepare Numerator and Denominator% 1.407 } 1.408 \isamarkuptrue% 1.409 % 1.410 \begin{isamarkuptext}% 1.411 -TODO insert Calculation (Referenz?!) 1.412 - 1.413 -The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps} 1.414 - 1.415 -the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}% 1.416 +\noindent The partial fraction decomposion is only possible ig we 1.417 + get the bound variable out of the numerator. Therefor we divide 1.418 + the expression by $z$. Follow up the Calculation at 1.419 + Section~\ref{sec:calc:ztrans} line number 02.% 1.420 \end{isamarkuptext}% 1.421 \isamarkuptrue% 1.422 -% 1.423 -\isamarkupsubsection{prepare expression \label{prep-expr}% 1.424 -} 1.425 -\isamarkuptrue% 1.426 -% 1.427 -\isadelimML 1.428 -% 1.429 -\endisadelimML 1.430 -% 1.431 -\isatagML 1.432 -\isacommand{ML}\isamarkupfalse% 1.433 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.434 -val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ % 1.435 -\isaantiq 1.436 -theory\ Isac{}% 1.437 -\endisaantiq 1.438 -{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.439 -val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}% 1.440 -\isaantiq 1.441 -term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}% 1.442 -\endisaantiq 1.443 -{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.444 -\isanewline 1.445 -val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.446 -val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.447 -{\isaliteral{2A7D}{\isacharverbatimclose}}% 1.448 -\endisatagML 1.449 -{\isafoldML}% 1.450 -% 1.451 -\isadelimML 1.452 -% 1.453 -\endisadelimML 1.454 -% 1.455 -\isamarkupsubsubsection{multply with z% 1.456 -} 1.457 -\isamarkuptrue% 1.458 \isacommand{axiomatization}\isamarkupfalse% 1.459 \ \isakeyword{where}\isanewline 1.460 \ \ ruleZY{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline 1.461 @@ -331,34 +378,45 @@ 1.462 \isatagML 1.463 \isacommand{ML}\isamarkupfalse% 1.464 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.465 -val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}% 1.466 +\ \ val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}% 1.467 \isaantiq 1.468 theory\ Isac{}% 1.469 \endisaantiq 1.470 {\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.471 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ % 1.472 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.473 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ % 1.474 \isaantiq 1.475 thm\ ruleZY{}% 1.476 \endisaantiq 1.477 \ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.478 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ % 1.479 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.480 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ % 1.481 \isaantiq 1.482 thm\ ruleZY{}% 1.483 \endisaantiq 1.484 \ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.485 \isanewline 1.486 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ % 1.487 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.488 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ % 1.489 \isaantiq 1.490 theory\ Isac{}% 1.491 \endisaantiq 1.492 \ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.493 -term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ TODO{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.494 -val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ % 1.495 +\ \ term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.496 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline 1.497 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ Fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.498 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ We\ solve\ this\ problem\ by\ using\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}x\ as\ a\ workaround{\isaliteral{2E}{\isachardot}}\isanewline 1.499 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.500 +\ \ val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.501 +\ \ \ \ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ % 1.502 \isaantiq 1.503 theory\ Isac{}% 1.504 \endisaantiq 1.505 \ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.506 -term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.507 +\ \ term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.508 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline 1.509 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}\ OK\ {\isaliteral{2D}{\isacharminus}}\ workaround{\isaliteral{21}{\isacharbang}}\isanewline 1.510 +\ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.511 {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.512 \endisatagML 1.513 {\isafoldML}% 1.514 @@ -367,21 +425,26 @@ 1.515 % 1.516 \endisadelimML 1.517 % 1.518 -\isamarkupsubsubsection{get argument of X': z is the variable the equation is solved for% 1.519 +\isamarkupsubsubsection{Get the Argument of the Expression X'% 1.520 } 1.521 \isamarkuptrue% 1.522 % 1.523 \begin{isamarkuptext}% 1.524 -grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,... 1.525 - 1.526 -grep -r "fun eva_" ... shows all functions witch can be used in a script. 1.527 -lookup this files how to build and handle such functions. 1.528 - 1.529 -the next section shows how to introduce such a function.% 1.530 +\noindent We use \texttt{grep} for finding possibilities how we can 1.531 + extract the bound variable in the expression. \ttfamily Atools.thy, 1.532 + Tools.thy \normalfont contain general utilities: \ttfamily 1.533 + eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont 1.534 + \ttfamily grep -r "fun eva\_" * \normalfont shows all functions 1.535 + witch can be used in a script. Lookup this files how to build 1.536 + and handle such functions. 1.537 + \par The next section shows how to introduce such a function.% 1.538 \end{isamarkuptext}% 1.539 \isamarkuptrue% 1.540 % 1.541 -\isamarkupsubsubsection{Decompose given term into lhs = rhs% 1.542 +\isamarkupsubsubsection{Decompose the Given Term Into lhs and rhs\footnote{Note: 1.543 + lhs means \em Left Hand Side \normalfont and rhs means 1.544 + \em Right Hand Side \normalfont and indicates the left or 1.545 + the right part of an equation.}% 1.546 } 1.547 \isamarkuptrue% 1.548 % 1.549 @@ -393,7 +456,8 @@ 1.550 \isacommand{ML}\isamarkupfalse% 1.551 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.552 \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ expr{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.553 -\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}bin\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}type{\isaliteral{5F}{\isacharunderscore}}of\ expr{\isaliteral{29}{\isacharparenright}}\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.554 +\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.555 +\ \ \ \ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}bin\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}type{\isaliteral{5F}{\isacharunderscore}}of\ expr{\isaliteral{29}{\isacharparenright}}\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.556 \ \ term{\isadigit{2}}str\ denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.557 {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.558 \endisatagML 1.559 @@ -404,17 +468,18 @@ 1.560 \endisadelimML 1.561 % 1.562 \begin{isamarkuptext}% 1.563 -we have rhs in the Script language, but we need a function 1.564 - which gets the denominator of a fraction% 1.565 +\noindent We have rhs in the Script language, but we need a function 1.566 + which gets the denominator of a fraction.% 1.567 \end{isamarkuptext}% 1.568 \isamarkuptrue% 1.569 % 1.570 -\isamarkupsubsubsection{get the denominator and numerator out of a fraction% 1.571 +\isamarkupsubsubsection{Get the Denominator and Numerator out of a Fraction% 1.572 } 1.573 \isamarkuptrue% 1.574 % 1.575 \begin{isamarkuptext}% 1.576 -get denominator should become a constant for the isabelle parser:% 1.577 +\noindent The selv written functions in e.g. \texttt{get\_denominator} 1.578 + should become a constant for the isabelle parser:% 1.579 \end{isamarkuptext}% 1.580 \isamarkuptrue% 1.581 \isacommand{consts}\isamarkupfalse% 1.582 @@ -422,11 +487,14 @@ 1.583 \ \ get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}\isanewline 1.584 \ \ get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}% 1.585 \begin{isamarkuptext}% 1.586 -With the above definition we run into problems with parsing the Script InverseZTransform: 1.587 - This leads to "ambiguous parse trees" and we avoid this by shifting the definition 1.588 - to Rational.thy and re-building Isac. 1.589 - ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch; 1.590 - it only works due to re-building Isac several times (indicated explicityl).% 1.591 +\noindent With the above definition we run into problems when we parse 1.592 + the Script \texttt{InverseZTransform}. This leads to \em ambiguous 1.593 + parse trees. \normalfont We avoid this by moving the definition 1.594 + to \ttfamily Rational.thy \normalfont and re-building Isac. 1.595 + \par \noindent ATTENTION: From now on \ttfamily 1.596 + Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch; 1.597 + it only works due to re-building Isac several times (indicated 1.598 + explicityl).% 1.599 \end{isamarkuptext}% 1.600 \isamarkuptrue% 1.601 % 1.602 @@ -437,16 +505,19 @@ 1.603 \isatagML 1.604 \isacommand{ML}\isamarkupfalse% 1.605 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.606 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.607 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline 1.608 +\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline 1.609 +\ {\isaliteral{2A}{\isacharasterisk}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.610 +\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.611 fun\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ \isanewline 1.612 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline 1.613 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ num\ {\isaliteral{24}{\isachardollar}}\isanewline 1.614 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\ \isanewline 1.615 \ \ \ \ \ \ \ \ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline 1.616 -\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline 1.617 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isanewline 1.618 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline 1.619 \ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline 1.620 \ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline 1.621 -\isanewline 1.622 {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.623 \endisatagML 1.624 {\isafoldML}% 1.625 @@ -704,7 +775,7 @@ 1.626 \ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.627 fun\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ s\ {\isaliteral{3D}{\isacharequal}}\isanewline 1.628 \ \ let\ val\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s\isanewline 1.629 -\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ flip{\isaliteral{5F}{\isacharunderscore}}sign\ rhs{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.630 +\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.631 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.632 \isacommand{ML}\isamarkupfalse% 1.633 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.634 @@ -1569,8 +1640,6 @@ 1.635 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline 1.636 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ eq{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{2C}{\isacharcomma}}\ REAL\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.637 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.638 -{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}aarg{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.639 -\isanewline 1.640 \isanewline 1.641 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.642 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq{\isaliteral{5F}{\isacharunderscore}}b\ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}zzz{\isaliteral{3D}{\isacharequal}}z{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.643 @@ -1578,15 +1647,23 @@ 1.644 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}sol{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline 1.645 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline 1.646 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ eq{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{2C}{\isacharcomma}}\ REAL\ {\isaliteral{28}{\isacharparenleft}}B{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.647 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rhs{\isaliteral{28}{\isacharparenleft}}NTH\ {\isadigit{1}}\ sol{\isaliteral{5F}{\isacharunderscore}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.648 \isanewline 1.649 +\isanewline 1.650 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.651 \ \ \ \ \ \ {\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.652 +\ \ \ \ \ \ {\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.653 +\ \ \ \ \ \ {\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.654 +\isanewline 1.655 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.656 \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.657 \isanewline 1.658 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}pbz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.659 +\ \ \ \ \ \ {\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.660 +\ \ \ \ \ \ {\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.661 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ iztrans{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.662 +\ \ \ \ \ \ {\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.663 \isanewline 1.664 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ pbz{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline 1.665 -\isanewline 1.666 -\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline 1.667 +\ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline 1.668 \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline 1.669 {\isaliteral{2A7D}{\isacharverbatimclose}}% 1.670 \endisatagML 1.671 @@ -1634,7 +1711,7 @@ 1.672 % 1.673 \endisadelimML 1.674 % 1.675 -\isamarkupsubsubsection{Stepwise check the program% 1.676 +\isamarkupsubsubsection{Stepwise check the program\label{sec:stepcheck}% 1.677 } 1.678 \isamarkuptrue% 1.679 % 1.680 @@ -1902,6 +1979,11 @@ 1.681 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.682 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.683 \isanewline 1.684 +\isacommand{ML}\isamarkupfalse% 1.685 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 1.686 +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.687 +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.688 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline 1.689 \isanewline 1.690 \isacommand{ML}\isamarkupfalse% 1.691 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline