930 \isadelimML |
932 \isadelimML |
931 % |
933 % |
932 \endisadelimML |
934 \endisadelimML |
933 % |
935 % |
934 \begin{isamarkuptext}% |
936 \begin{isamarkuptext}% |
935 \noindent The tracing output of the calc tree after apllying this |
937 \noindent The tracing output of the calc tree after applying this |
936 function was \ttfamily 24 / factors\_from\_solution |
938 function was: |
937 [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily |
939 \begin{verbatim} |
938 val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations |
940 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])] |
939 indicate, that the Lucas-Interpreter (LIP) does not know how to |
941 \end{verbatim} |
940 evaluate\\ \ttfamily factors\_from\_solution, \normalfont so we knew |
942 and the next step: |
941 that there is something wrong or missing.% |
943 \begin{verbatim} |
942 \end{isamarkuptext}% |
944 val nxt = ("Empty_Tac", ...): tac'_) |
943 \isamarkuptrue% |
945 \end{verbatim} |
944 % |
946 These observations indicate, that the Lucas-Interpreter (LIP) |
945 \begin{isamarkuptext}% |
947 does not know how to evaluate \ttfamily factors\_from\_solution |
946 \noindent First we isolate the difficulty in the program as follows:\\ |
948 \normalfont, so we knew that there is something wrong or missing.% |
947 \ttfamily \par \noindent |
949 \end{isamarkuptext}% |
948 "(L\_L::bool list) = (SubProblem (PolyEq',"\^\\ |
950 \isamarkuptrue% |
949 "[abcFormula,degree\_2,polynomial,univariate,equation],[no\_met])"\^\\ |
951 % |
950 "[BOOL equ, REAL zzz]);"\^\\ |
952 \begin{isamarkuptext}% |
951 "(facs::real) = factors\_from\_solution L\_L;"\^\\ |
953 \noindent First we isolate the difficulty in the program as follows: |
952 "(foo::real) = Take facs"\^\\ |
954 \begin{verbatim} |
|
955 " (L_L::bool list) = (SubProblem (PolyEq', " ^ |
|
956 " [abcFormula, degree_2, polynomial, " ^ |
|
957 " univariate,equation], " ^ |
|
958 " [no_met]) " ^ |
|
959 " [BOOL equ, REAL zzz]); " ^ |
|
960 " (facs::real) = factors_from_solution L_L; " ^ |
|
961 " (foo::real) = Take facs " ^ |
|
962 \end{verbatim} |
|
963 |
|
964 \par \noindent And see the tracing output: |
|
965 |
|
966 \begin{verbatim} |
|
967 [(([], Frm), Problem (Isac, [inverse, |
|
968 Z_Transform, |
|
969 SignalProcessing])), |
|
970 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))), |
|
971 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), |
|
972 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)), |
|
973 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)), |
|
974 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0), |
|
975 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)| |
|
976 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)), |
|
977 (([3,2], Res), z = 1 / 2 | z = -1 / 4), |
|
978 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]), |
|
979 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]), |
|
980 (([3], Res), [ z = 1 / 2, z = -1 / 4]), |
|
981 (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])] |
|
982 \end{verbatim} |
|
983 |
|
984 \par \noindent In particular that: |
|
985 |
|
986 \begin{verbatim} |
|
987 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)), |
|
988 \end{verbatim} |
|
989 \par \noindent Shows the equation which has been created in |
|
990 the program by: |
|
991 \begin{verbatim} |
|
992 "(denom::real) = get_denominator funterm; " ^ |
|
993 (* get_denominator *) |
|
994 "(equ::bool) = (denom = (0::real)); " ^ |
|
995 \end{verbatim} |
953 |
996 |
954 \normalfont \par \noindent And see the tracing output:\\ |
997 \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully, |
955 \ttfamily \par \noindent \lbrack\\ |
|
956 ((\lbrack\rbrack, Frm), Problem |
|
957 (Isac, \lbrack inverse, Z\_Transform, SignalProcessing\rbrack)),\\ |
|
958 ((\lbrack 1\rbrack, Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),\\ |
|
959 ((\lbrack 1\rbrack, Res), |
|
960 ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),\\ |
|
961 ((\lbrack 2\rbrack, Res), |
|
962 ?X' z = 24 / (-1 + -2 * z + 8 * z \^\^\^ ~2)),\\ |
|
963 ((\lbrack 3\rbrack, Pbl), |
|
964 solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\ |
|
965 ((\lbrack 3,1\rbrack, Frm), -1 + -2 * z + 8 * z \^\^\^ ~2 = 0),\\ |
|
966 ((\lbrack 3,1\rbrack, Res), |
|
967 z = (- -2 + sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)|\\ |
|
968 z = (- -2 - sqrt (-2 \^\^\^ ~2 - 4 * 8 * -1)) / (2 * 8)),\\ |
|
969 ((\lbrack 3,2\rbrack, Res), z = 1 / 2 | z = -1 / 4),\\ |
|
970 ((\lbrack 3,3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\ |
|
971 ((\lbrack 3,4\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\ |
|
972 ((\lbrack 3\rbrack, Res), \lbrack z = 1 / 2, z = -1 / 4\rbrack),\\ |
|
973 ((\lbrack 4\rbrack, Frm), |
|
974 factors\_from\_solution \lbrackz = 1 / 2, z = -1 / 4])\\ |
|
975 \rbrack\\ |
|
976 |
|
977 \normalfont \noindent In particular that:\\ |
|
978 \ttfamily \par \noindent ((\lbrack 3\rbrack, Pbl), |
|
979 solve (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0, z)),\\ |
|
980 \normalfont \par \noindent Shows the equation which has been created in |
|
981 the program by: \ttfamily \\ |
|
982 |
|
983 \noindent "(denom::real) = get\_denominator funterm;"\^ |
|
984 ~(*get\_denominator*)\\ |
|
985 "(equ::bool) = (denom = (0::real));"\^\\ |
|
986 |
|
987 \noindent get\_denominator \normalfont has been evaluated successfully, |
|
988 but not\\ \ttfamily factors\_from\_solution.\normalfont |
998 but not\\ \ttfamily factors\_from\_solution.\normalfont |
989 So we stepwise compare with an analogous case, \ttfamily get\_denominator |
999 So we stepwise compare with an analogous case, \ttfamily get\_denominator |
990 \normalfont successfully done above: We know that LIP evaluates |
1000 \normalfont successfully done above: We know that LIP evaluates |
991 expressions in the program by use of the \emph{srls}, so we try to get |
1001 expressions in the program by use of the \emph{srls}, so we try to get |
992 the original \emph{srls}.\\ |
1002 the original \emph{srls}.\\ |
993 |
1003 |
994 \noindent \ttfamily val \lbrace srls,\ldots\rbrace\ttfamily |
1004 \begin{verbatim} |
995 = get\_met \lbrack "SignalProcessing", |
1005 val {srls,...} = get_met ["SignalProcessing", |
996 "Z\_Transform","inverse"\rbrack;\\ |
1006 "Z_Transform", |
|
1007 "inverse"]; |
|
1008 \end{verbatim} |
997 |
1009 |
998 \par \noindent \normalfont Create 2 good example terms\\ |
1010 \par \noindent Create 2 good example terms: |
999 \ttfamily \par \noindent val SOME t1 =\\ |
|
1000 parseNEW ctxt "get\_denominator ((111::real) / 222)"; |
|
1001 \par \noindent val SOME t2 =\\ |
|
1002 parseNEW ctxt "factors\_from\_solution \lbrack(z::real) |
|
1003 = 1/2, z = -1/4\rbrack";\\ |
|
1004 |
1011 |
1005 \par \noindent \normalfont Rewrite the terms using srls:\\ |
1012 \begin{verbatim} |
|
1013 val SOME t1 = |
|
1014 parseNEW ctxt "get_denominator ((111::real) / 222)"; |
|
1015 val SOME t2 = |
|
1016 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]"; |
|
1017 \end{verbatim} |
|
1018 |
|
1019 \par \noindent Rewrite the terms using srls:\\ |
1006 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\ |
1020 \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\ |
1007 rewrite\_set\_ thy true srls t2;\\ |
1021 rewrite\_set\_ thy true srls t2;\\ |
1008 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives |
1022 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives |
1009 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the |
1023 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the |
1010 \emph{srls}:\\ |
1024 \emph{srls}: |
1011 |
1025 \begin{verbatim} |
1012 \par \noindent \ttfamily val srls = Rls \lbrace id = |
1026 val srls = |
1013 "srls\_InverseZTransform", rules =\\ |
1027 Rls{id = "srls_InverseZTransform", |
1014 \lbrack Calc("Rational.get\_numerator",\\ |
1028 rules = [Calc("Rational.get_numerator", |
1015 eval\_get\_numerator "Rational.get\_numerator"),\\ |
1029 eval_get_numerator "Rational.get_numerator"), |
1016 Calc("Partial\_Fractions.factors\_from\_solution",\\ |
1030 Calc("Partial_Fractions.factors_from_solution", |
1017 eval\_factors\_from\_solution |
1031 eval_factors_from_solution |
1018 "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\ |
1032 "Partial_Fractions.factors_from_solution")]} |
1019 |
1033 \end{verbatim} |
1020 \par \noindent \normalfont Here everthing is perfect. So the error can |
1034 \par \noindent Here everthing is perfect. So the error can |
1021 only be in the SML code of \ttfamily eval\_factors\_from\_solution. |
1035 only be in the SML code of \ttfamily eval\_factors\_from\_solution. |
1022 \normalfont We try to check the code with an existing test; since the |
1036 \normalfont We try to check the code with an existing test; since the |
1023 \emph{code} is in |
1037 \emph{code} is in |
1024 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy |
1038 \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy |
1025 \normalfont\end{center} |
1039 \normalfont\end{center} |
1026 the \emph{test} should be in |
1040 the \emph{test} should be in |
1027 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml |
1041 \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml |
1028 \normalfont\end{center} |
1042 \normalfont\end{center} |
1029 \par \noindent After updating the function \ttfamily |
1043 \par \noindent After updating the function \ttfamily |
1030 factors\_from\_solution \normalfont to a new version and putting a |
1044 factors\_from\_solution \normalfont to a new version and putting a |
1031 testcase to \ttfamily Partial\_Fractions.sml \normalfont we tried again |
1045 test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again |
1032 to evaluate the term with the same result. |
1046 to evaluate the term with the same result. |
1033 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that |
1047 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that |
1034 everything is working fine. Also we checked that the test \ttfamily |
1048 everything is working fine. Also we checked that the test \ttfamily |
1035 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy |
1049 partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy |
1036 \normalfont |
1050 \normalfont |
1037 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml" |
1051 \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml" |
1038 \normalfont \end{center} |
1052 \normalfont \end{center} |
1039 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of |
1053 and \ttfamily Partial\_Fractions.thy \normalfont is part is part of |
1040 {\sisac} by evaluating\\ |
1054 {\sisac} by evaluating |
1041 |
1055 |
1042 \par \noindent \ttfamily val thy = @\lbrace theory~Isac \rbrace; |
1056 \begin{verbatim} |
1043 \normalfont \\ |
1057 val thy = \hyperlink{theory.Isac}{\mbox{\isa{Isac}}}; |
|
1058 \end{verbatim} |
1044 |
1059 |
1045 \par \noindent \normalfont After rebuilding {\sisac} again it worked.% |
1060 After rebuilding {\sisac} again it worked.% |
1046 \end{isamarkuptext}% |
1061 \end{isamarkuptext}% |
1047 \isamarkuptrue% |
1062 \isamarkuptrue% |
1048 % |
1063 % |
1049 \isamarkupsubsubsection{Build Expression% |
1064 \isamarkupsubsubsection{Build Expression% |
1050 } |
1065 } |
1051 \isamarkuptrue% |
1066 \isamarkuptrue% |
1052 % |
1067 % |
1053 \begin{isamarkuptext}% |
1068 \begin{isamarkuptext}% |
1054 \noindent In {\sisac}'s CTP-based programming language we can build |
1069 \noindent In {\sisac}'s TP-based programming language we can build |
1055 expressions by:\\ |
1070 expressions by:\\ |
1056 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont% |
1071 \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont% |
1057 \end{isamarkuptext}% |
1072 \end{isamarkuptext}% |
1058 \isamarkuptrue% |
1073 \isamarkuptrue% |
1059 % |
1074 % |
1929 % |
1944 % |
1930 \isatagML |
1945 \isatagML |
1931 \isacommand{ML}\isamarkupfalse% |
1946 \isacommand{ML}\isamarkupfalse% |
1932 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1947 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
1933 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline |
1948 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline |
1934 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1949 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1935 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1950 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1936 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline |
1951 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline |
1937 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1952 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1938 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1953 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1939 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1954 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1940 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1955 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1941 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline |
1956 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline |
1942 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1957 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1943 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1958 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1944 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1959 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1945 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline |
1960 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline |
1946 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1961 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1947 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1962 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1948 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1963 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1949 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ NONE\isanewline |
1964 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ NONE\isanewline |
1950 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1965 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1951 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1966 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1952 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1967 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1953 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline |
1968 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline |
1954 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1969 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1955 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1970 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1956 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1971 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1957 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1972 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1958 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline |
1973 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator\isanewline |
1959 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1974 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1960 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1975 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1961 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1976 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
1962 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline |
1977 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ simplify\isanewline |
1963 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1978 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1964 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1979 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1965 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1980 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1966 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1981 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1967 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
1982 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
1968 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1983 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1969 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
1984 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
1970 \endisatagML |
1985 \endisatagML |
1971 {\isafoldML}% |
1986 {\isafoldML}% |
1972 % |
1987 % |
1973 \isadelimML |
1988 \isadelimML |
1974 % |
1989 % |
1975 \endisadelimML |
1990 \endisadelimML |
1976 % |
1991 % |
1977 \begin{isamarkuptext}% |
1992 \begin{isamarkuptext}% |
1978 \noindent To solve the equation it is neccessary to drop the left hand |
1993 \noindent To solve the equation it is necessary to drop the left hand |
1979 side, now we only need the denominator of the right hand side. The first |
1994 side, now we only need the denominator of the right hand side. The first |
1980 equation solves the zeros of our expression.% |
1995 equation solves the zeros of our expression.% |
1981 \end{isamarkuptext}% |
1996 \end{isamarkuptext}% |
1982 \isamarkuptrue% |
1997 \isamarkuptrue% |
1983 % |
1998 % |
2019 % |
2034 % |
2020 \isatagML |
2035 \isatagML |
2021 \isacommand{ML}\isamarkupfalse% |
2036 \isacommand{ML}\isamarkupfalse% |
2022 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
2037 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
2023 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline |
2038 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline |
2024 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline |
2039 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2025 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2040 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2026 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline |
2041 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2027 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline |
2042 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2028 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2043 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2029 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2044 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ argument{\isaliteral{5F}{\isacharunderscore}}in\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2030 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline |
2045 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}funterm{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2031 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ \isanewline |
2046 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}denom{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\ funterm{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2032 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
2047 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline |
2033 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\isanewline |
2048 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ get{\isaliteral{5F}{\isacharunderscore}}denominator\isanewline |
2034 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2049 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2035 \ \ \ \ {\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 |
2050 \ \ \ \ {\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 |
2036 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2051 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}L{\isaliteral{5F}{\isacharunderscore}}L{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2037 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2052 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2038 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2053 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}linear{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{2C}{\isacharcomma}}test{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2039 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2054 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Test{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}linear{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2040 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline |
2055 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ equ{\isaliteral{2C}{\isacharcomma}}\ REAL\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2041 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2056 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2042 \isanewline |
2057 \isanewline |
2043 \ \ parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2058 \ \ parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2044 \ \ val\ sc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}inst{\isaliteral{5F}{\isacharunderscore}}abs\ thy{\isaliteral{29}{\isacharparenright}}\ o\ term{\isaliteral{5F}{\isacharunderscore}}of\ o\ the\ o\ {\isaliteral{28}{\isacharparenleft}}parse\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2059 \ \ val\ sc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}inst{\isaliteral{5F}{\isacharunderscore}}abs\ thy{\isaliteral{29}{\isacharparenright}}\ o\ term{\isaliteral{5F}{\isacharunderscore}}of\ o\ the\ o\ {\isaliteral{28}{\isacharparenleft}}parse\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2045 \ \ atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2060 \ \ atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2062 \endisadelimML |
2077 \endisadelimML |
2063 % |
2078 % |
2064 \isatagML |
2079 \isatagML |
2065 \isacommand{ML}\isamarkupfalse% |
2080 \isacommand{ML}\isamarkupfalse% |
2066 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
2081 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
2067 \ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2082 \ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ \isanewline |
2068 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2083 \ \ \ \ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2069 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2084 \ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2070 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline |
2085 \ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2071 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2086 \ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline |
2072 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2087 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ asm\ in\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2073 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2088 \ \ \ \ \ \ \ \ \ \ \ \ Calc\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Orderings{\isaliteral{2E}{\isachardot}}ord{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}less{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}eval{\isaliteral{5F}{\isacharunderscore}}equ\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}less{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2074 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2089 \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2075 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2090 \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2076 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2091 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2077 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline |
2092 \ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2078 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % |
2093 \ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline |
|
2094 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % |
2079 \isaantiq |
2095 \isaantiq |
2080 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS{}% |
2096 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS{}% |
2081 \endisaantiq |
2097 \endisaantiq |
2082 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2098 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2083 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2099 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline |
2084 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2085 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % |
2101 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}NIL{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ % |
2086 \isaantiq |
2102 \isaantiq |
2087 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}NIL{}% |
2103 thm\ NTH{\isaliteral{5F}{\isacharunderscore}}NIL{}% |
2088 \endisaantiq |
2104 \endisaantiq |
2089 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2105 {\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2090 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2106 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}lhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}lhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2091 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2107 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Tools{\isaliteral{2E}{\isachardot}}rhs{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{22}{\isachardoublequote}}eval{\isaliteral{5F}{\isacharunderscore}}rhs{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2092 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2108 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Atools{\isaliteral{2E}{\isachardot}}argument{\isaliteral{27}{\isacharprime}}{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2093 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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 |
2109 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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 |
2094 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2110 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2095 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2111 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2096 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2112 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2097 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2113 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2098 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2114 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2099 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline |
2115 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ \isanewline |
2100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2116 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2101 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2117 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2102 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2118 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ eval{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}drop{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline |
2103 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2119 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline |
2104 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr\isanewline |
2120 \ \ \ \ \ \ \ \ \ scr\ {\isaliteral{3D}{\isacharequal}}\ EmptyScr{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2105 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
2106 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
2121 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
2107 \endisatagML |
2122 \endisatagML |
2108 {\isafoldML}% |
2123 {\isafoldML}% |
2109 % |
2124 % |
2110 \isadelimML |
2125 \isadelimML |
2203 \ \ \ \ \ {\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 |
2218 \ \ \ \ \ {\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 |
2204 \ \ \ \ \ {\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 |
2219 \ \ \ \ \ {\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 |
2205 \isanewline |
2220 \isanewline |
2206 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2221 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ eqr\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ eqr{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2207 \ \ \ \ \ {\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 |
2222 \ \ \ \ \ {\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 |
2208 \ \ \ \ \ {\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 |
2223 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Substitute\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3D}{\isacharequal}}a{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2209 \ \ \ \ \ {\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 |
|
2210 \isanewline |
2224 \isanewline |
2211 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2225 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleYZ\ False\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2212 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2226 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ pbz\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ pbz{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2213 \isanewline |
2227 \isanewline |
2214 \ \ \ \ \ {\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 |
2228 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Take\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}z\ {\isaliteral{3D}{\isacharequal}}\ pbz{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2215 \ \ \ \ \ {\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 |
2229 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ inverse{\isaliteral{5F}{\isacharunderscore}}z\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{5F}{\isacharunderscore}}z{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2216 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ iztrans\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ iztrans{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2230 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ n{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{3D}{\isacharequal}}\ drop{\isaliteral{5F}{\isacharunderscore}}questionmarks\ n{\isaliteral{5F}{\isacharunderscore}}eq\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline |
2217 \ \ \ \ \ {\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 |
|
2218 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline |
2231 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}in\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline |
2219 \ \ \ \ {\isaliteral{29}{\isacharparenright}}\isanewline |
2232 \ \ \ \ {\isaliteral{29}{\isacharparenright}}\isanewline |
2220 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2233 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2221 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
2234 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
2222 \endisatagML |
2235 \endisatagML |
2353 % |
2366 % |
2354 \begin{isamarkuptext}% |
2367 \begin{isamarkuptext}% |
2355 \noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had |
2368 \noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had |
2356 \ttfamily Empty\_Tac; \normalfont the search for the reason considered |
2369 \ttfamily Empty\_Tac; \normalfont the search for the reason considered |
2357 the following points:\begin{itemize} |
2370 the following points:\begin{itemize} |
2358 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?\\ |
2371 \item What shows \ttfamily show\_pt pt;\normalfont\ldots? |
2359 \ttfamily ((\lbrack 2\rbrack, Res), ?X' z = 24 / |
2372 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim} |
2360 (-1 + -2 * z + 8 * z \^\^\^ ~2))\rbrack\normalfont\\ |
|
2361 The calculation is ok but no \ttfamily next \normalfont step found: |
2373 The calculation is ok but no \ttfamily next \normalfont step found: |
2362 Should be\\ \ttfamily nxt = Subproblem\normalfont! |
2374 Should be\\ \ttfamily nxt = Subproblem\normalfont! |
2363 \item What shows \ttfamily trace\_script := true; \normalfont we read |
2375 \item What shows \ttfamily trace\_script := true; \normalfont we read |
2364 bottom up\ldots\\ |
2376 bottom up\ldots |
2365 \ttfamily @@@next leaf 'SubProbfrom\\ |
2377 \begin{verbatim} |
2366 (PolyEq',\\ |
2378 @@@next leaf 'SubProblem |
2367 \lbrack abcFormula, degree\_2, polynomial, univariate, |
2379 (PolyEq',[abcFormula, degree_2, polynomial, |
2368 equation\rbrack,\\ |
2380 univariate, equation], no_meth) |
2369 no\_meth)\\ |
2381 [BOOL equ, REAL z]' |
2370 \lbrack BOOL equ, REAL z\rbrack' ---> STac 'SubProblem\\ |
2382 ---> STac 'SubProblem (PolyEq', |
2371 (PolyEq',\\ |
2383 [abcFormula, degree_2, polynomial, |
2372 [abcFormula, degree\_2, polynomial, univariate, equation],\\ |
2384 univariate, equation], no_meth) |
2373 no\_meth)\\ |
2385 [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]' |
2374 \lbrack BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), |
2386 \end{verbatim} |
2375 REAL z\rbrack'\normalfont\\ |
|
2376 We see the SubProblem with correct arguments from searching next |
2387 We see the SubProblem with correct arguments from searching next |
2377 step (program text !!!--->!!! STac (script tactic) with arguments |
2388 step (program text !!!--->!!! STac (script tactic) with arguments |
2378 evaluated.) |
2389 evaluated.) |
2379 \item Do we have the right Script \ldots difference in the |
2390 \item Do we have the right Script \ldots difference in the |
2380 argumentsdifference in the arguments\ldots\\ |
2391 arguments in the arguments\ldots |
2381 \ttfamily val Script s =\\ |
2392 \begin{verbatim} |
2382 (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\ |
2393 val Script s = |
2383 writeln (term2str s);\normalfont\\ |
2394 (#scr o get_met) ["SignalProcessing", |
|
2395 "Z_Transform", |
|
2396 "inverse"]; |
|
2397 writeln (term2str s); |
|
2398 \end{verbatim} |
2384 \ldots shows the right script. Difference in the arguments. |
2399 \ldots shows the right script. Difference in the arguments. |
2385 \item Test --- Why helpless here ? --- shows: \ttfamily replace |
2400 \item Test --- Why helpless here ? --- shows: \ttfamily replace |
2386 no\_meth by [no\_meth] \normalfont in Script |
2401 no\_meth by [no\_meth] \normalfont in Script |
2387 \end{itemize}% |
2402 \end{itemize}% |
2388 \end{isamarkuptext}% |
2403 \end{isamarkuptext}% |
2593 \noindent As a last step we check the tracing output of the last calc |
2610 \noindent As a last step we check the tracing output of the last calc |
2594 tree instruction and compare it with the pre-calculated result.% |
2611 tree instruction and compare it with the pre-calculated result.% |
2595 \end{isamarkuptext}% |
2612 \end{isamarkuptext}% |
2596 \isamarkuptrue% |
2613 \isamarkuptrue% |
2597 % |
2614 % |
2598 \isadelimML |
2615 \isamarkupsection{Improve and Transfer into Knowledge% |
2599 % |
2616 } |
2600 \endisadelimML |
2617 \isamarkuptrue% |
2601 % |
2618 % |
2602 \isatagML |
2619 \begin{isamarkuptext}% |
2603 \isacommand{ML}\isamarkupfalse% |
2620 We want to improve the very long program \ttfamily InverseZTransform |
2604 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
2621 \normalfont by modularisation: partial fraction decomposition shall |
2605 \ \ trace{\isaliteral{5F}{\isacharunderscore}}script\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2622 become a sub-problem. |
2606 \ \ 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 |
2623 |
2607 \ \ show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
2624 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy |
2608 {\isaliteral{2A7D}{\isacharverbatimclose}}% |
2625 \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy |
2609 \endisatagML |
2626 \normalfont and then modularise. In this case TODO problems?!? |
2610 {\isafoldML}% |
2627 |
2611 % |
2628 We chose another way and go bottom up: first we build the sub-problem in |
2612 \isadelimML |
2629 \ttfamily Partial\_Fractions.thy \normalfont with the term: |
2613 % |
2630 |
2614 \endisadelimML |
2631 $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$ |
2615 \isanewline |
2632 |
|
2633 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont), |
|
2634 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy: |
|
2635 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy |
|
2636 \normalfont and the respective tests to: |
|
2637 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}% |
|
2638 \end{isamarkuptext}% |
|
2639 \isamarkuptrue% |
|
2640 % |
|
2641 \isamarkupsubsection{Transfer to Partial\_Fractions.thy% |
|
2642 } |
|
2643 \isamarkuptrue% |
|
2644 % |
|
2645 \begin{isamarkuptext}% |
|
2646 First we transfer both, knowledge and tests into: |
|
2647 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center} |
|
2648 in order to immediately have the test results. |
|
2649 |
|
2650 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\ |
|
2651 ansatz\_2nd\_order \normalfont and rule-sets --- no problem. |
|
2652 |
|
2653 Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac" |
|
2654 \normalfont is easy. |
|
2655 |
|
2656 But then we copy from:\\ |
|
2657 (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv" |
|
2658 \normalfont\\ to\\ |
|
2659 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv" |
|
2660 \normalfont\\ and cut out the respective part from the program. First we ensure that |
|
2661 the string is correct. When we insert the string into (2) |
|
2662 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.% |
|
2663 \end{isamarkuptext}% |
|
2664 \isamarkuptrue% |
|
2665 % |
|
2666 \isamarkupsubsubsection{'Programming' in ISAC's TP-based Language% |
|
2667 } |
|
2668 \isamarkuptrue% |
|
2669 % |
|
2670 \begin{isamarkuptext}% |
|
2671 At the present state writing programs in {\sisac} is particularly cumbersome. |
|
2672 So we give hints how to cope with the many obstacles. Below we describe the |
|
2673 steps we did in making (2) run. |
|
2674 |
|
2675 \begin{enumerate} |
|
2676 \item We check if the \textbf{string} containing the program is correct. |
|
2677 \item We check if the \textbf{types in the program} are correct. |
|
2678 For this purpose we start start with the first and last lines |
|
2679 \begin{verbatim} |
|
2680 "PartFracScript (f_f::real) (v_v::real) = " ^ |
|
2681 " (let X = Take f_f; " ^ |
|
2682 " pbz = ((Substitute []) X) " ^ |
|
2683 " in pbz)" |
|
2684 \end{verbatim} |
|
2685 The last but one line helps not to bother with ';'. |
|
2686 \item Then we add line by line. Already the first line causes the error. |
|
2687 So we investigate it by |
|
2688 \begin{verbatim} |
|
2689 val ctxt = ProofContext.init_global @ { theory } ; |
|
2690 val SOME t = |
|
2691 parseNEW ctxt "(num_orig::real) = |
|
2692 get_numerator(rhs f_f)"; |
|
2693 \end{verbatim} |
|
2694 and see a type clash: \ttfamily rhs \normalfont from (1) requires type |
|
2695 \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real). |
|
2696 \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore. |
|
2697 \item Type-checking can be very tedious. One might even inspect the |
|
2698 parse-tree of the program with {\sisac}'s specific debug tools: |
|
2699 \begin{verbatim} |
|
2700 val {scr = Script t,...} = |
|
2701 get_met ["simplification", |
|
2702 "of_rationals", |
|
2703 "to_partial_fraction"]; |
|
2704 atomty_thy @ { theory } t ; |
|
2705 \end{verbatim} |
|
2706 \item We check if the \textbf{semantics of the program} by stepwise evaluation |
|
2707 of the program. Evaluation is done by the Lucas-Interpreter, which works |
|
2708 using the knowledge in theory Isac; so we have to re-build Isac. And the |
|
2709 test are performed simplest in a file which is loaded with Isac. |
|
2710 See \ttfamily tests/../partial\_fractions.sml \normalfont. |
|
2711 \end{enumerate}% |
|
2712 \end{isamarkuptext}% |
|
2713 \isamarkuptrue% |
|
2714 % |
|
2715 \isamarkupsubsection{Transfer to Inverse\_Z\_Transform.thy% |
|
2716 } |
|
2717 \isamarkuptrue% |
|
2718 % |
|
2719 \begin{isamarkuptext}% |
|
2720 Unfortunately it was not possible to complete this task. Because we ran out of time\ldots% |
|
2721 \end{isamarkuptext}% |
|
2722 \isamarkuptrue% |
2616 % |
2723 % |
2617 \isadelimtheory |
2724 \isadelimtheory |
2618 \isanewline |
|
2619 % |
2725 % |
2620 \endisadelimtheory |
2726 \endisadelimtheory |
2621 % |
2727 % |
2622 \isatagtheory |
2728 \isatagtheory |
2623 \isacommand{end}\isamarkupfalse% |
2729 \isacommand{end}\isamarkupfalse% |