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 Thu Nov 24 14:48:22 2011 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Dec 01 16:54:20 2011 +0100
1.3 @@ -428,7 +428,7 @@
1.4 \begin{isamarkuptext}%
1.5 With the above definition we run into problems with parsing the Script InverseZTransform:
1.6 This leads to "ambiguous parse trees" and we avoid this by shifting the definition
1.7 - to Rationa.thy and re-building Isac.
1.8 + to Rational.thy and re-building Isac.
1.9 ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;
1.10 it only works due to re-building Isac several times (indicated explicityl).%
1.11 \end{isamarkuptext}%
1.12 @@ -469,6 +469,43 @@
1.13 \end{isamarkuptext}%
1.14 \isamarkuptrue%
1.15 %
1.16 +\isamarkupsubsubsection{get the numerator out of a fraction%
1.17 +}
1.18 +\isamarkuptrue%
1.19 +%
1.20 +\begin{isamarkuptext}%
1.21 +get numerator should also become a constant for the isabelle parser:%
1.22 +\end{isamarkuptext}%
1.23 +\isamarkuptrue%
1.24 +\isacommand{consts}\isamarkupfalse%
1.25 +\isanewline
1.26 +\ \ 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}}\isanewline
1.27 +%
1.28 +\isadelimML
1.29 +\isanewline
1.30 +%
1.31 +\endisadelimML
1.32 +%
1.33 +\isatagML
1.34 +\isacommand{ML}\isamarkupfalse%
1.35 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.36 +fun\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ \isanewline
1.37 + \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline
1.38 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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\isanewline
1.39 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{24}{\isachardollar}}denom\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.40 +\ \ \ \ \ \ \ \ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
1.41 +\ \ \ \ \ \ \ \ \ \ \ \ {\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}}\ num{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.42 + \ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ num{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.43 +\ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.44 +\isanewline
1.45 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
1.46 +\endisatagML
1.47 +{\isafoldML}%
1.48 +%
1.49 +\isadelimML
1.50 +%
1.51 +\endisadelimML
1.52 +%
1.53 \isamarkupsubsection{solve equation%
1.54 }
1.55 \isamarkuptrue%
1.56 @@ -659,6 +696,113 @@
1.57 %
1.58 \endisadelimML
1.59 %
1.60 +\begin{isamarkuptext}%
1.61 +for the programming language a function
1.62 + collecting all the above manipulations is helpful%
1.63 +\end{isamarkuptext}%
1.64 +\isamarkuptrue%
1.65 +%
1.66 +\isadelimML
1.67 +%
1.68 +\endisadelimML
1.69 +%
1.70 +\isatagML
1.71 +\isacommand{ML}\isamarkupfalse%
1.72 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.73 +fun\ mk{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ T\ {\isaliteral{3D}{\isacharequal}}\ Free{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}TODO\ DELETE\ WITH\ numbers{\isaliteral{5F}{\isacharunderscore}}to{\isaliteral{5F}{\isacharunderscore}}string{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.74 +fun\ flip{\isaliteral{5F}{\isacharunderscore}}sign\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}TODO\ improve\ for\ use\ in\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ etc{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.75 +\ \ let\ val\ minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ type{\isaliteral{5F}{\isacharunderscore}}of\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ mk{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\isanewline
1.76 +\ \ 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.77 +fun\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ s\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.78 +\ \ 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.79 +\ \ 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.80 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.81 +\isacommand{ML}\isamarkupfalse%
1.82 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.83 +e{\isaliteral{5F}{\isacharunderscore}}term\isanewline
1.84 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.85 +\isacommand{ML}\isamarkupfalse%
1.86 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.87 +fun\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.88 +\ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ then\ error\ {\isaliteral{22}{\isachardoublequote}}mk{\isaliteral{5F}{\isacharunderscore}}prod\ called\ with\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ else\ prod\isanewline
1.89 +\ \ {\isaliteral{7C}{\isacharbar}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.90 +\ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ then\ t\ else\ 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}}prod{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\isanewline
1.91 +\ \ {\isaliteral{7C}{\isacharbar}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ t{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.92 +\ \ \ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ \isanewline
1.93 +\ \ \ \ \ \ \ \ then\ \isanewline
1.94 +\ \ \ \ \ \ \ \ \ \ \ let\ val\ p\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.95 +\ \ \ \ \ \ \ \ \ \ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ p\ ts\ end\ \isanewline
1.96 +\ \ \ \ \ \ \ \ else\ \isanewline
1.97 +\ \ \ \ \ \ \ \ \ \ \ let\ val\ p\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}prod{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.98 +\ \ \ \ \ \ \ \ \ \ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ p\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ts{\isaliteral{29}{\isacharparenright}}\ end\ \isanewline
1.99 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.100 +\isacommand{ML}\isamarkupfalse%
1.101 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.102 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.103 +\isacommand{ML}\isamarkupfalse%
1.104 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.105 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}probably\ keept\ these\ test\ in\ test{\isaliteral{2F}{\isacharslash}}Tools{\isaliteral{2F}{\isacharslash}}isac{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}\isanewline
1.106 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.107 +\isanewline
1.108 +val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.109 +term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.110 +\isanewline
1.111 +val\ sol\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.112 +val\ sols\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}list\ sol{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.113 +val\ facs\ {\isaliteral{3D}{\isacharequal}}\ map\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ sols{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.114 +val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ facs{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.115 +term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.116 +\isanewline
1.117 +val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.118 +term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.119 +{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.120 +\isanewline
1.121 +fun\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ sol\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
1.122 +\ \ let\ val\ ts\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}list\ sol\isanewline
1.123 +\ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}map\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ ts{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.124 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
1.125 +val\ sol\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.126 +val\ fs\ {\isaliteral{3D}{\isacharequal}}\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ sol{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.127 +term{\isadigit{2}}str\ fs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
1.128 +{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.129 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
1.130 +\endisatagML
1.131 +{\isafoldML}%
1.132 +%
1.133 +\isadelimML
1.134 +%
1.135 +\endisadelimML
1.136 +%
1.137 +\begin{isamarkuptext}%
1.138 +This function needs to be packed such that it can be evaluated by the Lucas-Interpreter:
1.139 + # shift these functions into the related Equation.thy
1.140 + # -- compare steps done with get_denominator above%
1.141 +\end{isamarkuptext}%
1.142 +\isamarkuptrue%
1.143 +%
1.144 +\isadelimML
1.145 +%
1.146 +\endisadelimML
1.147 +%
1.148 +\isatagML
1.149 +\isacommand{ML}\isamarkupfalse%
1.150 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.151 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Equation{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.152 +fun\ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ t\ thy\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.153 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}let\ val\ prod\ {\isaliteral{3D}{\isacharequal}}\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ t\isanewline
1.154 +\ \ \ \ \ in\ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
1.155 +\ \ \ \ \ \ \ \ \ \ \ \ {\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}}\ prod{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.156 + \ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ prod{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.157 +\ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}\isanewline
1.158 +\ \ \ \ \ handle\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.159 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
1.160 +\endisatagML
1.161 +{\isafoldML}%
1.162 +%
1.163 +\isadelimML
1.164 +%
1.165 +\endisadelimML
1.166 +%
1.167 \isamarkupsubsubsection{build expression%
1.168 }
1.169 \isamarkuptrue%
1.170 @@ -711,7 +855,7 @@
1.171 \isacommand{axiomatization}\isamarkupfalse%
1.172 \ \isakeyword{where}\isanewline
1.173 \ \ ansatz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
1.174 -\ \ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n\ \ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.175 +\ \ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n\ \ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isanewline
1.176 %
1.177 \isadelimML
1.178 \isanewline
1.179 @@ -1206,7 +1350,9 @@
1.180 \ \ \ \ \ 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}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ ONLY\ USED{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.181 \ \ \ \ \ 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}}\ 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.182 \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.183 -\ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.184 +\ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.185 +\ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.186 +\ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.187 \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
1.188 \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.189 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.190 @@ -1248,9 +1394,16 @@
1.191 {\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.192 \isanewline
1.193 {\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{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}PolyEq{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.194 -{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}abcFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}meth{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.195 -{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ zzz{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.196 -{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
1.197 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}abcFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.198 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ zzz{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.199 +\isanewline
1.200 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}numerator\ funterm{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.201 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}facs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.202 +\isanewline
1.203 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}funterm\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}num\ {\isaliteral{2F}{\isacharslash}}\ facs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.204 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eq\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Try\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ ansatz\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ eq{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
1.205 +\isanewline
1.206 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline
1.207 \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.208 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.209 \endisatagML
1.210 @@ -1315,7 +1468,10 @@
1.211 \ \ {\isaliteral{22}{\isachardoublequote}}stepResponse\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.212 val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
1.213 \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.214 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
1.215 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.216 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.217 +\isacommand{ML}\isamarkupfalse%
1.218 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.219 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}Add{\isaliteral{5F}{\isacharunderscore}}Given{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.220 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}Add{\isaliteral{5F}{\isacharunderscore}}Find{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.221 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}Specify{\isaliteral{5F}{\isacharunderscore}}Theory{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.222 @@ -1324,10 +1480,7 @@
1.223 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.224 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ {\isaliteral{28}{\isacharparenleft}}ruleZY{\isaliteral{2C}{\isacharcomma}}\ Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}ruleZY{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ 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}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}TODO\ naming{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.225 val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ {\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{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.226 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.227 -\isacommand{ML}\isamarkupfalse%
1.228 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.229 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Empty{\isaliteral{5F}{\isacharunderscore}}Tac\ instead\ of\ SubProblem{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.230 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ SubProblem{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.231 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.232 \endisatagML
1.233 {\isafoldML}%
1.234 @@ -1352,10 +1505,10 @@
1.235 [BOOL (-1 + -2 * z + 8 * z ^^^ 2 = 0), REAL z]'
1.236 ... and see the SubProblem with correct arguments from searching next step
1.237 (program text !!!--->!!! STac (script tactic) with arguments evaluated.)
1.238 - # do we have the right Script ...
1.239 + # do we have the right Script ...difference in the argumentsdifference in the arguments
1.240 val Script s = (#scr o get_met) ["SignalProcessing","Z_Transform","inverse"];
1.241 writeln (term2str s);
1.242 - ... shows the right script.
1.243 + ... shows the right script.difference in the arguments
1.244 # test --- why helpless here ? --- shows: replace no_meth by [no_meth] in Script%
1.245 \end{isamarkuptext}%
1.246 \isamarkuptrue%
1.247 @@ -1367,9 +1520,7 @@
1.248 \isatagML
1.249 \isacommand{ML}\isamarkupfalse%
1.250 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.251 -print{\isaliteral{5F}{\isacharunderscore}}depth\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.252 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Empty{\isaliteral{5F}{\isacharunderscore}}Tac\ instead\ Model{\isaliteral{5F}{\isacharunderscore}}Problem{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.253 -print{\isaliteral{5F}{\isacharunderscore}}depth\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.254 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Model{\isaliteral{5F}{\isacharunderscore}}Problem{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.255 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.256 \endisatagML
1.257 {\isafoldML}%
1.258 @@ -1380,9 +1531,10 @@
1.259 %
1.260 \begin{isamarkuptext}%
1.261 Instead of nxt = Model_Problem above we had Empty_Tac; the search for the reason
1.262 - considered the following points:
1.263 + considered the following points:difference in the arguments
1.264 # comparison with subsection { *solve equation* }: there solving this equation works,
1.265 - so there must be some difference in the arguments of the Subproblem.%
1.266 + so there must be some difference in the arguments of the Subproblem:
1.267 + RIGHT: we had [no_meth] instead of [no_met] ;-))%
1.268 \end{isamarkuptext}%
1.269 \isamarkuptrue%
1.270 %
1.271 @@ -1393,31 +1545,10 @@
1.272 \isatagML
1.273 \isacommand{ML}\isamarkupfalse%
1.274 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.275 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\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{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.276 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.277 -\isacommand{ML}\isamarkupfalse%
1.278 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.279 -\isanewline
1.280 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.281 -\isacommand{ML}\isamarkupfalse%
1.282 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.283 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.284 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.285 -\isacommand{ML}\isamarkupfalse%
1.286 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.287 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Add{\isaliteral{5F}{\isacharunderscore}}Find{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.288 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.289 -\isacommand{ML}\isamarkupfalse%
1.290 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.291 -show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.292 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.293 -\isacommand{ML}\isamarkupfalse%
1.294 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.295 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Empty{\isaliteral{5F}{\isacharunderscore}}Tac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.296 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.297 -\isacommand{ML}\isamarkupfalse%
1.298 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.299 -val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Empty{\isaliteral{5F}{\isacharunderscore}}Tac\ instead\ Specify{\isaliteral{5F}{\isacharunderscore}}Theory{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.300 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Add{\isaliteral{5F}{\isacharunderscore}}Given\ equality\ {\isaliteral{28}{\isacharparenleft}}{\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{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.301 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Add{\isaliteral{5F}{\isacharunderscore}}Given\ solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.302 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Add{\isaliteral{5F}{\isacharunderscore}}Find\ solutions\ z{\isaliteral{5F}{\isacharunderscore}}i{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.303 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Theory\ Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.304 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.305 \endisatagML
1.306 {\isafoldML}%
1.307 @@ -1427,7 +1558,8 @@
1.308 \endisadelimML
1.309 %
1.310 \begin{isamarkuptext}%
1.311 -We had "nxt = (Empty_Tac"; the search for the reason considered the following points:
1.312 +We had "nxt = Empty_Tac instead Specify_Theory;
1.313 + the search for the reason considered the following points:
1.314 # was there an error message ? NO --ok
1.315 # has "nxt = Add_Find" been inserted in pt: get_obj g_pbl pt (fst p); YES --ok
1.316 # what is the returned "formula": print_depth 999; f; print_depth 999; --
1.317 @@ -1458,54 +1590,47 @@
1.318 \isatagML
1.319 \isacommand{ML}\isamarkupfalse%
1.320 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.321 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}abcFormula{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.322 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.323 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.324 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{22}{\isachardoublequote}}nxt\ {\isaliteral{3D}{\isacharequal}}\ Rewrite{\isaliteral{5F}{\isacharunderscore}}Set{\isaliteral{5F}{\isacharunderscore}}Inst\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}bdv{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abcFormula{\isaliteral{5F}{\isacharunderscore}}simplify{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.325 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.326 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.327 +\isacommand{ML}\isamarkupfalse%
1.328 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.329 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.330 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.331 \isacommand{ML}\isamarkupfalse%
1.332 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.333 -\isanewline
1.334 +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.335 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.336 \isacommand{ML}\isamarkupfalse%
1.337 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.338 -show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.339 +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.340 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.341 \isacommand{ML}\isamarkupfalse%
1.342 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.343 +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.344 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.345 \isacommand{ML}\isamarkupfalse%
1.346 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.347 -\isanewline
1.348 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.349 -\isacommand{ML}\isamarkupfalse%
1.350 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.351 -\isanewline
1.352 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.353 -\isacommand{ML}\isamarkupfalse%
1.354 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.355 -\isanewline
1.356 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.357 -\isacommand{ML}\isamarkupfalse%
1.358 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.359 -\isanewline
1.360 +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.361 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.362 \isanewline
1.363 \isacommand{ML}\isamarkupfalse%
1.364 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.365 -\isanewline
1.366 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.367 -\isacommand{ML}\isamarkupfalse%
1.368 -\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.369 -%
1.370 -\isaantiq
1.371 -theory\ Isac{}%
1.372 -\endisaantiq
1.373 -\isanewline
1.374 +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.375 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.376 \isanewline
1.377 \isacommand{ML}\isamarkupfalse%
1.378 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.379 +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.380 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.381 +\isanewline
1.382 \isacommand{ML}\isamarkupfalse%
1.383 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.384 +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.385 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.386 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
1.387 \isacommand{ML}\isamarkupfalse%
1.388 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.389 @@ -1533,7 +1658,6 @@
1.390 \isatagML
1.391 \isacommand{ML}\isamarkupfalse%
1.392 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
1.393 -\isanewline
1.394 {\isaliteral{2A7D}{\isacharverbatimclose}}%
1.395 \endisatagML
1.396 {\isafoldML}%